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 217	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

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

This theorem is referenced by:  pm5.32rd  577  pm5.32da  578  anbi2d  628  ralrexbidOLD  3251  raltpd  4714  opeqsng  5411  dfres3  5885  cores  6142  isoini  7189  mpoeq123  7325  ordpwsuc  7637  rdglim2  8234  fzind  12348  btwnz  12352  elfzm11  13256  isprm2  16315  isprm3  16316  modprminv  16428  modprminveq  16429  isrim  19892  elimifd  30787  xrecex  31096  ordtconnlem1  31776  indpi1  31888  eqfunresadj  33641  xpord3pred  33725  dfrdg4  34180  ee7.2aOLD  34577  wl-ax11-lem8  35670  expdioph  40761  pm14.122b  41930  rexbidar  41953  isrngim  45350