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  8460  omwordri  8482  oeordsuc  8504  phplem2  9109  muladd  11541  iccshftr  13378  iccshftl  13380  iccdil  13382  icccntr  13384  fzaddel  13450  fzsubel  13452  modadd1  13804  modmul1  13823  mulexp  14000  faclbnd5  14197  upxp  23531  uptx  23533  brbtwn2  28876  colinearalg  28881  eleesub  28882  eleesubd  28883  axcgrrflx  28885  axcgrid  28887  axsegconlem2  28889  phoeqi  30827  hial2eq2  31077  spansncvi  31622  5oalem3  31626  5oalem5  31628  hoscl  31715  hoeq1  31800  hoeq2  31801  hmops  31990  leopadd  32102  mdsymlem5  32377  lineintmo  36170  matunitlindflem1  37635  heicant  37674  ftc1anclem3  37714  ftc1anclem4  37715  ftc1anclem6  37717  ftc1anclem7  37718  ftc1anclem8  37719  ftc1anc  37720