Theorem biimt 730

Description: A wff is equivalent to itself with true antecedent.

Assertion

Ref	Expression
biimt	|- (ph -> (ps <-> (ph -> ps)))

Proof of Theorem biimt

Step	Hyp	Ref	Expression
1		ax-1 4	. 2 |- (ps -> (ph -> ps))
2		pm2.27 62	. 2 |- (ph -> ((ph -> ps) -> ps))
3	1, 2	impbid2 517	1 |- (ph -> (ps <-> (ph -> ps)))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  pm5.5 731  biorf 734  reu8 1932  sbc5g 1950  sbc6g 1951  elrabsf 1959  r19.3rzv 2344  ralidm 2353  notzfaus 2736  fncnv 3553  brecop 4296  kmlem8 4752  kmlem13 4757  cvg2 6867  caucvg 7107  metcnplem 7838  r19.3rzvb 10373

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain