Theorem biimt 350

Description: A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996.)

Assertion

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

Proof of Theorem biimt

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 |- ( ps -> ( ph -> ps ) )
2		pm2.27 42	. 2 |- ( ph -> ( ( ph -> ps ) -> ps ) )
3	1, 2	impbid2 216	1 |- ( ph -> ( ps <-> ( ph -> ps ) ) )

Syntax hints:   -> wi 4   <-> wb 196

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

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  pm5.5  351  a1bi  352  mtt  354  abai  836  dedlem0a  1000  ifptru  1023  ceqsralt  3229  reu8  3402  csbiebt  3553  r19.3rz  4062  ralidm  4075  notzfaus  4840  reusv2lem5  4873  fncnv  5962  ovmpt2dxf  6786  brecop  7840  kmlem8  8979  kmlem13  8984  fin71num  9219  ttukeylem6  9336  ltxrlt  10108  rlimresb  14296  acsfn  16320  tgss2  20791  ist1-3  21153  mbflimsup  23433  mdegle0  23837  dchrelbas3  24963  tgcgr4  25426  cdleme32fva  35725  ntrneik2  38390  ntrneix2  38391  ntrneikb  38392  ovmpt2rdxf  42117