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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm5.32rd  578  pm5.32da  579  anbi2d  630  raltpd  4748  opeqsng  5466  dfres3  5958  cores  6225  isoini  7316  eqfunresadj  7338  mpoeq123  7464  ordpwsuc  7793  xpord3pred  8134  rdglim2  8403  fzind  12639  btwnz  12644  elfzm11  13563  isprm2  16659  isprm3  16660  modprminv  16777  modprminveq  16778  isrngim2  20369  isrimOLD  20409  bian1d  32392  elimifd  32479  indpi1  32790  xrecex  32847  ordtconnlem1  33921  dfrdg4  35946  ee7.2aOLD  36456  wl-ax11-lem8  37587  expdioph  43019  cantnf2  43321  pm14.122b  44419  rexbidar  44442