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  3482  clel2g  3625  clel4g  3629  reu8  3704  csbiebt  3891  r19.3rz  4460  reusv2lem5  5357  fncnv  6589  ovmpodxf  7539  brecop  8783  kmlem8  10111  kmlem13  10116  fin71num  10350  ttukeylem6  10467  ltxrlt  11244  rlimresb  15531  acsfn  17620  tgss2  22874  ist1-3  23236  mbflimsup  25567  mdegle0  25982  dchrelbas3  27149  tgcgr4  28458  wl-clabtv  37585  wl-clabt  37586  cdleme32fva  40431  ntrneik2  44081  ntrneix2  44082  ntrneikb  44083  r19.3rzf  45152  ovmpordxf  48327  fulltermc  49500