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  4735  opeqsng  5450  dfres3  5939  cores  6202  isoini  7279  eqfunresadj  7301  mpoeq123  7425  ordpwsuc  7754  xpord3pred  8092  rdglim2  8361  fzind  12592  btwnz  12597  elfzm11  13516  isprm2  16611  isprm3  16612  modprminv  16729  modprminveq  16730  isrngim2  20356  isrimOLD  20396  bian1d  32418  elimifd  32505  indpi1  32816  xrecex  32873  ordtconnlem1  33890  dfrdg4  35924  ee7.2aOLD  36434  wl-ax11-lem8  37565  expdioph  42996  cantnf2  43298  pm14.122b  44396  rexbidar  44419