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  3492  clel2g  3621  clel4g  3625  reu8  3699  csbiebt  3885  r19.3rz  4467  reusv2lem5  5378  fncnv  6616  ovmpodxf  7573  brecop  8817  kmlem8  10160  kmlem13  10165  fin71num  10399  ttukeylem6  10516  ltxrlt  11298  rlimresb  15642  acsfn  17740  tgss2  23181  ist1-3  23543  mbflimsup  25862  mdegle0  26271  dchrelbas3  27439  tgcgr4  28837  mh-infprim1bi  37098  wl-clabtv  38282  wl-clabt  38283  cdleme32fva  41252  ntrneik2  44859  ntrneix2  44860  ntrneikb  44861  r19.3rzf  45917  ovmpordxf  49160  fulltermc  50330