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  8534  omwordri  8556  oeordsuc  8579  phplem2  9188  muladd  11645  iccshftr  13512  iccshftl  13514  iccdil  13516  icccntr  13518  fzaddel  13586  fzsubel  13588  modadd1  13941  modmul1  13960  mulexp  14137  faclbnd5  14334  upxp  23759  uptx  23761  brbtwn2  29221  colinearalg  29226  eleesub  29227  eleesubd  29228  axcgrrflx  29230  axcgrid  29232  axsegconlem2  29234  phoeqi  31175  hial2eq2  31425  spansncvi  31970  5oalem3  31974  5oalem5  31976  hoscl  32063  hoeq1  32148  hoeq2  32149  hmops  32338  leopadd  32450  mdsymlem5  32725  lineintmo  36615  matunitlindflem1  38233  heicant  38272  ftc1anclem3  38312  ftc1anclem4  38313  ftc1anclem6  38315  ftc1anclem7  38316  ftc1anclem8  38317  ftc1anc  38318