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  5480  dfres3  5987  cores  6264  isoini  7372  eqfunresadj  7396  mpoeq123  7518  ordpwsuc  7853  xpord3pred  8199  rdglim2  8471  indpi1  12364  fzind  12827  btwnz  12832  elfzm11  13759  isprm2  16889  isprm3  16890  modprminv  17009  modprminveq  17010  isrngim2  20716  elimifd  33214  xrecex  33559  ordtconnlem1  34639  dfrdg4  36906  ee7.2aOLD  37440  expdioph  44234  cantnf2  44530  pm14.122b  45609  rexbidar  45631