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 394

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 206  df-an 395

This theorem is referenced by:  3impdir  1348  oawordri  8569  omwordri  8591  oeordsuc  8613  phplem2  9231  phplem4OLD  9243  muladd  11676  iccshftr  13495  iccshftl  13497  iccdil  13499  icccntr  13501  fzaddel  13567  fzsubel  13569  modadd1  13905  modmul1  13921  mulexp  14098  faclbnd5  14289  upxp  23557  uptx  23559  brbtwn2  28772  colinearalg  28777  eleesub  28778  eleesubd  28779  axcgrrflx  28781  axcgrid  28783  axsegconlem2  28785  phoeqi  30723  hial2eq2  30973  spansncvi  31518  5oalem3  31522  5oalem5  31524  hoscl  31611  hoeq1  31696  hoeq2  31697  hmops  31886  leopadd  31998  mdsymlem5  32273  lineintmo  35823  matunitlindflem1  37159  heicant  37198  ftc1anclem3  37238  ftc1anclem4  37239  ftc1anclem6  37241  ftc1anclem7  37242  ftc1anclem8  37243  ftc1anc  37244