Theorem biimt 349

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  pm5.5  350  a1bi  351  mtt  353  abai  871  dedlem0a  1030  ifptru  1061  ceqsralt  3370  reu8  3544  csbiebt  3695  r19.3rz  4207  ralidm  4220  notzfaus  4990  reusv2lem5  5023  fncnv  6124  ovmpt2dxf  6953  brecop  8010  kmlem8  9192  kmlem13  9197  fin71num  9432  ttukeylem6  9549  ltxrlt  10321  rlimresb  14516  acsfn  16542  tgss2  21014  ist1-3  21376  mbflimsup  23653  mdegle0  24057  dchrelbas3  25184  tgcgr4  25647  cdleme32fva  36246  ntrneik2  38911  ntrneix2  38912  ntrneikb  38913  ovmpt2rdxf  42646