Theorem pm5.32d 582

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  pm5.32rd  583  pm5.32da  584  anbi2d  636  raltpd  4720  opeqsng  5451  dfres3  5943  cores  6207  isoini  7289  eqfunresadj  7311  mpoeq123  7435  ordpwsuc  7762  xpord3pred  8099  rdglim2  8368  indpi1  12171  fzind  12625  btwnz  12630  elfzm11  13547  isprm2  16649  isprm3  16650  modprminv  16768  modprminveq  16769  isrngim2  20431  elimifd  32638  xrecex  33005  ordtconnlem1  34115  dfrdg4  36186  ee7.2aOLD  36696  expdioph  43475  cantnf2  43777  pm14.122b  44874  rexbidar  44896