Theorem biimt 360

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  pm5.5  361  a1bi  362  mtt  364  abai  827  dedlem0a  1044  ifptru  1075  norasslem2  1537  ceqsralt  3465  clel2g  3602  clel4g  3606  reu8  3680  csbiebt  3867  r19.3rz  4442  reusv2lem5  5339  fncnv  6565  ovmpodxf  7510  brecop  8750  kmlem8  10071  kmlem13  10076  fin71num  10310  ttukeylem6  10427  ltxrlt  11207  rlimresb  15518  acsfn  17616  tgss2  22962  ist1-3  23324  mbflimsup  25643  mdegle0  26052  dchrelbas3  27215  tgcgr4  28613  mh-infprim1bi  36744  wl-clabtv  37925  wl-clabt  37926  cdleme32fva  40897  ntrneik2  44537  ntrneix2  44538  ntrneikb  44539  r19.3rzf  45606  ovmpordxf  48827  fulltermc  49998