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  339  imim21b  393  pm5.74da  800  sbiedvw  2094  sbiedw  2307  dvelimdf  2446  sbied  2500  2mos  2643  cbvraldva2  3342  csbie2df  4439  dfiin2g  5034  oneqmini  6415  tfindsg  7852  findsg  7892  brecop  8806  dom2lem  8990  indpi  10904  nn0ind-raph  12666  cncls2  22997  ismbl2  25276  voliunlem3  25301  mdbr2  31816  dmdbr2  31823  mdsl2i  31842  mdsl2bi  31843  sgn3da  33838  wl-dral1d  36703  wl-equsald  36711  cvlsupr3  38517  cdleme32fva  39611  cdlemk33N  40083  cdlemk34  40084  ralbidar  43506  logic1  47563  tfis2d  47812