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  1565  ceqsralt  3488  clel2g  3616  clel4g  3620  reu8  3694  csbiebt  3880  r19.3rz  4460  reusv2lem5  5369  fncnv  6638  ovmpodxf  7597  brecop  8862  kmlem8  10266  kmlem13  10271  fin71num  10505  ttukeylem6  10622  ltxrlt  11410  rlimresb  15764  acsfn  17865  tgss2  23338  ist1-3  23700  mbflimsup  26020  mdegle0  26428  dchrelbas3  27598  tgcgr4  29027  mh-infprim1bi  37525  wl-clabtv  38723  wl-clabt  38724  cdleme32fva  41697  ntrneik2  45295  ntrneix2  45296  ntrneikb  45297  r19.3rzf  46388  ovmpordxf  49666  fulltermc  50861