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 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))

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  364  a1bi  365  mtt  367  abai  838  dedlem0a  1057  ifptru  1089  norasslem2  1558  ceqsralt  3491  clel2g  3621  clel4g  3625  reu8  3699  csbiebt  3884  r19.3rz  4458  reusv2lem5  5364  fncnv  6598  ovmpodxf  7550  brecop  8796  kmlem8  10129  kmlem13  10134  fin71num  10369  ttukeylem6  10486  ltxrlt  11268  rlimresb  15606  acsfn  17705  tgss2  23105  ist1-3  23467  mbflimsup  25786  mdegle0  26195  dchrelbas3  27360  tgcgr4  28758  mh-infprim1bi  36919  wl-clabtv  38101  wl-clabt  38102  cdleme32fva  41073  ntrneik2  44680  ntrneix2  44681  ntrneikb  44682  r19.3rzf  45734  ovmpordxf  48970  fulltermc  50140