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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  pm5.32rd  578  pm5.32da  579  anbi2d  629  ralrexbidOLD  3256  raltpd  4717  opeqsng  5417  dfres3  5896  cores  6153  isoini  7209  mpoeq123  7347  ordpwsuc  7662  rdglim2  8263  fzind  12418  btwnz  12423  elfzm11  13327  isprm2  16387  isprm3  16388  modprminv  16500  modprminveq  16501  isrim  19977  elimifd  30886  xrecex  31194  ordtconnlem1  31874  indpi1  31988  eqfunresadj  33735  xpord3pred  33798  dfrdg4  34253  ee7.2aOLD  34650  wl-ax11-lem8  35743  expdioph  40845  pm14.122b  42041  rexbidar  42064  isrngim  45462