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  826  dedlem0a  1043  ifptru  1075  norasslem2  1537  ceqsralt  3507  clel2g  3648  clel4g  3653  reu8  3730  csbiebt  3924  r19.3rz  4497  ralidmOLD  4516  reusv2lem5  5401  fncnv  6622  ovmpodxf  7558  brecop  8804  kmlem8  10152  kmlem13  10157  fin71num  10392  ttukeylem6  10509  ltxrlt  11284  rlimresb  15509  acsfn  17603  tgss2  22490  ist1-3  22853  mbflimsup  25183  mdegle0  25595  dchrelbas3  26741  tgcgr4  27782  wl-clabtv  36459  wl-clabt  36460  cdleme32fva  39308  ntrneik2  42843  ntrneix2  42844  ntrneikb  42845  r19.3rzf  43852  ovmpordxf  47014