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  4738  opeqsng  5474  dfres3  5974  cores  6250  isoini  7346  eqfunresadj  7370  mpoeq123  7492  ordpwsuc  7826  xpord3pred  8171  rdglim2  8443  indpi1  12337  fzind  12800  btwnz  12805  elfzm11  13732  isprm2  16862  isprm3  16863  modprminv  16982  modprminveq  16983  isrngim2  20688  elimifd  33186  xrecex  33532  ordtconnlem1  34602  dfrdg4  36807  ee7.2aOLD  37341  expdioph  44123  cantnf2  44420  pm14.122b  45500  rexbidar  45522