Theorem pm5.74d 272

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  imbi2d  340  imim21b  395  pm5.74da  802  sbiedvw  2096  sbiedw  2309  dvelimdf  2448  sbied  2502  2mos  2645  cbvraldva2  3344  csbie2df  4439  dfiin2g  5034  oneqmini  6413  tfindsg  7846  findsg  7886  brecop  8800  dom2lem  8984  indpi  10898  nn0ind-raph  12658  cncls2  22768  ismbl2  25035  voliunlem3  25060  mdbr2  31536  dmdbr2  31543  mdsl2i  31562  mdsl2bi  31563  sgn3da  33528  wl-dral1d  36388  wl-equsald  36396  cvlsupr3  38202  cdleme32fva  39296  cdlemk33N  39768  cdlemk34  39769  ralbidar  43189  logic1  47429  tfis2d  47678