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  3464  clel2g  3601  clel4g  3605  reu8  3679  csbiebt  3866  r19.3rz  4441  reusv2lem5  5344  fncnv  6571  ovmpodxf  7517  brecop  8757  kmlem8  10080  kmlem13  10085  fin71num  10319  ttukeylem6  10436  ltxrlt  11216  rlimresb  15527  acsfn  17625  tgss2  22952  ist1-3  23314  mbflimsup  25633  mdegle0  26042  dchrelbas3  27201  tgcgr4  28599  mh-infprim1bi  36728  wl-clabtv  37911  wl-clabt  37912  cdleme32fva  40883  ntrneik2  44519  ntrneix2  44520  ntrneikb  44521  r19.3rzf  45588  ovmpordxf  48815  fulltermc  49986