Theorem anandirs 675

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 656	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜒)) → 𝜏)
3	2	anabsan2 670	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 206  df-an 396

This theorem is referenced by:  3impdir  1349  oawordri  8357  omwordri  8379  oeordsuc  8401  phplem2  8955  phplem4OLD  8968  muladd  11390  iccshftr  13200  iccshftl  13202  iccdil  13204  icccntr  13206  fzaddel  13272  fzsubel  13274  modadd1  13609  modmul1  13625  mulexp  13803  faclbnd5  13993  upxp  22755  uptx  22757  brbtwn2  27254  colinearalg  27259  eleesub  27260  eleesubd  27261  axcgrrflx  27263  axcgrid  27265  axsegconlem2  27267  phoeqi  29198  hial2eq2  29448  spansncvi  29993  5oalem3  29997  5oalem5  29999  hoscl  30086  hoeq1  30171  hoeq2  30172  hmops  30361  leopadd  30473  mdsymlem5  30748  lineintmo  34438  matunitlindflem1  35752  heicant  35791  ftc1anclem3  35831  ftc1anclem4  35832  ftc1anclem6  35834  ftc1anclem7  35835  ftc1anclem8  35836  ftc1anc  35837