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  826  dedlem0a  1043  ifptru  1074  norasslem2  1535  ceqsralt  3495  clel2g  3638  clel4g  3642  reu8  3716  csbiebt  3903  r19.3rz  4472  reusv2lem5  5372  fncnv  6609  ovmpodxf  7557  brecop  8824  kmlem8  10172  kmlem13  10177  fin71num  10411  ttukeylem6  10528  ltxrlt  11305  rlimresb  15581  acsfn  17671  tgss2  22925  ist1-3  23287  mbflimsup  25619  mdegle0  26034  dchrelbas3  27201  tgcgr4  28510  wl-clabtv  37615  wl-clabt  37616  cdleme32fva  40456  ntrneik2  44116  ntrneix2  44117  ntrneikb  44118  r19.3rzf  45182  ovmpordxf  48314  fulltermc  49396