Theorem pm5.74d 276

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 21-Mar-1996.)

Hypothesis

Ref	Expression
pm5.74d.1	⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))

Assertion

Ref	Expression
pm5.74d	⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

Proof of Theorem pm5.74d

Step	Hyp	Ref	Expression
1		pm5.74d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
2		pm5.74 273	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))
3	1, 2	sylib 221	1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  imbi2d  343  imim21b  400  pm5.74da  816  sbiedvw  2131  sbiedw  2346  dvelimdf  2478  sbied  2532  csbie2df  4400  dfiin2g  4988  oneqmini  6416  tfindsg  7872  findsg  7909  brecop  8834  dom2lem  9022  indpi  10995  nn0ind-raph  12802  sgn3da  15259  cncls2  23596  ismbl2  25853  voliunlem3  25878  mdbr2  32903  dmdbr2  32910  mdsl2i  32929  mdsl2bi  32930  wl-dral1d  38556  wl-equsald  38564  wl-equsaldv  38565  cvlsupr3  40494  cdleme32fva  41587  cdlemk33N  42059  cdlemk34  42060  ralbidar  45521  imbi12d2  49994  tfis2d  50955