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  4725  opeqsng  5457  dfres3  5949  cores  6213  isoini  7293  eqfunresadj  7315  mpoeq123  7439  ordpwsuc  7766  xpord3pred  8102  rdglim2  8371  indpi1  12173  fzind  12627  btwnz  12632  elfzm11  13549  isprm2  16651  isprm3  16652  modprminv  16770  modprminveq  16771  isrngim2  20433  elimifd  32613  xrecex  32979  ordtconnlem1  34068  dfrdg4  36133  ee7.2aOLD  36643  expdioph  43451  cantnf2  43753  pm14.122b  44850  rexbidar  44872