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 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  578  pm5.32da  579  anbi2d  630  raltpd  4745  opeqsng  5463  dfres3  5955  cores  6222  isoini  7313  eqfunresadj  7335  mpoeq123  7461  ordpwsuc  7790  xpord3pred  8131  rdglim2  8400  fzind  12632  btwnz  12637  elfzm11  13556  isprm2  16652  isprm3  16653  modprminv  16770  modprminveq  16771  isrngim2  20362  isrimOLD  20402  bian1d  32385  elimifd  32472  indpi1  32783  xrecex  32840  ordtconnlem1  33914  dfrdg4  35939  ee7.2aOLD  36449  wl-ax11-lem8  37580  expdioph  43012  cantnf2  43314  pm14.122b  44412  rexbidar  44435