Theorem simpl1l 1243

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl1l	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpl1l

Step	Hyp	Ref	Expression
1		simpll 778	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl1 1204	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  soisores  7327  tfisi  7856  funelss  8045  omopth2  8570  swrdsbslen  14704  swrdspsleq  14705  repswswrd  14823  ramub1lem1  17087  cntzsubrng  20653  cntzsubr  20692  lbspss  21184  maducoeval2  22778  cramer  22829  neiptopnei  23270  ptbasin  23715  basqtop  23849  tmdgsum  24233  ustuqtop1  24379  cxplea  26839  cxple2  26840  nosupbnd2lem1  27857  noinfbnd2lem1  27872  ltmuls2  28342  ewlkle  29933  uspgr2wlkeq2  29974  clwwlkccat  30319  br8d  32931  isarchi2  33483  archiabllem2c  33493  cvmlift2lem10  35782  5segofs  36476  2llnjaN  40318  lvolnle3at  40334  paddasslem12  40583  paddasslem13  40584  atmod1i1m  40610  lhp2lt  40753  lhpexle2lem  40761  lhpmcvr3  40777  lhpat3  40798  ltrneq2  40900  trlnle  40938  trlval3  40939  trlval4  40940  cdleme0moN  40977  cdleme17b  41039  cdlemefrs29pre00  41147  cdlemefr27cl  41155  cdleme42ke  41237  cdleme42mgN  41240  cdleme46f2g2  41245  cdleme46f2g1  41246  cdleme50eq  41293  cdleme50trn3  41305  trlord  41321  cdlemg6c  41372  cdlemg11b  41394  cdlemg18a  41430  cdlemg42  41481  cdlemg46  41487  trljco  41492  tendococl  41524  cdlemj3  41575  tendotr  41582  cdlemk35s-id  41690  cdlemk39s-id  41692  cdlemk53b  41708  cdlemk53  41709  cdlemk35u  41716  tendoex  41727  cdlemm10N  41870  dihopelvalcpre  42000  dihord6apre  42008  dihord5b  42011  dihglblem5apreN  42043  dihglblem2N  42046  dihmeetlem4preN  42058  dihmeetlem6  42061  dihmeetlem10N  42068  dihmeetlem11N  42069  dihmeetlem16N  42074  dihmeetlem17N  42075  dihmeetlem18N  42076  dihmeetlem19N  42077  dihmeetALTN  42079  dihlspsnat  42085  dvh3dim2  42200  dvh3dim3N  42201  jm2.25lem1  43705  jm2.26  43709  grur1cld  44936  limcperiod  46324  0ellimcdiv  46343  cncfshift  46568  cncfperiod  46573  icccncfext  46581  stoweidlem34  46728  fourierdlem48  46848  fourierdlem87  46887  sge0xaddlem2  47128  smflimsuplem7  47520  domnmsuppn0  49126  itscnhlinecirc02plem2  49540