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 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  361  a1bi  362  mtt  364  abai  823  dedlem0a  1040  ifptru  1072  norasslem2  1533  ceqsralt  3453  clel2g  3581  clel4g  3586  reu8  3663  csbiebt  3858  r19.3rz  4424  ralidmOLD  4443  reusv2lem5  5320  fncnv  6491  ovmpodxf  7401  brecop  8557  kmlem8  9844  kmlem13  9849  fin71num  10084  ttukeylem6  10201  ltxrlt  10976  rlimresb  15202  acsfn  17285  tgss2  22045  ist1-3  22408  mbflimsup  24735  mdegle0  25147  dchrelbas3  26291  tgcgr4  26796  wl-clabtv  35675  wl-clabt  35676  cdleme32fva  38378  ntrneik2  41591  ntrneix2  41592  ntrneikb  41593  ovmpordxf  45562