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  4742  opeqsng  5475  dfres3  5975  cores  6243  isoini  7338  eqfunresadj  7362  mpoeq123  7484  ordpwsuc  7815  xpord3pred  8153  rdglim2  8424  indpi1  12315  fzind  12778  btwnz  12783  elfzm11  13709  isprm2  16837  isprm3  16838  modprminv  16957  modprminveq  16958  isrngim2  20663  elimifd  33121  xrecex  33468  ordtconnlem1  34538  dfrdg4  36685  ee7.2aOLD  37219  expdioph  43983  cantnf2  44285  pm14.122b  45366  rexbidar  45388