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  1350  oawordri  8587  omwordri  8609  oeordsuc  8631  phplem2  9243  phplem4OLD  9255  muladd  11693  iccshftr  13523  iccshftl  13525  iccdil  13527  icccntr  13529  fzaddel  13595  fzsubel  13597  modadd1  13945  modmul1  13962  mulexp  14139  faclbnd5  14334  upxp  23647  uptx  23649  brbtwn2  28935  colinearalg  28940  eleesub  28941  eleesubd  28942  axcgrrflx  28944  axcgrid  28946  axsegconlem2  28948  phoeqi  30886  hial2eq2  31136  spansncvi  31681  5oalem3  31685  5oalem5  31687  hoscl  31774  hoeq1  31859  hoeq2  31860  hmops  32049  leopadd  32161  mdsymlem5  32436  lineintmo  36139  matunitlindflem1  37603  heicant  37642  ftc1anclem3  37682  ftc1anclem4  37683  ftc1anclem6  37685  ftc1anclem7  37686  ftc1anclem8  37687  ftc1anc  37688