Theorem anandirs 692

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

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

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 402

This theorem is used by:  3impdir  1370  oawordri  8540  omwordri  8562  oeordsuc  8585  phplem2  9202  muladd  11673  iccshftr  13541  iccshftl  13543  iccdil  13545  icccntr  13547  fzaddel  13615  fzsubel  13617  modadd1  13971  modmul1  13990  mulexp  14167  faclbnd5  14364  matunitlindflem1  22905  upxp  23853  uptx  23855  brbtwn2  29363  colinearalg  29368  eleesub  29369  eleesubd  29370  axcgrrflx  29372  axcgrid  29374  axsegconlem2  29376  phoeqi  31339  hial2eq2  31589  spansncvi  32134  5oalem3  32138  5oalem5  32140  hoscl  32227  hoeq1  32312  hoeq2  32313  hmops  32502  leopadd  32614  mdsymlem5  32889  lineintmo  36739  heicant  38406  ftc1anclem3  38446  ftc1anclem4  38447  ftc1anclem6  38449  ftc1anclem7  38450  ftc1anclem8  38451  ftc1anc  38452