Theorem anandirs 678

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 659	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜒)) → 𝜏)
3	2	anabsan2 673	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  1352  oawordri  8547  omwordri  8569  oeordsuc  8591  phplem2  9205  phplem4OLD  9217  muladd  11643  iccshftr  13460  iccshftl  13462  iccdil  13464  icccntr  13466  fzaddel  13532  fzsubel  13534  modadd1  13870  modmul1  13886  mulexp  14064  faclbnd5  14255  upxp  23119  uptx  23121  brbtwn2  28153  colinearalg  28158  eleesub  28159  eleesubd  28160  axcgrrflx  28162  axcgrid  28164  axsegconlem2  28166  phoeqi  30098  hial2eq2  30348  spansncvi  30893  5oalem3  30897  5oalem5  30899  hoscl  30986  hoeq1  31071  hoeq2  31072  hmops  31261  leopadd  31373  mdsymlem5  31648  lineintmo  35118  matunitlindflem1  36473  heicant  36512  ftc1anclem3  36552  ftc1anclem4  36553  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558