Theorem pm5.74d 273

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 270	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))
3	1, 2	sylib 218	1 ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  imbi2d  340  imim21b  394  pm5.74da  804  sbiedvw  2095  sbiedw  2316  dvelimdf  2454  sbied  2508  2mosOLD  2650  cbvraldva2  3348  csbie2df  4443  dfiin2g  5032  oneqmini  6436  tfindsg  7882  findsg  7919  brecop  8850  dom2lem  9032  indpi  10947  nn0ind-raph  12718  cncls2  23281  ismbl2  25562  voliunlem3  25587  mdbr2  32315  dmdbr2  32322  mdsl2i  32341  mdsl2bi  32342  sgn3da  34544  wl-dral1d  37532  wl-equsald  37540  wl-equsaldv  37541  cvlsupr3  39345  cdleme32fva  40439  cdlemk33N  40911  cdlemk34  40912  ralbidar  44464  logic1  48711  tfis2d  49199