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  4786  opeqsng  5504  dfres3  5987  cores  6249  isoini  7335  eqfunresadj  7357  mpoeq123  7481  ordpwsuc  7803  xpord3pred  8138  rdglim2  8432  fzind  12660  btwnz  12665  elfzm11  13572  isprm2  16619  isprm3  16620  modprminv  16732  modprminveq  16733  isrimOLD  20271  elimifd  31806  xrecex  32117  ordtconnlem1  32935  indpi1  33049  dfrdg4  34954  ee7.2aOLD  35394  wl-ax11-lem8  36502  expdioph  41810  cantnf2  42123  pm14.122b  43230  rexbidar  43253  isrngim  46750