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 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  3impdir  1369  oawordri  8533  omwordri  8555  oeordsuc  8578  phplem2  9187  muladd  11652  iccshftr  13519  iccshftl  13521  iccdil  13523  icccntr  13525  fzaddel  13593  fzsubel  13595  modadd1  13948  modmul1  13967  mulexp  14144  faclbnd5  14341  upxp  23791  uptx  23793  brbtwn2  29266  colinearalg  29271  eleesub  29272  eleesubd  29273  axcgrrflx  29275  axcgrid  29277  axsegconlem2  29279  phoeqi  31220  hial2eq2  31470  spansncvi  32015  5oalem3  32019  5oalem5  32021  hoscl  32108  hoeq1  32193  hoeq2  32194  hmops  32383  leopadd  32495  mdsymlem5  32770  lineintmo  36657  matunitlindflem1  38295  heicant  38334  ftc1anclem3  38374  ftc1anclem4  38375  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380