Theorem biimt 803

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 76	. 2 |- (ph -> ((ph -> ps) -> ps))
3	1, 2	impbid2 576	1 |- (ph -> (ps <-> (ph -> ps)))

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

This theorem is referenced by:  pm5.5 804  biorf 807  reu8 2448  sbc5gOLD 2471  sbc6gOLD 2473  elrabsf 2486  r19.3rz 2960  r19.3rzv 2962  ralidm 2973  notzfaus 3478  fncnv 4479  brecop 5365  kmlem8 5934  kmlem13 5939  cvg2i 8174  caucvgi 8423  metcnplem 9164  r19.3rzvb 14273

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 164  df-an 242

Copyright terms: Public domain