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  3487  clel2g  3616  clel4g  3620  reu8  3694  csbiebt  3879  r19.3rz  4460  reusv2lem5  5371  fncnv  6610  ovmpodxf  7567  brecop  8814  kmlem8  10164  kmlem13  10169  fin71num  10403  ttukeylem6  10520  ltxrlt  11308  rlimresb  15656  acsfn  17753  tgss2  23218  ist1-3  23580  mbflimsup  25900  mdegle0  26309  dchrelbas3  27482  tgcgr4  28881  mh-infprim1bi  37173  wl-clabtv  38357  wl-clabt  38358  cdleme32fva  41318  ntrneik2  44940  ntrneix2  44941  ntrneikb  44942  r19.3rzf  45998  ovmpordxf  49277  fulltermc  50445