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  8514  omwordri  8536  oeordsuc  8558  phplem2  9169  muladd  11610  iccshftr  13447  iccshftl  13449  iccdil  13451  icccntr  13453  fzaddel  13519  fzsubel  13521  modadd1  13870  modmul1  13889  mulexp  14066  faclbnd5  14263  upxp  23510  uptx  23512  brbtwn2  28832  colinearalg  28837  eleesub  28838  eleesubd  28839  axcgrrflx  28841  axcgrid  28843  axsegconlem2  28845  phoeqi  30786  hial2eq2  31036  spansncvi  31581  5oalem3  31585  5oalem5  31587  hoscl  31674  hoeq1  31759  hoeq2  31760  hmops  31949  leopadd  32061  mdsymlem5  32336  lineintmo  36145  matunitlindflem1  37610  heicant  37649  ftc1anclem3  37689  ftc1anclem4  37690  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695