Theorem anandirs 874

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  3impdir  1382  oawordri  7630  omwordri  7652  oeordsuc  7674  phplem4  8142  muladd  10462  iccshftr  12306  iccshftl  12308  iccdil  12310  icccntr  12312  fzaddel  12375  fzsubel  12377  modadd1  12707  modmul1  12723  mulexp  12899  faclbnd5  13085  upxp  21426  uptx  21428  brbtwn2  25785  colinearalg  25790  eleesub  25791  eleesubd  25792  axcgrrflx  25794  axcgrid  25796  axsegconlem2  25798  phoeqi  27713  hial2eq2  27964  spansncvi  28511  5oalem3  28515  5oalem5  28517  hoscl  28604  hoeq1  28689  hoeq2  28690  hmops  28879  leopadd  28991  mdsymlem5  29266  lineintmo  32264  matunitlindflem1  33405  heicant  33444  ftc1anclem3  33487  ftc1anclem4  33488  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493