Theorem biimt 350

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  351  a1bi  352  mtt  354  abai  835  dedlem0a  999  ifptru  1022  ceqsralt  3219  reu8  3389  csbiebt  3539  r19.3rz  4040  ralidm  4053  notzfaus  4810  reusv2lem5  4843  fncnv  5930  ovmpt2dxf  6751  brecop  7800  kmlem8  8939  kmlem13  8944  fin71num  9179  ttukeylem6  9296  ltxrlt  10068  rlimresb  14246  acsfn  16260  tgss2  20731  ist1-3  21093  mbflimsup  23373  mdegle0  23775  dchrelbas3  24897  tgcgr4  25360  cdleme32fva  35244  ntrneik2  37911  ntrneix2  37912  ntrneikb  37913  ovmpt2rdxf  41435