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  8588  omwordri  8610  oeordsuc  8632  phplem2  9245  phplem4OLD  9257  muladd  11695  iccshftr  13526  iccshftl  13528  iccdil  13530  icccntr  13532  fzaddel  13598  fzsubel  13600  modadd1  13948  modmul1  13965  mulexp  14142  faclbnd5  14337  upxp  23631  uptx  23633  brbtwn2  28920  colinearalg  28925  eleesub  28926  eleesubd  28927  axcgrrflx  28929  axcgrid  28931  axsegconlem2  28933  phoeqi  30876  hial2eq2  31126  spansncvi  31671  5oalem3  31675  5oalem5  31677  hoscl  31764  hoeq1  31849  hoeq2  31850  hmops  32039  leopadd  32151  mdsymlem5  32426  lineintmo  36158  matunitlindflem1  37623  heicant  37662  ftc1anclem3  37702  ftc1anclem4  37703  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708