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  2095  sbiedw  2320  dvelimdf  2457  sbied  2511  2mosOLD  2653  cbvraldva2  3356  csbie2df  4466  dfiin2g  5055  oneqmini  6447  tfindsg  7898  findsg  7937  brecop  8868  dom2lem  9052  indpi  10976  nn0ind-raph  12743  cncls2  23302  ismbl2  25581  voliunlem3  25606  mdbr2  32328  dmdbr2  32335  mdsl2i  32354  mdsl2bi  32355  sgn3da  34506  wl-dral1d  37485  wl-equsald  37493  wl-equsaldv  37494  cvlsupr3  39300  cdleme32fva  40394  cdlemk33N  40866  cdlemk34  40867  ralbidar  44414  logic1  48524  tfis2d  48772