Theorem pm5.32d 580

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  pm5.32rd  581  pm5.32da  582  anbi2d  632  ralrexbid  3231  raltpd  4683  opeqsng  5371  dfres3  5841  cores  6093  isoini  7125  mpoeq123  7261  ordpwsuc  7572  rdglim2  8146  fzind  12240  btwnz  12244  elfzm11  13148  isprm2  16202  isprm3  16203  modprminv  16315  modprminveq  16316  isrim  19707  elimifd  30559  xrecex  30868  ordtconnlem1  31542  indpi1  31654  eqfunresadj  33405  xpord3pred  33478  dfrdg4  33939  ee7.2aOLD  34336  wl-ax11-lem8  35429  expdioph  40489  pm14.122b  41655  rexbidar  41678  isrngim  45078