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  631  raltpd  4726  opeqsng  5451  dfres3  5943  cores  6207  isoini  7286  eqfunresadj  7308  mpoeq123  7432  ordpwsuc  7759  xpord3pred  8095  rdglim2  8364  indpi1  12164  fzind  12618  btwnz  12623  elfzm11  13540  isprm2  16642  isprm3  16643  modprminv  16761  modprminveq  16762  isrngim2  20424  elimifd  32628  xrecex  32994  ordtconnlem1  34084  dfrdg4  36149  ee7.2aOLD  36659  expdioph  43469  cantnf2  43771  pm14.122b  44868  rexbidar  44890