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  8487  omwordri  8509  oeordsuc  8532  phplem2  9141  muladd  11581  iccshftr  13414  iccshftl  13416  iccdil  13418  icccntr  13420  fzaddel  13486  fzsubel  13488  modadd1  13840  modmul1  13859  mulexp  14036  faclbnd5  14233  upxp  23579  uptx  23581  brbtwn2  28990  colinearalg  28995  eleesub  28996  eleesubd  28997  axcgrrflx  28999  axcgrid  29001  axsegconlem2  29003  phoeqi  30944  hial2eq2  31194  spansncvi  31739  5oalem3  31743  5oalem5  31745  hoscl  31832  hoeq1  31917  hoeq2  31918  hmops  32107  leopadd  32219  mdsymlem5  32494  lineintmo  36370  matunitlindflem1  37856  heicant  37895  ftc1anclem3  37935  ftc1anclem4  37936  ftc1anclem6  37938  ftc1anclem7  37939  ftc1anclem8  37940  ftc1anc  37941