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 397

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 398

This theorem is referenced by:  3impdir  1351  oawordri  8412  omwordri  8434  oeordsuc  8456  phplem2  9029  phplem4OLD  9041  muladd  11453  iccshftr  13264  iccshftl  13266  iccdil  13268  icccntr  13270  fzaddel  13336  fzsubel  13338  modadd1  13674  modmul1  13690  mulexp  13868  faclbnd5  14058  upxp  22819  uptx  22821  brbtwn2  27318  colinearalg  27323  eleesub  27324  eleesubd  27325  axcgrrflx  27327  axcgrid  27329  axsegconlem2  27331  phoeqi  29264  hial2eq2  29514  spansncvi  30059  5oalem3  30063  5oalem5  30065  hoscl  30152  hoeq1  30237  hoeq2  30238  hmops  30427  leopadd  30539  mdsymlem5  30814  lineintmo  34504  matunitlindflem1  35817  heicant  35856  ftc1anclem3  35896  ftc1anclem4  35897  ftc1anclem6  35899  ftc1anclem7  35900  ftc1anclem8  35901  ftc1anc  35902