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  2321  dvelimdf  2453  sbied  2507  2mosOLD  2650  csbie2df  4383  dfiin2g  4973  oneqmini  6376  tfindsg  7812  findsg  7848  brecop  8757  dom2lem  8939  indpi  10830  nn0ind-raph  12629  cncls2  23238  ismbl2  25494  voliunlem3  25519  mdbr2  32367  dmdbr2  32374  mdsl2i  32393  mdsl2bi  32394  sgn3da  32907  wl-dral1d  37856  wl-equsald  37864  wl-equsaldv  37865  cvlsupr3  39790  cdleme32fva  40883  cdlemk33N  41355  cdlemk34  41356  ralbidar  44871  logic1  49266  tfis2d  50155