Theorem simp1l 1211

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 476	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	3ad2ant1 1124	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  simpl1lOLD  1251  simpr1lOLD  1263  simp11l  1340  simp21l  1346  simp31l  1352  tfisi  7336  omeulem2  7947  uniinqs  8110  unxpdomlem3  8454  elfiun  8624  cantnffval  8857  tcrank  9044  cofsmo  9426  isfin2-2  9476  tskint  9942  tskun  9943  tskurn  9946  gruina  9975  dedekind  10539  subaddmulsub  10838  dmdcan  11085  lt2msq1  11261  supmullem1  11347  supmul  11349  xaddass  12391  xaddass2  12392  xlt2add  12402  xmulasslem3  12428  xadddi2r  12440  iccsplit  12622  expaddzlem  13221  expaddz  13222  expmulz  13224  ccatopth2  13836  pfxccat3  13863  swrdccat3OLD  13864  resqrtcl  14401  limsupgle  14616  o1add  14752  o1mul  14753  o1sub  14754  bitsfzo  15563  sadfval  15580  smufval  15605  prmexpb  15834  4sqlem18  16070  vdwlem10  16098  fsets  16288  setsstruct2  16293  submre  16651  mrelatlub  17572  mndodcong  18345  subgabl  18627  gex2abl  18640  cntzsubr  19204  abvres  19231  lbsind2  19476  lspsneu  19518  lbsextlem2  19556  lbsextg  19559  lindfind2  20561  matring  20653  maducoeval  20850  maducoeval2  20851  maduf  20852  madurid  20855  gsummatr01  20871  cramerimplem3  20898  cnprest  21501  hausnei2  21565  isreg2  21589  cmpcld  21614  llyrest  21697  nllyrest  21698  csdfil  22106  hausflimlem  22191  ssblps  22635  ssbl  22636  cphassi  23421  cphassir  23422  4cphipval2  23448  cphipval  23449  dvres2  24113  plyadd  24410  plymul  24411  coeeu  24418  vieta1  24504  aalioulem3  24526  aalioulem4  24527  efgh  24725  cxpadd  24862  cxpsub  24865  mulcxp  24868  divcxp  24870  cxple2  24880  cxplt2  24881  cxpcn3lem  24928  angcan  24980  ang180lem5  24991  isosctrlem3  24998  logexprlim  25402  lgssq  25514  abvcxp  25756  padicabv  25771  brbtwn2  26254  ax5seglem6  26283  axcontlem4  26316  axcontlem8  26320  uhgr2edg  26554  nbgrisvtx  26688  nbupgrres  26711  clwwlkccat  27370  frgrreggt1  27825  chscllem4  29071  ogrpinvlt  30286  eqfunresadj  32252  poseq  32342  nosupbnd2lem1  32450  noetalem5  32456  ifscgr  32740  matunitlindflem1  34031  lshpnelb  35138  lfl1  35224  lshpkrlem6  35269  lshpkrex  35272  hlrelat3  35566  atbtwnexOLDN  35601  atbtwnex  35602  3dim3  35623  3atlem5  35641  2llnmat  35678  lvolex3N  35692  lvolnle3at  35736  4atlem11  35763  4atlem12  35766  dalemccea  35837  cdlema2N  35946  paddasslem2  35975  atmod1i1m  36012  lhp2lt  36155  lhp0lt  36157  lhpj1  36176  lhpmcvr4N  36180  lhpelim  36191  lhpmod2i2  36192  lhpmod6i1  36193  cdlemb2  36195  lhple  36196  lhpat  36197  4atex  36230  4atex2-0aOLDN  36232  4atex3  36235  ldilco  36270  ltrncl  36279  ltrn11  36280  ltrnle  36283  ltrncnvleN  36284  ltrnm  36285  ltrnj  36286  ltrncvr  36287  ltrnatb  36291  ltrnel  36293  ltrncnvel  36296  ltrncnv  36300  trlval2  36317  trlcnv  36319  trljat1  36320  trljat2  36321  trl0  36324  ltrnnidn  36328  trlnidatb  36331  cdlemc1  36345  cdlemc2  36346  cdlemc5  36349  cdlemc6  36350  cdlemd3  36354  cdlemd6  36357  cdleme0aa  36364  cdleme0b  36366  cdleme0c  36367  cdleme0e  36371  cdleme0fN  36372  cdleme01N  36375  cdleme02N  36376  cdleme0ex1N  36377  cdleme0moN  36379  cdleme3g  36388  cdleme3h  36389  cdleme3  36391  cdleme4  36392  cdleme4a  36393  cdleme5  36394  cdleme8  36404  cdleme9  36407  cdleme10  36408  cdleme16aN  36413  cdleme11a  36414  cdleme11fN  36418  cdleme11g  36419  cdleme11h  36420  cdleme11j  36421  cdleme11k  36422  cdleme12  36425  cdleme13  36426  cdleme17c  36442  cdleme17d1  36443  cdleme18a  36445  cdleme18b  36446  cdleme18c  36447  cdleme22gb  36448  cdlemeda  36452  cdlemednpq  36453  cdlemednuN  36454  cdleme19c  36459  cdleme20aN  36463  cdleme20bN  36464  cdleme20c  36465  cdleme22aa  36493  cdleme22a  36494  cdleme22b  36495  cdleme22d  36497  cdleme22e  36498  cdleme27cl  36520  cdleme27a  36521  cdleme30a  36532  cdleme42a  36625  cdleme42c  36626  cdleme50laut  36701  cdlemf1  36715  cdlemf  36717  cdlemfnid  36718  trlord  36723  cdlemg2fv2  36754  cdlemg2kq  36756  cdlemg2m  36758  cdlemg4a  36762  cdlemg4d  36767  cdlemg4g  36770  cdlemg4  36771  cdlemg6c  36774  cdlemg7aN  36779  cdlemg8a  36781  cdlemg8b  36782  cdlemg8c  36783  cdlemg9a  36786  cdlemg9b  36787  cdlemg9  36788  cdlemg11aq  36792  cdlemg10c  36793  cdlemg12a  36797  cdlemg12b  36798  cdlemg12c  36799  cdlemg17a  36815  cdlemg18b  36833  cdlemg18c  36834  cdlemg31b0a  36849  cdlemg31a  36851  cdlemg31b  36852  cdlemg31d  36854  cdlemg35  36867  trlcoabs2N  36876  trlcolem  36880  cdlemg44a  36885  trljco  36894  trljco2  36895  tendoco2  36922  tendopltp  36934  cdlemi1  36972  cdlemi2  36973  cdlemj3  36977  tendocan  36978  cdlemk3  36987  cdlemk4  36988  cdlemk5a  36989  cdlemk9  36993  cdlemk9bN  36994  cdlemkvcl  36996  cdlemk10  36997  cdlemk30  37048  cdlemk31  37050  cdlemk39  37070  cdlemkfid1N  37075  cdlemkid1  37076  cdlemkid2  37078  cdlemkfid3N  37079  cdlemk19ylem  37084  cdlemk19xlem  37096  cdlemk19x  37097  cdlemk53b  37110  cdlemk53  37111  cdlemk54  37112  cdlemk55a  37113  cdlemk43N  37117  cdlemk19u1  37123  cdlemk19u  37124  cdleml1N  37130  erngdvlem4  37145  erngdvlem4-rN  37153  dia11N  37202  cdlemm10N  37272  dib11N  37314  cdlemn2  37349  cdlemn10  37360  dihjustlem  37370  dihord2cN  37375  dihlsscpre  37388  dih1dimb2  37395  dihvalcq2  37401  dihopelvalcpre  37402  dihord6b  37414  dih11  37419  dihmeetlem1N  37444  dihglblem2N  37448  dihglblem3N  37449  dihmeetlem2N  37453  dihglbcpreN  37454  dihmeetcN  37456  dihmeetbclemN  37458  dihmeetlem4preN  37460  dihmeetlem9N  37469  dihmeetlem20N  37480  dihlspsnssN  37486  dihlspsnat  37487  dihatlat  37488  dihglblem6  37494  dihmeet  37497  dochss  37519  hdmapval3N  37992  hgmap11  38056  nn0rppwr  38162  congtr  38491  fzmaxdif  38507  isnumbasgrplem2  38633  ntrclsk13  39325  ssmapsn  40329  infleinf  40496  suplesup2  40500  supxrunb3  40529  mullimc  40756  mullimcf  40763  islpcn  40779  limsupresxr  40906  liminfresxr  40907  cncfuni  41027  icccncfext  41028  stoweidlem34  41178  stoweidlem59  41203  stirlinglem13  41230  fourierdlem41  41292  fourierdlem42  41293  fourierdlem73  41323  sge0iunmptlemfi  41554  meadjiunlem  41606  ovncvrrp  41705  sssmf  41874  smflimsuplem7  41959  smflimsuplem8  41960  funressneu  42112  lincscm  43234  lincext3  43260  el0ldep  43270  el0ldepsnzr  43271  itscnhlc0xyqsol  43501