Theorem pm5.74d 275

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  imbi2d  343  imim21b  397  pm5.74da  802  sbiedvw  2100  sbiedw  2328  sbiedwOLD  2329  cbval2vOLD  2360  cbval2OLD  2429  dvelimdf  2467  sbied  2541  sbiedALT  2610  2mos  2730  cbvraldva2  3456  cbvrexdva2OLD  3458  csbie2df  4391  dfiin2g  4949  oneqmini  6236  tfindsg  7569  findsg  7603  brecop  8384  dom2lem  8543  indpi  10323  nn0ind-raph  12076  cncls2  21875  ismbl2  24122  voliunlem3  24147  mdbr2  30067  dmdbr2  30074  mdsl2i  30093  mdsl2bi  30094  sgn3da  31794  wl-dral1d  34765  wl-equsald  34773  cvlsupr3  36474  cdleme32fva  37567  cdlemk33N  38039  cdlemk34  38040  ralbidar  40770  tfis2d  44777