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  1043  ifptru  1074  norasslem2  1536  ceqsralt  3471  clel2g  3614  clel4g  3618  reu8  3692  csbiebt  3879  r19.3rz  4447  reusv2lem5  5340  fncnv  6554  ovmpodxf  7496  brecop  8734  kmlem8  10046  kmlem13  10051  fin71num  10285  ttukeylem6  10402  ltxrlt  11180  rlimresb  15469  acsfn  17562  tgss2  22900  ist1-3  23262  mbflimsup  25592  mdegle0  26007  dchrelbas3  27174  tgcgr4  28507  wl-clabtv  37630  wl-clabt  37631  cdleme32fva  40475  ntrneik2  44124  ntrneix2  44125  ntrneikb  44126  r19.3rzf  45194  ovmpordxf  48369  fulltermc  49542