Theorem biimt 360

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

Assertion

Ref	Expression
biimt	⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))

Proof of Theorem biimt

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 ⊢ (𝜓 → (𝜑 → 𝜓))
2		pm2.27 42	. 2 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
3	1, 2	impbid2 226	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  pm5.5  361  a1bi  362  mtt  364  abai  827  dedlem0a  1043  ifptru  1074  norasslem2  1531  ceqsralt  3513  clel2g  3658  clel4g  3662  reu8  3741  csbiebt  3937  r19.3rz  4502  reusv2lem5  5407  fncnv  6640  ovmpodxf  7582  brecop  8848  kmlem8  10195  kmlem13  10200  fin71num  10434  ttukeylem6  10551  ltxrlt  11328  rlimresb  15597  acsfn  17703  tgss2  23009  ist1-3  23372  mbflimsup  25714  mdegle0  26130  dchrelbas3  27296  tgcgr4  28553  wl-clabtv  37577  wl-clabt  37578  cdleme32fva  40419  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  r19.3rzf  45100  ovmpordxf  48183