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  2101  sbiedw  2322  dvelimdf  2454  sbied  2508  2mosOLD  2651  cbvraldva2  3320  csbie2df  4397  dfiin2g  4988  oneqmini  6378  tfindsg  7813  findsg  7849  brecop  8759  dom2lem  8941  indpi  10830  nn0ind-raph  12604  cncls2  23229  ismbl2  25496  voliunlem3  25521  mdbr2  32383  dmdbr2  32390  mdsl2i  32409  mdsl2bi  32410  sgn3da  32925  wl-dral1d  37780  wl-equsald  37788  wl-equsaldv  37789  cvlsupr3  39714  cdleme32fva  40807  cdlemk33N  41279  cdlemk34  41280  ralbidar  44794  logic1  49144  tfis2d  50033