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  ralrexbidOLD  3105  raltpd  4786  opeqsng  5513  dfres3  6005  cores  6271  isoini  7358  eqfunresadj  7380  mpoeq123  7505  ordpwsuc  7835  xpord3pred  8176  rdglim2  8471  fzind  12714  btwnz  12719  elfzm11  13632  isprm2  16716  isprm3  16717  modprminv  16833  modprminveq  16834  isrngim2  20470  isrimOLD  20510  bian1d  32484  elimifd  32564  xrecex  32887  ordtconnlem1  33885  indpi1  34001  dfrdg4  35933  ee7.2aOLD  36444  wl-ax11-lem8  37573  expdioph  43012  cantnf2  43315  pm14.122b  44419  rexbidar  44442