Theorem anandirs 685

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  3impdir  1358  oawordri  8482  omwordri  8504  oeordsuc  8527  phplem2  9136  muladd  11580  iccshftr  13437  iccshftl  13439  iccdil  13441  icccntr  13443  fzaddel  13510  fzsubel  13512  modadd1  13865  modmul1  13884  mulexp  14061  faclbnd5  14258  upxp  23613  uptx  23615  brbtwn2  28999  colinearalg  29004  eleesub  29005  eleesubd  29006  axcgrrflx  29008  axcgrid  29010  axsegconlem2  29012  phoeqi  30953  hial2eq2  31203  spansncvi  31748  5oalem3  31752  5oalem5  31754  hoscl  31841  hoeq1  31926  hoeq2  31927  hmops  32116  leopadd  32228  mdsymlem5  32503  lineintmo  36386  matunitlindflem1  37984  heicant  38023  ftc1anclem3  38063  ftc1anclem4  38064  ftc1anclem6  38066  ftc1anclem7  38067  ftc1anclem8  38068  ftc1anc  38069