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  2448  sbied  2502  2mosOLD  2644  cbvraldva2  3323  csbie2df  4409  dfiin2g  4999  oneqmini  6388  tfindsg  7840  findsg  7876  brecop  8786  dom2lem  8966  indpi  10867  nn0ind-raph  12641  cncls2  23167  ismbl2  25435  voliunlem3  25460  mdbr2  32232  dmdbr2  32239  mdsl2i  32258  mdsl2bi  32259  sgn3da  32766  wl-dral1d  37526  wl-equsald  37534  wl-equsaldv  37535  cvlsupr3  39344  cdleme32fva  40438  cdlemk33N  40910  cdlemk34  40911  ralbidar  44441  logic1  48783  tfis2d  49673