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  1044  ifptru  1075  norasslem2  1535  ceqsralt  3516  clel2g  3659  clel4g  3663  reu8  3739  csbiebt  3928  r19.3rz  4497  reusv2lem5  5402  fncnv  6639  ovmpodxf  7583  brecop  8850  kmlem8  10198  kmlem13  10203  fin71num  10437  ttukeylem6  10554  ltxrlt  11331  rlimresb  15601  acsfn  17702  tgss2  22994  ist1-3  23357  mbflimsup  25701  mdegle0  26116  dchrelbas3  27282  tgcgr4  28539  wl-clabtv  37598  wl-clabt  37599  cdleme32fva  40439  ntrneik2  44105  ntrneix2  44106  ntrneikb  44107  r19.3rzf  45163  ovmpordxf  48255  fulltermc  49143