Theorem pm5.32d 674

Description: Distribution of implication over biconditional (deduction rule). (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 671	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3	1, 2	sylib 208	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  pm5.32rd  675  pm5.32da  676  anbi2d  742  raltpd  4458  dfres3  5556  cores  5799  isoini  6751  mpt2eq123  6879  ordpwsuc  7180  rdglim2  7697  fzind  11667  btwnz  11671  elfzm11  12604  isprm2  15597  isprm3  15598  modprminv  15706  modprminveq  15707  isrim  18935  elimifd  29669  funcnvmptOLD  29776  xrecex  29937  ordtconnlem1  30279  indpi1  30391  dfrdg4  32364  ee7.2aOLD  32766  wl-ax11-lem8  33682  expdioph  38092  pm14.122b  39126  rexbidar  39152  mapsnend  39890  isrngim  42414