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  8562  omwordri  8584  oeordsuc  8606  phplem2  9219  muladd  11669  iccshftr  13503  iccshftl  13505  iccdil  13507  icccntr  13509  fzaddel  13575  fzsubel  13577  modadd1  13925  modmul1  13942  mulexp  14119  faclbnd5  14316  upxp  23561  uptx  23563  brbtwn2  28884  colinearalg  28889  eleesub  28890  eleesubd  28891  axcgrrflx  28893  axcgrid  28895  axsegconlem2  28897  phoeqi  30838  hial2eq2  31088  spansncvi  31633  5oalem3  31637  5oalem5  31639  hoscl  31726  hoeq1  31811  hoeq2  31812  hmops  32001  leopadd  32113  mdsymlem5  32388  lineintmo  36175  matunitlindflem1  37640  heicant  37679  ftc1anclem3  37719  ftc1anclem4  37720  ftc1anclem6  37722  ftc1anclem7  37723  ftc1anclem8  37724  ftc1anc  37725