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  8170  omwordri  8192  oeordsuc  8214  phplem4  8693  muladd  11066  iccshftr  12866  iccshftl  12868  iccdil  12870  icccntr  12872  fzaddel  12935  fzsubel  12937  modadd1  13270  modmul1  13286  mulexp  13462  faclbnd5  13652  upxp  22225  uptx  22227  brbtwn2  26685  colinearalg  26690  eleesub  26691  eleesubd  26692  axcgrrflx  26694  axcgrid  26696  axsegconlem2  26698  phoeqi  28628  hial2eq2  28878  spansncvi  29423  5oalem3  29427  5oalem5  29429  hoscl  29516  hoeq1  29601  hoeq2  29602  hmops  29791  leopadd  29903  mdsymlem5  30178  lineintmo  33613  matunitlindflem1  34882  heicant  34921  ftc1anclem3  34963  ftc1anclem4  34964  ftc1anclem6  34966  ftc1anclem7  34967  ftc1anclem8  34968  ftc1anc  34969