Theorem anandirs 678

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 659	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜒)) → 𝜏)
3	2	anabsan2 673	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 206  df-an 396

This theorem is referenced by:  3impdir  1349  oawordri  8564  omwordri  8586  oeordsuc  8608  phplem2  9224  phplem4OLD  9236  muladd  11668  iccshftr  13487  iccshftl  13489  iccdil  13491  icccntr  13493  fzaddel  13559  fzsubel  13561  modadd1  13897  modmul1  13913  mulexp  14090  faclbnd5  14281  upxp  23514  uptx  23516  brbtwn2  28703  colinearalg  28708  eleesub  28709  eleesubd  28710  axcgrrflx  28712  axcgrid  28714  axsegconlem2  28716  phoeqi  30654  hial2eq2  30904  spansncvi  31449  5oalem3  31453  5oalem5  31455  hoscl  31542  hoeq1  31627  hoeq2  31628  hmops  31817  leopadd  31929  mdsymlem5  32204  lineintmo  35689  matunitlindflem1  37024  heicant  37063  ftc1anclem3  37103  ftc1anclem4  37104  ftc1anclem6  37106  ftc1anclem7  37107  ftc1anclem8  37108  ftc1anc  37109