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  803  sbiedvw  2096  sbiedw  2315  dvelimdf  2447  sbied  2501  2mosOLD  2643  cbvraldva2  3311  csbie2df  4390  dfiin2g  4978  oneqmini  6354  tfindsg  7785  findsg  7821  brecop  8728  dom2lem  8908  indpi  10789  nn0ind-raph  12564  cncls2  23142  ismbl2  25409  voliunlem3  25434  mdbr2  32227  dmdbr2  32234  mdsl2i  32253  mdsl2bi  32254  sgn3da  32772  wl-dral1d  37522  wl-equsald  37530  wl-equsaldv  37531  cvlsupr3  39340  cdleme32fva  40433  cdlemk33N  40905  cdlemk34  40906  ralbidar  44434  logic1  48789  tfis2d  49679