Theorem anandirs 891

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 886	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜒)) → 𝜏)
3	2	anabsan2 880	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  3impdir  1422  oawordri  7675  omwordri  7697  oeordsuc  7719  phplem4  8183  muladd  10500  iccshftr  12344  iccshftl  12346  iccdil  12348  icccntr  12350  fzaddel  12413  fzsubel  12415  modadd1  12747  modmul1  12763  mulexp  12939  faclbnd5  13125  upxp  21474  uptx  21476  brbtwn2  25830  colinearalg  25835  eleesub  25836  eleesubd  25837  axcgrrflx  25839  axcgrid  25841  axsegconlem2  25843  phoeqi  27841  hial2eq2  28092  spansncvi  28639  5oalem3  28643  5oalem5  28645  hoscl  28732  hoeq1  28817  hoeq2  28818  hmops  29007  leopadd  29119  mdsymlem5  29394  lineintmo  32389  matunitlindflem1  33535  heicant  33574  ftc1anclem3  33617  ftc1anclem4  33618  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623