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  3477  clel2g  3615  clel4g  3619  reu8  3693  csbiebt  3880  r19.3rz  4456  reusv2lem5  5349  fncnv  6573  ovmpodxf  7518  brecop  8759  kmlem8  10080  kmlem13  10085  fin71num  10319  ttukeylem6  10436  ltxrlt  11215  rlimresb  15500  acsfn  17594  tgss2  22943  ist1-3  23305  mbflimsup  25635  mdegle0  26050  dchrelbas3  27217  tgcgr4  28615  wl-clabtv  37835  wl-clabt  37836  cdleme32fva  40807  ntrneik2  44442  ntrneix2  44443  ntrneikb  44444  r19.3rzf  45511  ovmpordxf  48693  fulltermc  49864