Theorem biimt 362

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 228	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  pm5.5  363  a1bi  364  mtt  366  abai  836  dedlem0a  1054  ifptru  1085  norasslem2  1554  ceqsralt  3487  clel2g  3618  clel4g  3622  reu8  3695  csbiebt  3881  r19.3rz  4454  reusv2lem5  5358  fncnv  6590  ovmpodxf  7542  brecop  8787  kmlem8  10111  kmlem13  10116  fin71num  10351  ttukeylem6  10468  ltxrlt  11250  rlimresb  15575  acsfn  17674  tgss2  23027  ist1-3  23389  mbflimsup  25708  mdegle0  26117  dchrelbas3  27279  tgcgr4  28677  mh-infprim1bi  36870  wl-clabtv  38053  wl-clabt  38054  cdleme32fva  41025  ntrneik2  44632  ntrneix2  44633  ntrneikb  44634  r19.3rzf  45700  ovmpordxf  48925  fulltermc  50096