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  8474  omwordri  8496  oeordsuc  8518  phplem2  9124  muladd  11559  iccshftr  13396  iccshftl  13398  iccdil  13400  icccntr  13402  fzaddel  13468  fzsubel  13470  modadd1  13822  modmul1  13841  mulexp  14018  faclbnd5  14215  upxp  23548  uptx  23550  brbtwn2  28894  colinearalg  28899  eleesub  28900  eleesubd  28901  axcgrrflx  28903  axcgrid  28905  axsegconlem2  28907  phoeqi  30848  hial2eq2  31098  spansncvi  31643  5oalem3  31647  5oalem5  31649  hoscl  31736  hoeq1  31821  hoeq2  31822  hmops  32011  leopadd  32123  mdsymlem5  32398  lineintmo  36212  matunitlindflem1  37666  heicant  37705  ftc1anclem3  37745  ftc1anclem4  37746  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751