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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  pm5.5  361  a1bi  362  mtt  364  abai  826  dedlem0a  1042  ifptru  1073  norasslem2  1529  ceqsralt  3504  clel2g  3645  clel4g  3650  reu8  3728  csbiebt  3922  r19.3rz  4497  ralidmOLD  4516  reusv2lem5  5402  fncnv  6626  ovmpodxf  7571  brecop  8829  kmlem8  10181  kmlem13  10186  fin71num  10421  ttukeylem6  10538  ltxrlt  11315  rlimresb  15542  acsfn  17639  tgss2  22903  ist1-3  23266  mbflimsup  25608  mdegle0  26026  dchrelbas3  27184  tgcgr4  28348  wl-clabtv  37064  wl-clabt  37065  cdleme32fva  39910  ntrneik2  43522  ntrneix2  43523  ntrneikb  43524  r19.3rzf  44529  ovmpordxf  47402