Theorem anandirs 679

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 660	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜒)) → 𝜏)
3	2	anabsan2 674	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  1352  oawordri  8468  omwordri  8490  oeordsuc  8512  phplem2  9119  muladd  11552  iccshftr  13389  iccshftl  13391  iccdil  13393  icccntr  13395  fzaddel  13461  fzsubel  13463  modadd1  13812  modmul1  13831  mulexp  14008  faclbnd5  14205  upxp  23508  uptx  23510  brbtwn2  28850  colinearalg  28855  eleesub  28856  eleesubd  28857  axcgrrflx  28859  axcgrid  28861  axsegconlem2  28863  phoeqi  30801  hial2eq2  31051  spansncvi  31596  5oalem3  31600  5oalem5  31602  hoscl  31689  hoeq1  31774  hoeq2  31775  hmops  31964  leopadd  32076  mdsymlem5  32351  lineintmo  36135  matunitlindflem1  37600  heicant  37639  ftc1anclem3  37679  ftc1anclem4  37680  ftc1anclem6  37682  ftc1anclem7  37683  ftc1anclem8  37684  ftc1anc  37685