Theorem anandirs 679

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 660	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜒)) → 𝜏)
3	2	anabsan2 674	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ 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:  3impdir  1352  oawordri  8475  omwordri  8497  oeordsuc  8519  phplem2  9129  muladd  11570  iccshftr  13407  iccshftl  13409  iccdil  13411  icccntr  13413  fzaddel  13479  fzsubel  13481  modadd1  13830  modmul1  13849  mulexp  14026  faclbnd5  14223  upxp  23526  uptx  23528  brbtwn2  28868  colinearalg  28873  eleesub  28874  eleesubd  28875  axcgrrflx  28877  axcgrid  28879  axsegconlem2  28881  phoeqi  30819  hial2eq2  31069  spansncvi  31614  5oalem3  31618  5oalem5  31620  hoscl  31707  hoeq1  31792  hoeq2  31793  hmops  31982  leopadd  32094  mdsymlem5  32369  lineintmo  36130  matunitlindflem1  37595  heicant  37634  ftc1anclem3  37674  ftc1anclem4  37675  ftc1anclem6  37677  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680