Theorem pm5.32d 578

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 575	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3	1, 2	sylib 217	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

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

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 398

This theorem is referenced by:  pm5.32rd  579  pm5.32da  580  anbi2d  630  ralrexbidOLD  3108  raltpd  4737  opeqsng  5454  dfres3  5935  cores  6194  isoini  7274  eqfunresadj  7296  mpoeq123  7418  ordpwsuc  7737  rdglim2  8342  fzind  12528  btwnz  12533  elfzm11  13437  isprm2  16489  isprm3  16490  modprminv  16602  modprminveq  16603  isrimOLD  20078  elimifd  31237  xrecex  31545  ordtconnlem1  32236  indpi1  32350  xpord3pred  34144  dfrdg4  34392  ee7.2aOLD  34789  wl-ax11-lem8  35899  expdioph  41159  pm14.122b  42414  rexbidar  42437  isrngim  45880