Theorem pm5.32d 572

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  pm5.32rd  573  pm5.32da  574  anbi2d  622  raltpd  4535  opeqsng  5189  dfres3  5638  cores  5883  isoini  6848  mpt2eq123  6979  ordpwsuc  7281  rdglim2  7799  mapsnend  8307  fzind  11810  btwnz  11814  elfzm11  12712  isprm2  15774  isprm3  15775  modprminv  15882  modprminveq  15883  isrim  19096  elimifd  29906  xrecex  30169  ordtconnlem1  30511  indpi1  30623  eqfunresadj  32196  dfrdg4  32592  ee7.2aOLD  32988  wl-ax11-lem8  33908  expdioph  38428  pm14.122b  39458  rexbidar  39483  isrngim  42765