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  3485  clel2g  3613  clel4g  3617  reu8  3691  csbiebt  3876  r19.3rz  4457  reusv2lem5  5364  fncnv  6605  ovmpodxf  7562  brecop  8815  kmlem8  10217  kmlem13  10222  fin71num  10456  ttukeylem6  10573  ltxrlt  11361  rlimresb  15712  acsfn  17813  tgss2  23285  ist1-3  23647  mbflimsup  25967  mdegle0  26375  dchrelbas3  27547  tgcgr4  28976  mh-infprim1bi  37304  wl-clabtv  38486  wl-clabt  38487  cdleme32fva  41462  ntrneik2  45051  ntrneix2  45052  ntrneikb  45053  r19.3rzf  46116  ovmpordxf  49395  fulltermc  50563