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  4731  opeqsng  5441  dfres3  5932  cores  6196  isoini  7272  eqfunresadj  7294  mpoeq123  7418  ordpwsuc  7745  xpord3pred  8082  rdglim2  8351  fzind  12571  btwnz  12576  elfzm11  13495  isprm2  16593  isprm3  16594  modprminv  16711  modprminveq  16712  isrngim2  20371  bian1d  32435  elimifd  32523  indpi1  32841  xrecex  32900  ordtconnlem1  33937  dfrdg4  35995  ee7.2aOLD  36505  expdioph  43115  cantnf2  43417  pm14.122b  44515  rexbidar  44537