Theorem trueimp_eqv_self ≪ | index | src | ≫

\true\imp等价自身

theorem trueimp_eqv_self (A: wff): $ \true \imp A \iff A $;
StepHypRefExpression
1 iff_comp 
((\true \imp A) \imp A) \imp (A \imp \true \imp A) \imp (\true \imp A \iff A)
2 _hyp_null_intro 
(\true \imp A) \imp \true \imp A
3 true_proof 
\true
4 3 _hyp_null_complete 
(\true \imp A) \imp \true
5 2, 4 _hyp_mp 
(\true \imp A) \imp A
6 1, 5 ax_mp 
(A \imp \true \imp A) \imp (\true \imp A \iff A)
7 introl_imp 
A \imp \true \imp A
8 6, 7 ax_mp 
\true \imp A \iff A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)