Theorem pm5.32d 579

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm5.32rd  580  pm5.32da  581  anbi2d  630  ralrexbid  3322  raltpd  4709  opeqsng  5385  dfres3  5852  cores  6096  isoini  7085  mpoeq123  7220  ordpwsuc  7524  rdglim2  8062  fzind  12074  btwnz  12078  elfzm11  12972  isprm2  16020  isprm3  16021  modprminv  16130  modprminveq  16131  isrim  19479  elimifd  30292  xrecex  30591  ordtconnlem1  31162  indpi1  31274  eqfunresadj  32999  dfrdg4  33407  ee7.2aOLD  33804  wl-ax11-lem8  34818  expdioph  39613  pm14.122b  40748  rexbidar  40771  isrngim  44169