Theorem simp1l 1193

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1l	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Proof of Theorem simp1l

Step	Hyp	Ref	Expression
1		simpl 485	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	3ad2ant1 1129	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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  df-3an 1085

This theorem is referenced by:  simp11l  1280  simp21l  1286  simp31l  1292  tfisi  7573  offsplitfpar  7815  omeulem2  8209  uniinqs  8377  unxpdomlem3  8724  elfiun  8894  cantnffval  9126  tcrank  9313  cofsmo  9691  isfin2-2  9741  tskint  10207  tskun  10208  tskurn  10211  gruina  10240  dedekind  10803  subaddmulsub  11103  dmdcan  11350  lt2msq1  11524  supmullem1  11611  supmul  11613  xaddass  12643  xaddass2  12644  xlt2add  12654  xmulasslem3  12680  xadddi2r  12692  iccsplit  12872  expaddzlem  13473  expaddz  13474  expmulz  13476  ccatopth2  14079  pfxccat3  14096  resqrtcl  14613  limsupgle  14834  o1add  14970  o1mul  14971  o1sub  14972  bitsfzo  15784  sadfval  15801  smufval  15826  prmexpb  16062  4sqlem18  16298  vdwlem10  16326  fsets  16516  setsstruct2  16521  submre  16876  mrelatlub  17796  gsmsymgreqlem2  18559  mndodcong  18670  subgabl  18956  gex2abl  18971  cntzsubr  19568  abvres  19610  lbsind2  19853  lspsneu  19895  lbsextlem2  19931  lbsextg  19934  lindfind2  20962  matring  21052  maducoeval  21248  maducoeval2  21249  maduf  21250  madurid  21253  gsummatr01  21268  cramerimplem3  21294  cnprest  21897  hausnei2  21961  isreg2  21985  cmpcld  22010  llyrest  22093  nllyrest  22094  csdfil  22502  hausflimlem  22587  ssblps  23032  ssbl  23033  cphassi  23818  cphassir  23819  4cphipval2  23845  cphipval  23846  dvres2  24510  plyadd  24807  plymul  24808  coeeu  24815  vieta1  24901  aalioulem3  24923  aalioulem4  24924  efgh  25125  cxpadd  25262  cxpsub  25265  mulcxp  25268  divcxp  25270  cxple2  25280  cxplt2  25281  cxpcn3lem  25328  angcan  25380  ang180lem5  25391  isosctrlem3  25398  logexprlim  25801  lgssq  25913  abvcxp  26191  padicabv  26206  brbtwn2  26691  ax5seglem6  26720  axcontlem4  26753  axcontlem8  26757  uhgr2edg  26990  nbgrisvtx  27123  nbupgrres  27146  clwwlkccat  27768  clwwlknonex2lem2  27887  frgrreggt1  28172  chscllem4  29417  cshwrnid  30635  ogrpinvlt  30724  eqfunresadj  33004  poseq  33095  nosupbnd2lem1  33215  noetalem5  33221  ifscgr  33505  matunitlindflem1  34903  lshpnelb  36135  lfl1  36221  lshpkrlem6  36266  lshpkrex  36269  hlrelat3  36563  atbtwnexOLDN  36598  atbtwnex  36599  3dim3  36620  3atlem5  36638  2llnmat  36675  lvolex3N  36689  lvolnle3at  36733  4atlem11  36760  4atlem12  36763  dalemccea  36834  cdlema2N  36943  paddasslem2  36972  atmod1i1m  37009  lhp2lt  37152  lhp0lt  37154  lhpj1  37173  lhpmcvr4N  37177  lhpelim  37188  lhpmod2i2  37189  lhpmod6i1  37190  cdlemb2  37192  lhple  37193  lhpat  37194  4atex  37227  4atex2-0aOLDN  37229  4atex3  37232  ldilco  37267  ltrncl  37276  ltrn11  37277  ltrnle  37280  ltrncnvleN  37281  ltrnm  37282  ltrnj  37283  ltrncvr  37284  ltrnatb  37288  ltrnel  37290  ltrncnvel  37293  ltrncnv  37297  trlval2  37314  trlcnv  37316  trljat1  37317  trljat2  37318  trl0  37321  ltrnnidn  37325  trlnidatb  37328  cdlemc1  37342  cdlemc2  37343  cdlemc5  37346  cdlemc6  37347  cdlemd3  37351  cdlemd6  37354  cdleme0aa  37361  cdleme0b  37363  cdleme0c  37364  cdleme0e  37368  cdleme0fN  37369  cdleme01N  37372  cdleme02N  37373  cdleme0ex1N  37374  cdleme0moN  37376  cdleme3g  37385  cdleme3h  37386  cdleme3  37388  cdleme4  37389  cdleme4a  37390  cdleme5  37391  cdleme8  37401  cdleme9  37404  cdleme10  37405  cdleme16aN  37410  cdleme11a  37411  cdleme11fN  37415  cdleme11g  37416  cdleme11h  37417  cdleme11j  37418  cdleme11k  37419  cdleme12  37422  cdleme13  37423  cdleme17c  37439  cdleme17d1  37440  cdleme18a  37442  cdleme18b  37443  cdleme18c  37444  cdleme22gb  37445  cdlemeda  37449  cdlemednpq  37450  cdlemednuN  37451  cdleme19c  37456  cdleme20aN  37460  cdleme20bN  37461  cdleme20c  37462  cdleme22aa  37490  cdleme22a  37491  cdleme22b  37492  cdleme22d  37494  cdleme22e  37495  cdleme27cl  37517  cdleme27a  37518  cdleme30a  37529  cdleme42a  37622  cdleme42c  37623  cdleme50laut  37698  cdlemf1  37712  cdlemf  37714  cdlemfnid  37715  trlord  37720  cdlemg2fv2  37751  cdlemg2kq  37753  cdlemg2m  37755  cdlemg4a  37759  cdlemg4d  37764  cdlemg4g  37767  cdlemg4  37768  cdlemg6c  37771  cdlemg7aN  37776  cdlemg8a  37778  cdlemg8b  37779  cdlemg8c  37780  cdlemg9a  37783  cdlemg9b  37784  cdlemg9  37785  cdlemg11aq  37789  cdlemg10c  37790  cdlemg12a  37794  cdlemg12b  37795  cdlemg12c  37796  cdlemg17a  37812  cdlemg18b  37830  cdlemg18c  37831  cdlemg31b0a  37846  cdlemg31a  37848  cdlemg31b  37849  cdlemg31d  37851  cdlemg35  37864  trlcoabs2N  37873  trlcolem  37877  cdlemg44a  37882  trljco  37891  trljco2  37892  tendoco2  37919  tendopltp  37931  cdlemi1  37969  cdlemi2  37970  cdlemj3  37974  tendocan  37975  cdlemk3  37984  cdlemk4  37985  cdlemk5a  37986  cdlemk9  37990  cdlemk9bN  37991  cdlemkvcl  37993  cdlemk10  37994  cdlemk30  38045  cdlemk31  38047  cdlemk39  38067  cdlemkfid1N  38072  cdlemkid1  38073  cdlemkid2  38075  cdlemkfid3N  38076  cdlemk19ylem  38081  cdlemk19xlem  38093  cdlemk19x  38094  cdlemk53b  38107  cdlemk53  38108  cdlemk54  38109  cdlemk55a  38110  cdlemk43N  38114  cdlemk19u1  38120  cdlemk19u  38121  cdleml1N  38127  erngdvlem4  38142  erngdvlem4-rN  38150  dia11N  38199  cdlemm10N  38269  dib11N  38311  cdlemn2  38346  cdlemn10  38357  dihjustlem  38367  dihord2cN  38372  dihlsscpre  38385  dih1dimb2  38392  dihvalcq2  38398  dihopelvalcpre  38399  dihord6b  38411  dih11  38416  dihmeetlem1N  38441  dihglblem2N  38445  dihglblem3N  38446  dihmeetlem2N  38450  dihglbcpreN  38451  dihmeetcN  38453  dihmeetbclemN  38455  dihmeetlem4preN  38457  dihmeetlem9N  38466  dihmeetlem20N  38477  dihlspsnssN  38483  dihlspsnat  38484  dihatlat  38485  dihglblem6  38491  dihmeet  38494  dochss  38516  hdmapval3N  38989  hgmap11  39053  nn0rppwr  39202  remulcand  39270  congtr  39582  fzmaxdif  39598  isnumbasgrplem2  39724  ntrclsk13  40441  ssmapsn  41499  infleinf  41660  suplesup2  41664  supxrunb3  41692  mullimc  41917  mullimcf  41924  islpcn  41940  limsupresxr  42067  liminfresxr  42068  cncfuni  42189  icccncfext  42190  stoweidlem34  42339  stoweidlem59  42364  stirlinglem13  42391  fourierdlem41  42453  fourierdlem42  42454  fourierdlem73  42484  sge0iunmptlemfi  42715  meadjiunlem  42767  ovncvrrp  42866  sssmf  43035  smflimsuplem7  43120  smflimsuplem8  43121  funressneu  43302  lincscm  44505  lincext3  44531  el0ldep  44541  el0ldepsnzr  44542  itscnhlc0xyqsol  44772