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  4757  opeqsng  5478  dfres3  5971  cores  6238  isoini  7331  eqfunresadj  7353  mpoeq123  7479  ordpwsuc  7809  xpord3pred  8151  rdglim2  8446  fzind  12691  btwnz  12696  elfzm11  13612  isprm2  16701  isprm3  16702  modprminv  16819  modprminveq  16820  isrngim2  20413  isrimOLD  20453  bian1d  32437  elimifd  32524  indpi1  32837  xrecex  32894  ordtconnlem1  33955  dfrdg4  35969  ee7.2aOLD  36479  wl-ax11-lem8  37610  expdioph  43047  cantnf2  43349  pm14.122b  44447  rexbidar  44470