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  3472  clel2g  3610  clel4g  3614  reu8  3688  csbiebt  3875  r19.3rz  4446  reusv2lem5  5342  fncnv  6559  ovmpodxf  7502  brecop  8740  kmlem8  10056  kmlem13  10061  fin71num  10295  ttukeylem6  10412  ltxrlt  11190  rlimresb  15474  acsfn  17567  tgss2  22903  ist1-3  23265  mbflimsup  25595  mdegle0  26010  dchrelbas3  27177  tgcgr4  28510  wl-clabtv  37651  wl-clabt  37652  cdleme32fva  40556  ntrneik2  44209  ntrneix2  44210  ntrneikb  44211  r19.3rzf  45279  ovmpordxf  48463  fulltermc  49636