Theorem pm5.74d 274

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  imbi2d  341  imim21b  395  pm5.74da  809  sbiedvw  2106  sbiedw  2325  dvelimdf  2457  sbied  2511  2mosOLD  2654  csbie2df  4378  dfiin2g  4967  oneqmini  6370  tfindsg  7808  findsg  7844  brecop  8754  dom2lem  8936  indpi  10828  nn0ind-raph  12627  cncls2  23263  ismbl2  25519  voliunlem3  25544  mdbr2  32392  dmdbr2  32399  mdsl2i  32418  mdsl2bi  32419  sgn3da  32933  wl-dral1d  37909  wl-equsald  37917  wl-equsaldv  37918  cvlsupr3  39843  cdleme32fva  40936  cdlemk33N  41408  cdlemk34  41409  ralbidar  44895  logic1  49288  tfis2d  50177