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  1536  ceqsralt  3475  clel2g  3613  clel4g  3617  reu8  3691  csbiebt  3878  r19.3rz  4454  reusv2lem5  5347  fncnv  6565  ovmpodxf  7508  brecop  8747  kmlem8  10068  kmlem13  10073  fin71num  10307  ttukeylem6  10424  ltxrlt  11203  rlimresb  15488  acsfn  17582  tgss2  22931  ist1-3  23293  mbflimsup  25623  mdegle0  26038  dchrelbas3  27205  tgcgr4  28603  wl-clabtv  37787  wl-clabt  37788  cdleme32fva  40693  ntrneik2  44329  ntrneix2  44330  ntrneikb  44331  r19.3rzf  45398  ovmpordxf  48581  fulltermc  49752