Theorem true_or_wff_iff_true ≪ | index | src | ≫

\or真值表：\true \or wff \iff \true

theorem true_or_wff_iff_true (A: wff): $ \true \or A \iff \true $;
StepHypRefExpression
1 iff_tran 
(\true \or A \iff A \or \true) \imp (A \or \true \iff \true) \imp (\true \or A \iff \true)
2 or_comm 
\true \or A \iff A \or \true
3 1, 2 ax_mp 
(A \or \true \iff \true) \imp (\true \or A \iff \true)
4 wff_or_true_iff_true 
A \or \true \iff \true
5 3, 4 ax_mp 
\true \or A \iff \true

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)