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  826  dedlem0a  1044  ifptru  1075  norasslem2  1532  ceqsralt  3524  clel2g  3672  clel4g  3676  reu8  3755  csbiebt  3951  r19.3rz  4520  reusv2lem5  5420  fncnv  6651  ovmpodxf  7600  brecop  8868  kmlem8  10227  kmlem13  10232  fin71num  10466  ttukeylem6  10583  ltxrlt  11360  rlimresb  15611  acsfn  17717  tgss2  23015  ist1-3  23378  mbflimsup  25720  mdegle0  26136  dchrelbas3  27300  tgcgr4  28557  wl-clabtv  37551  wl-clabt  37552  cdleme32fva  40394  ntrneik2  44054  ntrneix2  44055  ntrneikb  44056  r19.3rzf  45063  ovmpordxf  48063