Theorem biimt 363

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 43	. 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  364  a1bi  365  mtt  367  abai  838  dedlem0a  1059  ifptru  1091  norasslem2  1565  ceqsralt  3489  clel2g  3619  clel4g  3623  reu8  3697  csbiebt  3883  r19.3rz  4463  reusv2lem5  5375  fncnv  6611  ovmpodxf  7562  brecop  8809  kmlem8  10142  kmlem13  10147  fin71num  10382  ttukeylem6  10499  ltxrlt  11281  rlimresb  15618  acsfn  17716  tgss2  23125  ist1-3  23487  mbflimsup  25806  mdegle0  26215  dchrelbas3  27383  tgcgr4  28781  mh-infprim1bi  37038  wl-clabtv  38222  wl-clabt  38223  cdleme32fva  41192  ntrneik2  44801  ntrneix2  44802  ntrneikb  44803  r19.3rzf  45859  ovmpordxf  49102  fulltermc  50272