Theorem anandirs 680

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  3impdir  1353  oawordri  8479  omwordri  8501  oeordsuc  8524  phplem2  9133  muladd  11573  iccshftr  13406  iccshftl  13408  iccdil  13410  icccntr  13412  fzaddel  13478  fzsubel  13480  modadd1  13832  modmul1  13851  mulexp  14028  faclbnd5  14225  upxp  23571  uptx  23573  brbtwn2  28961  colinearalg  28966  eleesub  28967  eleesubd  28968  axcgrrflx  28970  axcgrid  28972  axsegconlem2  28974  phoeqi  30915  hial2eq2  31165  spansncvi  31710  5oalem3  31714  5oalem5  31716  hoscl  31803  hoeq1  31888  hoeq2  31889  hmops  32078  leopadd  32190  mdsymlem5  32465  lineintmo  36332  matunitlindflem1  37788  heicant  37827  ftc1anclem3  37867  ftc1anclem4  37868  ftc1anclem6  37870  ftc1anclem7  37871  ftc1anclem8  37872  ftc1anc  37873