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 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  341  imim21b  396  pm5.74da  803  sbiedvw  2097  sbiedw  2310  dvelimdf  2449  sbied  2503  2mos  2646  cbvraldva2  3345  csbie2df  4441  dfiin2g  5036  oneqmini  6417  tfindsg  7850  findsg  7890  brecop  8804  dom2lem  8988  indpi  10902  nn0ind-raph  12662  cncls2  22777  ismbl2  25044  voliunlem3  25069  mdbr2  31549  dmdbr2  31556  mdsl2i  31575  mdsl2bi  31576  sgn3da  33540  wl-dral1d  36400  wl-equsald  36408  cvlsupr3  38214  cdleme32fva  39308  cdlemk33N  39780  cdlemk34  39781  ralbidar  43204  logic1  47476  tfis2d  47725