Theorem biimt 365

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 229	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  pm5.5  366  a1bi  367  mtt  369  abai  826  dedlem0a  1040  ifptru  1072  norasslem2  1533  ceqsralt  3445  clel2g  3571  clel4g  3576  reu8  3648  csbiebt  3835  r19.3rz  4391  ralidmOLD  4409  notzfausOLD  5232  reusv2lem5  5272  fncnv  6409  ovmpodxf  7296  brecop  8401  kmlem8  9610  kmlem13  9615  fin71num  9850  ttukeylem6  9967  ltxrlt  10742  rlimresb  14963  acsfn  16981  tgss2  21680  ist1-3  22042  mbflimsup  24359  mdegle0  24770  dchrelbas3  25914  tgcgr4  26417  wl-clabtv  35267  wl-clabt  35268  cdleme32fva  38006  ntrneik2  41161  ntrneix2  41162  ntrneikb  41163  ovmpordxf  45100