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  3321  csbie2df  4406  dfiin2g  4996  oneqmini  6385  tfindsg  7837  findsg  7873  brecop  8783  dom2lem  8963  indpi  10860  nn0ind-raph  12634  cncls2  23160  ismbl2  25428  voliunlem3  25453  mdbr2  32225  dmdbr2  32232  mdsl2i  32251  mdsl2bi  32252  sgn3da  32759  wl-dral1d  37519  wl-equsald  37527  wl-equsaldv  37528  cvlsupr3  39337  cdleme32fva  40431  cdlemk33N  40903  cdlemk34  40904  ralbidar  44434  logic1  48779  tfis2d  49669