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  8559  omwordri  8581  oeordsuc  8604  phplem2  9221  muladd  11749  iccshftr  13618  iccshftl  13620  iccdil  13622  icccntr  13624  fzaddel  13693  fzsubel  13695  modadd1  14049  modmul1  14068  mulexp  14245  faclbnd5  14443  matunitlindflem1  22995  upxp  23943  uptx  23945  brbtwn2  29484  colinearalg  29489  eleesub  29490  eleesubd  29491  axcgrrflx  29493  axcgrid  29495  axsegconlem2  29497  phoeqi  31460  hial2eq2  31710  spansncvi  32255  5oalem3  32259  5oalem5  32261  hoscl  32348  hoeq1  32433  hoeq2  32434  hmops  32623  leopadd  32735  mdsymlem5  33010  lineintmo  36997  heicant  38649  ftc1anclem3  38689  ftc1anclem4  38690  ftc1anclem6  38692  ftc1anclem7  38693  ftc1anclem8  38694  ftc1anc  38695