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 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  1351  oawordri  8606  omwordri  8628  oeordsuc  8650  phplem2  9271  phplem4OLD  9283  muladd  11722  iccshftr  13546  iccshftl  13548  iccdil  13550  icccntr  13552  fzaddel  13618  fzsubel  13620  modadd1  13959  modmul1  13975  mulexp  14152  faclbnd5  14347  upxp  23652  uptx  23654  brbtwn2  28938  colinearalg  28943  eleesub  28944  eleesubd  28945  axcgrrflx  28947  axcgrid  28949  axsegconlem2  28951  phoeqi  30889  hial2eq2  31139  spansncvi  31684  5oalem3  31688  5oalem5  31690  hoscl  31777  hoeq1  31862  hoeq2  31863  hmops  32052  leopadd  32164  mdsymlem5  32439  lineintmo  36121  matunitlindflem1  37576  heicant  37615  ftc1anclem3  37655  ftc1anclem4  37656  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661