Theorem pm5.32d 576

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm5.32rd  577  pm5.32da  578  anbi2d  629  ralrexbidOLD  3113  raltpd  4806  opeqsng  5522  dfres3  6014  cores  6280  isoini  7374  eqfunresadj  7396  mpoeq123  7522  ordpwsuc  7851  xpord3pred  8193  rdglim2  8488  fzind  12741  btwnz  12746  elfzm11  13655  isprm2  16729  isprm3  16730  modprminv  16846  modprminveq  16847  isrngim2  20479  isrimOLD  20519  bian1d  32484  elimifd  32566  xrecex  32884  ordtconnlem1  33870  indpi1  33984  dfrdg4  35915  ee7.2aOLD  36427  wl-ax11-lem8  37546  expdioph  42980  cantnf2  43287  pm14.122b  44392  rexbidar  44415