Theorem anandirs 675

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  3impdir  1349  oawordri  8552  omwordri  8574  oeordsuc  8596  phplem2  9210  phplem4OLD  9222  muladd  11650  iccshftr  13467  iccshftl  13469  iccdil  13471  icccntr  13473  fzaddel  13539  fzsubel  13541  modadd1  13877  modmul1  13893  mulexp  14071  faclbnd5  14262  upxp  23347  uptx  23349  brbtwn2  28430  colinearalg  28435  eleesub  28436  eleesubd  28437  axcgrrflx  28439  axcgrid  28441  axsegconlem2  28443  phoeqi  30377  hial2eq2  30627  spansncvi  31172  5oalem3  31176  5oalem5  31178  hoscl  31265  hoeq1  31350  hoeq2  31351  hmops  31540  leopadd  31652  mdsymlem5  31927  lineintmo  35433  matunitlindflem1  36787  heicant  36826  ftc1anclem3  36866  ftc1anclem4  36867  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872