Theorem anandirs 691

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  3impdir  1368  oawordri  8523  omwordri  8545  oeordsuc  8568  phplem2  9177  muladd  11634  iccshftr  13504  iccshftl  13506  iccdil  13508  icccntr  13510  fzaddel  13577  fzsubel  13579  modadd1  13932  modmul1  13951  mulexp  14128  faclbnd5  14325  upxp  23741  uptx  23743  brbtwn2  29164  colinearalg  29169  eleesub  29170  eleesubd  29171  axcgrrflx  29173  axcgrid  29175  axsegconlem2  29177  phoeqi  31118  hial2eq2  31368  spansncvi  31913  5oalem3  31917  5oalem5  31919  hoscl  32006  hoeq1  32091  hoeq2  32092  hmops  32281  leopadd  32393  mdsymlem5  32668  lineintmo  36520  matunitlindflem1  38127  heicant  38166  ftc1anclem3  38206  ftc1anclem4  38207  ftc1anclem6  38209  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212