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  4733  opeqsng  5446  dfres3  5937  cores  6201  isoini  7278  eqfunresadj  7300  mpoeq123  7424  ordpwsuc  7751  xpord3pred  8088  rdglim2  8357  fzind  12577  btwnz  12582  elfzm11  13497  isprm2  16595  isprm3  16596  modprminv  16713  modprminveq  16714  isrngim2  20373  bian1d  32437  elimifd  32525  indpi1  32848  xrecex  32907  ordtconnlem1  33958  dfrdg4  36016  ee7.2aOLD  36526  expdioph  43140  cantnf2  43442  pm14.122b  44540  rexbidar  44562