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  8544  omwordri  8566  oeordsuc  8589  phplem2  9199  muladd  11664  iccshftr  13531  iccshftl  13533  iccdil  13535  icccntr  13537  fzaddel  13605  fzsubel  13607  modadd1  13961  modmul1  13980  mulexp  14157  faclbnd5  14354  upxp  23810  uptx  23812  brbtwn2  29285  colinearalg  29290  eleesub  29291  eleesubd  29292  axcgrrflx  29294  axcgrid  29296  axsegconlem2  29298  phoeqi  31239  hial2eq2  31489  spansncvi  32034  5oalem3  32038  5oalem5  32040  hoscl  32127  hoeq1  32212  hoeq2  32213  hmops  32402  leopadd  32514  mdsymlem5  32789  lineintmo  36662  matunitlindflem1  38300  heicant  38339  ftc1anclem3  38379  ftc1anclem4  38380  ftc1anclem6  38382  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385