Theorem biimt 364

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

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  pm5.5  365  a1bi  366  mtt  368  abai  825  dedlem0a  1039  ifptru  1071  norasslem2  1532  ceqsralt  3475  reu8  3672  csbiebt  3857  r19.3rz  4400  ralidm  4413  notzfausOLD  5228  reusv2lem5  5268  fncnv  6397  ovmpodxf  7279  brecop  8373  kmlem8  9568  kmlem13  9573  fin71num  9808  ttukeylem6  9925  ltxrlt  10700  rlimresb  14914  acsfn  16922  tgss2  21592  ist1-3  21954  mbflimsup  24270  mdegle0  24678  dchrelbas3  25822  tgcgr4  26325  wl-clabtv  34994  wl-clabt  34995  cdleme32fva  37733  ntrneik2  40795  ntrneix2  40796  ntrneikb  40797  ovmpordxf  44740