Theorem pm5.32d 588

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm5.32rd  589  pm5.32da  590  anbi2d  642  raltpd  4752  opeqsng  5491  dfres3  5988  cores  6255  isoini  7347  eqfunresadj  7371  mpoeq123  7495  ordpwsuc  7820  xpord3pred  8157  rdglim2  8428  indpi1  12250  fzind  12712  btwnz  12717  elfzm11  13642  isprm2  16765  isprm3  16766  modprminv  16884  modprminveq  16885  isrngim2  20568  elimifd  32926  xrecex  33276  ordtconnlem1  34345  dfrdg4  36464  ee7.2aOLD  37013  expdioph  43791  cantnf2  44093  pm14.122b  45174  rexbidar  45196