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 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  361  a1bi  362  mtt  364  abai  825  dedlem0a  1042  ifptru  1074  norasslem2  1536  ceqsralt  3506  clel2g  3646  clel4g  3651  reu8  3728  csbiebt  3922  r19.3rz  4495  ralidmOLD  4514  reusv2lem5  5399  fncnv  6618  ovmpodxf  7554  brecop  8800  kmlem8  10148  kmlem13  10153  fin71num  10388  ttukeylem6  10505  ltxrlt  11280  rlimresb  15505  acsfn  17599  tgss2  22481  ist1-3  22844  mbflimsup  25174  mdegle0  25586  dchrelbas3  26730  tgcgr4  27771  wl-clabtv  36447  wl-clabt  36448  cdleme32fva  39296  ntrneik2  42828  ntrneix2  42829  ntrneikb  42830  r19.3rzf  43837  ovmpordxf  46967