Theorem anandirs 678

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  3impdir  1352  oawordri  8546  omwordri  8568  oeordsuc  8590  phplem2  9204  phplem4OLD  9216  muladd  11642  iccshftr  13459  iccshftl  13461  iccdil  13463  icccntr  13465  fzaddel  13531  fzsubel  13533  modadd1  13869  modmul1  13885  mulexp  14063  faclbnd5  14254  upxp  23109  uptx  23111  brbtwn2  28143  colinearalg  28148  eleesub  28149  eleesubd  28150  axcgrrflx  28152  axcgrid  28154  axsegconlem2  28156  phoeqi  30088  hial2eq2  30338  spansncvi  30883  5oalem3  30887  5oalem5  30889  hoscl  30976  hoeq1  31061  hoeq2  31062  hmops  31251  leopadd  31363  mdsymlem5  31638  lineintmo  35067  matunitlindflem1  36422  heicant  36461  ftc1anclem3  36501  ftc1anclem4  36502  ftc1anclem6  36504  ftc1anclem7  36505  ftc1anclem8  36506  ftc1anc  36507