Theorem anandirs 692

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  3impdir  1370  oawordri  8536  omwordri  8558  oeordsuc  8581  phplem2  9198  muladd  11718  iccshftr  13587  iccshftl  13589  iccdil  13591  icccntr  13593  fzaddel  13661  fzsubel  13663  modadd1  14017  modmul1  14036  mulexp  14213  faclbnd5  14410  matunitlindflem1  22956  upxp  23904  uptx  23906  brbtwn2  29417  colinearalg  29422  eleesub  29423  eleesubd  29424  axcgrrflx  29426  axcgrid  29428  axsegconlem2  29430  phoeqi  31393  hial2eq2  31643  spansncvi  32188  5oalem3  32192  5oalem5  32194  hoscl  32281  hoeq1  32366  hoeq2  32367  hmops  32556  leopadd  32668  mdsymlem5  32943  lineintmo  36844  heicant  38493  ftc1anclem3  38533  ftc1anclem4  38534  ftc1anclem6  38536  ftc1anclem7  38537  ftc1anclem8  38538  ftc1anc  38539