Theorem biimt 359

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 225	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  pm5.5  360  a1bi  361  mtt  363  abai  825  dedlem0a  1041  ifptru  1072  norasslem2  1528  ceqsralt  3497  clel2g  3643  clel4g  3648  reu8  3726  csbiebt  3920  r19.3rz  4497  ralidmOLD  4516  reusv2lem5  5401  fncnv  6625  ovmpodxf  7569  brecop  8827  kmlem8  10180  kmlem13  10185  fin71num  10420  ttukeylem6  10537  ltxrlt  11314  rlimresb  15541  acsfn  17638  tgss2  22920  ist1-3  23283  mbflimsup  25625  mdegle0  26043  dchrelbas3  27201  tgcgr4  28391  wl-clabtv  37134  wl-clabt  37135  cdleme32fva  39979  ntrneik2  43587  ntrneix2  43588  ntrneikb  43589  r19.3rzf  44593  ovmpordxf  47514