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  394  pm5.74da  800  sbiedvw  2098  sbiedw  2313  sbiedwOLD  2314  cbval2vOLD  2343  dvelimdf  2449  sbied  2507  2mos  2651  cbvraldva2  3381  csbie2df  4371  dfiin2g  4958  oneqmini  6302  tfindsg  7682  findsg  7720  brecop  8557  dom2lem  8735  indpi  10594  nn0ind-raph  12350  cncls2  22332  ismbl2  24596  voliunlem3  24621  mdbr2  30559  dmdbr2  30566  mdsl2i  30585  mdsl2bi  30586  sgn3da  32408  wl-dral1d  35617  wl-equsald  35625  cvlsupr3  37285  cdleme32fva  38378  cdlemk33N  38850  cdlemk34  38851  ralbidar  41952  logic1  46024  tfis2d  46272