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  8517  omwordri  8539  oeordsuc  8561  phplem2  9175  muladd  11617  iccshftr  13454  iccshftl  13456  iccdil  13458  icccntr  13460  fzaddel  13526  fzsubel  13528  modadd1  13877  modmul1  13896  mulexp  14073  faclbnd5  14270  upxp  23517  uptx  23519  brbtwn2  28839  colinearalg  28844  eleesub  28845  eleesubd  28846  axcgrrflx  28848  axcgrid  28850  axsegconlem2  28852  phoeqi  30793  hial2eq2  31043  spansncvi  31588  5oalem3  31592  5oalem5  31594  hoscl  31681  hoeq1  31766  hoeq2  31767  hmops  31956  leopadd  32068  mdsymlem5  32343  lineintmo  36152  matunitlindflem1  37617  heicant  37656  ftc1anclem3  37696  ftc1anclem4  37697  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702