Theorem anandirs 677

Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)

Hypothesis

Ref	Expression
anandirs.1	⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒)) → 𝜏)

Assertion

Ref	Expression
anandirs	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏)

Proof of Theorem anandirs

Step	Hyp	Ref	Expression
1		anandirs.1	. . 3 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
2	1	an4s 658	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜒)) → 𝜏)
3	2	anabsan2 672	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  3impdir  1347  oawordri  8178  omwordri  8200  oeordsuc  8222  phplem4  8701  muladd  11074  iccshftr  12875  iccshftl  12877  iccdil  12879  icccntr  12881  fzaddel  12944  fzsubel  12946  modadd1  13279  modmul1  13295  mulexp  13471  faclbnd5  13661  upxp  22233  uptx  22235  brbtwn2  26693  colinearalg  26698  eleesub  26699  eleesubd  26700  axcgrrflx  26702  axcgrid  26704  axsegconlem2  26706  phoeqi  28636  hial2eq2  28886  spansncvi  29431  5oalem3  29435  5oalem5  29437  hoscl  29524  hoeq1  29609  hoeq2  29610  hmops  29799  leopadd  29911  mdsymlem5  30186  lineintmo  33620  matunitlindflem1  34890  heicant  34929  ftc1anclem3  34971  ftc1anclem4  34972  ftc1anclem6  34974  ftc1anclem7  34975  ftc1anclem8  34976  ftc1anc  34977