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  8586  omwordri  8608  oeordsuc  8631  phplem2  9248  muladd  11775  iccshftr  13644  iccshftl  13646  iccdil  13648  icccntr  13650  fzaddel  13719  fzsubel  13721  modadd1  14075  modmul1  14094  mulexp  14271  faclbnd5  14469  matunitlindflem1  23024  upxp  23972  uptx  23974  brbtwn2  29513  colinearalg  29518  eleesub  29519  eleesubd  29520  axcgrrflx  29522  axcgrid  29524  axsegconlem2  29526  phoeqi  31489  hial2eq2  31739  spansncvi  32284  5oalem3  32288  5oalem5  32290  hoscl  32377  hoeq1  32462  hoeq2  32463  hmops  32652  leopadd  32764  mdsymlem5  33039  lineintmo  37100  heicant  38765  ftc1anclem3  38805  ftc1anclem4  38806  ftc1anclem6  38808  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811