Theorem anandirs 687

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  3impdir  1361  oawordri  8507  omwordri  8529  oeordsuc  8552  phplem2  9162  muladd  11609  iccshftr  13480  iccshftl  13482  iccdil  13484  icccntr  13486  fzaddel  13553  fzsubel  13555  modadd1  13908  modmul1  13927  mulexp  14104  faclbnd5  14301  upxp  23656  uptx  23658  brbtwn2  29045  colinearalg  29050  eleesub  29051  eleesubd  29052  axcgrrflx  29054  axcgrid  29056  axsegconlem2  29058  phoeqi  30999  hial2eq2  31249  spansncvi  31794  5oalem3  31798  5oalem5  31800  hoscl  31887  hoeq1  31972  hoeq2  31973  hmops  32162  leopadd  32274  mdsymlem5  32549  lineintmo  36455  matunitlindflem1  38063  heicant  38102  ftc1anclem3  38142  ftc1anclem4  38143  ftc1anclem6  38145  ftc1anclem7  38146  ftc1anclem8  38147  ftc1anc  38148