Theorem pm5.74d 276

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  imbi2d  344  imim21b  398  pm5.74da  804  sbiedvw  2100  sbiedw  2314  sbiedwOLD  2315  cbval2vOLD  2344  dvelimdf  2448  sbied  2506  2mos  2650  cbvraldva2  3367  csbie2df  4355  dfiin2g  4941  oneqmini  6264  tfindsg  7639  findsg  7677  brecop  8492  dom2lem  8668  indpi  10521  nn0ind-raph  12277  cncls2  22170  ismbl2  24424  voliunlem3  24449  mdbr2  30377  dmdbr2  30384  mdsl2i  30403  mdsl2bi  30404  sgn3da  32220  wl-dral1d  35427  wl-equsald  35435  cvlsupr3  37095  cdleme32fva  38188  cdlemk33N  38660  cdlemk34  38661  ralbidar  41736  logic1  45809  tfis2d  46057