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 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

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:  imbi2d  343  imim21b  399  pm5.74da  815  sbiedvw  2130  sbiedw  2349  dvelimdf  2481  sbied  2535  csbie2df  4409  dfiin2g  4996  oneqmini  6416  tfindsg  7858  findsg  7895  brecop  8809  dom2lem  8990  indpi  10893  nn0ind-raph  12697  sgn3da  15140  cncls2  23411  ismbl2  25667  voliunlem3  25692  mdbr2  32629  dmdbr2  32636  mdsl2i  32655  mdsl2bi  32656  wl-dral1d  38167  wl-equsald  38175  wl-equsaldv  38176  cvlsupr3  40099  cdleme32fva  41192  cdlemk33N  41664  cdlemk34  41665  ralbidar  45137  logic1  49552  tfis2d  50441