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  630  raltpd  4738  opeqsng  5451  dfres3  5943  cores  6207  isoini  7284  eqfunresadj  7306  mpoeq123  7430  ordpwsuc  7757  xpord3pred  8094  rdglim2  8363  fzind  12590  btwnz  12595  elfzm11  13511  isprm2  16609  isprm3  16610  modprminv  16727  modprminveq  16728  isrngim2  20389  bian1d  32530  elimifd  32618  indpi1  32941  xrecex  33001  ordtconnlem1  34081  dfrdg4  36145  ee7.2aOLD  36655  expdioph  43261  cantnf2  43563  pm14.122b  44660  rexbidar  44682