Theorem biimt 361

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  362  a1bi  363  mtt  365  abai  824  dedlem0a  1041  ifptru  1073  norasslem2  1533  ceqsralt  3464  clel2g  3589  clel4g  3594  reu8  3669  csbiebt  3863  r19.3rz  4428  ralidmOLD  4447  reusv2lem5  5326  fncnv  6514  ovmpodxf  7432  brecop  8608  kmlem8  9922  kmlem13  9927  fin71num  10162  ttukeylem6  10279  ltxrlt  11054  rlimresb  15283  acsfn  17377  tgss2  22146  ist1-3  22509  mbflimsup  24839  mdegle0  25251  dchrelbas3  26395  tgcgr4  26901  wl-clabtv  35757  wl-clabt  35758  cdleme32fva  38458  ntrneik2  41709  ntrneix2  41710  ntrneikb  41711  ovmpordxf  45685