Theorem anandirs 680

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 661	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜒)) → 𝜏)
3	2	anabsan2 675	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  1353  oawordri  8485  omwordri  8507  oeordsuc  8530  phplem2  9139  muladd  11582  iccshftr  13439  iccshftl  13441  iccdil  13443  icccntr  13445  fzaddel  13512  fzsubel  13514  modadd1  13867  modmul1  13886  mulexp  14063  faclbnd5  14260  upxp  23588  uptx  23590  brbtwn2  28974  colinearalg  28979  eleesub  28980  eleesubd  28981  axcgrrflx  28983  axcgrid  28985  axsegconlem2  28987  phoeqi  30928  hial2eq2  31178  spansncvi  31723  5oalem3  31727  5oalem5  31729  hoscl  31816  hoeq1  31901  hoeq2  31902  hmops  32091  leopadd  32203  mdsymlem5  32478  lineintmo  36339  matunitlindflem1  37937  heicant  37976  ftc1anclem3  38016  ftc1anclem4  38017  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022