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 399

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 210  df-an 400

This theorem is referenced by:  3impdir  1348  oawordri  8159  omwordri  8181  oeordsuc  8203  phplem4  8683  muladd  11061  iccshftr  12864  iccshftl  12866  iccdil  12868  icccntr  12870  fzaddel  12936  fzsubel  12938  modadd1  13271  modmul1  13287  mulexp  13464  faclbnd5  13654  upxp  22228  uptx  22230  brbtwn2  26699  colinearalg  26704  eleesub  26705  eleesubd  26706  axcgrrflx  26708  axcgrid  26710  axsegconlem2  26712  phoeqi  28640  hial2eq2  28890  spansncvi  29435  5oalem3  29439  5oalem5  29441  hoscl  29528  hoeq1  29613  hoeq2  29614  hmops  29803  leopadd  29915  mdsymlem5  30190  lineintmo  33731  matunitlindflem1  35053  heicant  35092  ftc1anclem3  35132  ftc1anclem4  35133  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138