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  1535  ceqsralt  3485  clel2g  3628  clel4g  3632  reu8  3707  csbiebt  3894  r19.3rz  4463  reusv2lem5  5360  fncnv  6592  ovmpodxf  7542  brecop  8786  kmlem8  10118  kmlem13  10123  fin71num  10357  ttukeylem6  10474  ltxrlt  11251  rlimresb  15538  acsfn  17627  tgss2  22881  ist1-3  23243  mbflimsup  25574  mdegle0  25989  dchrelbas3  27156  tgcgr4  28465  wl-clabtv  37592  wl-clabt  37593  cdleme32fva  40438  ntrneik2  44088  ntrneix2  44089  ntrneikb  44090  r19.3rzf  45159  ovmpordxf  48331  fulltermc  49504