Theorem biimt 729

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 516	1 |- (ph -> (ps <-> (ph -> ps)))

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

This theorem is referenced by:  pm5.5 730  biorf 733  reu8 1926  sbc5g 1944  sbc6g 1945  elrabsf 1953  r19.3rzv 2338  ralidm 2347  notzfaus 2731  fncnv 3547  brecop 4290  kmlem8 4744  kmlem13 4749  cvg2 6859  caucvg 7099  metcnplem 7825  r19.3rzvb 10337

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