Theorem biimt 363

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 43	. 2 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
3	1, 2	impbid2 229	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.5  364  a1bi  365  mtt  367  abai  839  dedlem0a  1059  ifptru  1091  norasslem2  1564  ceqsralt  3484  clel2g  3612  clel4g  3616  reu8  3690  csbiebt  3875  r19.3rz  4456  reusv2lem5  5363  fncnv  6614  ovmpodxf  7571  brecop  8835  kmlem8  10240  kmlem13  10245  fin71num  10479  ttukeylem6  10596  ltxrlt  11384  rlimresb  15738  acsfn  17839  tgss2  23311  ist1-3  23673  mbflimsup  25993  mdegle0  26401  dchrelbas3  27571  tgcgr4  29000  mh-infprim1bi  37427  wl-clabtv  38612  wl-clabt  38613  cdleme32fva  41588  ntrneik2  45186  ntrneix2  45187  ntrneikb  45188  r19.3rzf  46267  ovmpordxf  49545  fulltermc  50740