Theorem pm5.32d 577

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.)

Hypothesis

Ref	Expression
pm5.32d.1	⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))

Assertion

Ref	Expression
pm5.32d	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Proof of Theorem pm5.32d

Step	Hyp	Ref	Expression
1		pm5.32d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
2		pm5.32 574	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3	1, 2	sylib 217	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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  df-an 397

This theorem is referenced by:  pm5.32rd  578  pm5.32da  579  anbi2d  629  ralrexbidOLD  3107  raltpd  4784  opeqsng  5502  dfres3  5984  cores  6245  isoini  7331  eqfunresadj  7353  mpoeq123  7477  ordpwsuc  7799  xpord3pred  8134  rdglim2  8428  fzind  12656  btwnz  12661  elfzm11  13568  isprm2  16615  isprm3  16616  modprminv  16728  modprminveq  16729  isrimOLD  20263  elimifd  31762  xrecex  32073  ordtconnlem1  32892  indpi1  33006  dfrdg4  34911  ee7.2aOLD  35334  wl-ax11-lem8  36442  expdioph  41747  cantnf2  42060  pm14.122b  43167  rexbidar  43190  isrngim  46687