Theorem biimt 359

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  360  a1bi  361  mtt  363  abai  823  dedlem0a  1040  ifptru  1072  norasslem2  1534  ceqsralt  3505  clel2g  3648  clel4g  3653  reu8  3730  csbiebt  3924  r19.3rz  4497  ralidmOLD  4516  reusv2lem5  5401  fncnv  6622  ovmpodxf  7562  brecop  8808  kmlem8  10156  kmlem13  10161  fin71num  10396  ttukeylem6  10513  ltxrlt  11290  rlimresb  15515  acsfn  17609  tgss2  22712  ist1-3  23075  mbflimsup  25417  mdegle0  25829  dchrelbas3  26975  tgcgr4  28047  wl-clabtv  36764  wl-clabt  36765  cdleme32fva  39613  ntrneik2  43147  ntrneix2  43148  ntrneikb  43149  r19.3rzf  44155  ovmpordxf  47104