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  8476  omwordri  8498  oeordsuc  8521  phplem2  9130  muladd  11571  iccshftr  13428  iccshftl  13430  iccdil  13432  icccntr  13434  fzaddel  13501  fzsubel  13503  modadd1  13856  modmul1  13875  mulexp  14052  faclbnd5  14249  upxp  23597  uptx  23599  brbtwn2  28993  colinearalg  28998  eleesub  28999  eleesubd  29000  axcgrrflx  29002  axcgrid  29004  axsegconlem2  29006  phoeqi  30948  hial2eq2  31198  spansncvi  31743  5oalem3  31747  5oalem5  31749  hoscl  31836  hoeq1  31921  hoeq2  31922  hmops  32111  leopadd  32223  mdsymlem5  32498  lineintmo  36360  matunitlindflem1  37948  heicant  37987  ftc1anclem3  38027  ftc1anclem4  38028  ftc1anclem6  38030  ftc1anclem7  38031  ftc1anclem8  38032  ftc1anc  38033