Theorem simp1l 1194

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084

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 206  df-an 396  df-3an 1086

This theorem is referenced by:  simp11l  1281  simp21l  1287  simp31l  1293  eqfunresadj  7349  tfisi  7841  offsplitfpar  8099  poseq  8138  omeulem2  8578  uniinqs  8786  unxpdomlem3  9247  elfiun  9420  cantnffval  9653  tcrank  9874  cofsmo  10259  isfin2-2  10309  tskint  10775  tskun  10776  tskurn  10779  gruina  10808  dedekind  11373  subaddmulsub  11673  dmdcan  11920  lt2msq1  12094  supmullem1  12180  supmul  12182  xaddass  13224  xaddass2  13225  xlt2add  13235  xmulasslem3  13261  xadddi2r  13273  iccsplit  13458  expaddzlem  14067  expaddz  14068  expmulz  14070  ccatopth2  14663  pfxccat3  14680  resqrtcl  15196  limsupgle  15417  o1add  15554  o1mul  15555  o1sub  15556  bitsfzo  16372  sadfval  16389  smufval  16414  prmexpb  16653  4sqlem18  16891  vdwlem10  16919  fsets  17098  setsstruct2  17103  submre  17545  mrelatlub  18514  gsmsymgreqlem2  19336  mndodcong  19447  subgabl  19741  gex2abl  19756  cntzsubrng  20452  cntzsubr  20493  abvres  20667  lbsind2  20914  lspsneu  20959  lbsextlem2  20995  lbsextg  20998  lindfind2  21673  matring  22255  maducoeval  22451  maducoeval2  22452  maduf  22453  madurid  22456  gsummatr01  22471  cramerimplem3  22497  cnprest  23103  hausnei2  23167  isreg2  23191  cmpcld  23216  llyrest  23299  nllyrest  23300  csdfil  23708  hausflimlem  23793  ssblps  24238  ssbl  24239  cphassi  25052  cphassir  25053  4cphipval2  25080  cphipval  25081  dvres2  25751  plyadd  26059  plymul  26060  coeeu  26067  vieta1  26154  aalioulem3  26176  aalioulem4  26177  efgh  26380  cxpadd  26517  cxpsub  26520  mulcxp  26523  divcxp  26525  cxple2  26535  cxplt2  26536  cxpcn3lem  26586  angcan  26638  ang180lem5  26649  isosctrlem3  26656  logexprlim  27062  lgssq  27174  abvcxp  27452  padicabv  27467  nosupbnd2lem1  27552  noinfbnd2lem1  27567  nosupinfsep  27569  noetalem1  27578  sltmul2  27975  brbtwn2  28587  ax5seglem6  28616  axcontlem4  28649  axcontlem8  28653  uhgr2edg  28889  nbgrisvtx  29022  nbupgrres  29045  clwwlkccat  29667  clwwlknonex2lem2  29785  frgrreggt1  30070  chscllem4  31317  cshwrnid  32549  ogrpinvlt  32668  ifscgr  35477  matunitlindflem1  36940  lshpnelb  38310  lfl1  38396  lshpkrlem6  38441  lshpkrex  38444  hlrelat3  38739  atbtwnexOLDN  38774  atbtwnex  38775  3dim3  38796  3atlem5  38814  2llnmat  38851  lvolex3N  38865  lvolnle3at  38909  4atlem11  38936  4atlem12  38939  dalemccea  39010  cdlema2N  39119  paddasslem2  39148  atmod1i1m  39185  lhp2lt  39328  lhp0lt  39330  lhpj1  39349  lhpmcvr4N  39353  lhpelim  39364  lhpmod2i2  39365  lhpmod6i1  39366  cdlemb2  39368  lhple  39369  lhpat  39370  4atex  39403  4atex2-0aOLDN  39405  4atex3  39408  ldilco  39443  ltrncl  39452  ltrn11  39453  ltrnle  39456  ltrncnvleN  39457  ltrnm  39458  ltrnj  39459  ltrncvr  39460  ltrnatb  39464  ltrnel  39466  ltrncnvel  39469  ltrncnv  39473  trlval2  39490  trlcnv  39492  trljat1  39493  trljat2  39494  trl0  39497  ltrnnidn  39501  trlnidatb  39504  cdlemc1  39518  cdlemc2  39519  cdlemc5  39522  cdlemc6  39523  cdlemd3  39527  cdlemd6  39530  cdleme0aa  39537  cdleme0b  39539  cdleme0c  39540  cdleme0e  39544  cdleme0fN  39545  cdleme01N  39548  cdleme02N  39549  cdleme0ex1N  39550  cdleme0moN  39552  cdleme3g  39561  cdleme3h  39562  cdleme3  39564  cdleme4  39565  cdleme4a  39566  cdleme5  39567  cdleme8  39577  cdleme9  39580  cdleme10  39581  cdleme16aN  39586  cdleme11a  39587  cdleme11fN  39591  cdleme11g  39592  cdleme11h  39593  cdleme11j  39594  cdleme11k  39595  cdleme12  39598  cdleme13  39599  cdleme17c  39615  cdleme17d1  39616  cdleme18a  39618  cdleme18b  39619  cdleme18c  39620  cdleme22gb  39621  cdlemeda  39625  cdlemednpq  39626  cdlemednuN  39627  cdleme19c  39632  cdleme20aN  39636  cdleme20bN  39637  cdleme20c  39638  cdleme22aa  39666  cdleme22a  39667  cdleme22b  39668  cdleme22d  39670  cdleme22e  39671  cdleme27cl  39693  cdleme27a  39694  cdleme30a  39705  cdleme42a  39798  cdleme42c  39799  cdleme50laut  39874  cdlemf1  39888  cdlemf  39890  cdlemfnid  39891  trlord  39896  cdlemg2fv2  39927  cdlemg2kq  39929  cdlemg2m  39931  cdlemg4a  39935  cdlemg4d  39940  cdlemg4g  39943  cdlemg4  39944  cdlemg6c  39947  cdlemg7aN  39952  cdlemg8a  39954  cdlemg8b  39955  cdlemg8c  39956  cdlemg9a  39959  cdlemg9b  39960  cdlemg9  39961  cdlemg11aq  39965  cdlemg10c  39966  cdlemg12a  39970  cdlemg12b  39971  cdlemg12c  39972  cdlemg17a  39988  cdlemg18b  40006  cdlemg18c  40007  cdlemg31b0a  40022  cdlemg31a  40024  cdlemg31b  40025  cdlemg31d  40027  cdlemg35  40040  trlcoabs2N  40049  trlcolem  40053  cdlemg44a  40058  trljco  40067  trljco2  40068  tendoco2  40095  tendopltp  40107  cdlemi1  40145  cdlemi2  40146  cdlemj3  40150  tendocan  40151  cdlemk3  40160  cdlemk4  40161  cdlemk5a  40162  cdlemk9  40166  cdlemk9bN  40167  cdlemkvcl  40169  cdlemk10  40170  cdlemk30  40221  cdlemk31  40223  cdlemk39  40243  cdlemkfid1N  40248  cdlemkid1  40249  cdlemkid2  40251  cdlemkfid3N  40252  cdlemk19ylem  40257  cdlemk19xlem  40269  cdlemk19x  40270  cdlemk53b  40283  cdlemk53  40284  cdlemk54  40285  cdlemk55a  40286  cdlemk43N  40290  cdlemk19u1  40296  cdlemk19u  40297  cdleml1N  40303  erngdvlem4  40318  erngdvlem4-rN  40326  dia11N  40375  cdlemm10N  40445  dib11N  40487  cdlemn2  40522  cdlemn10  40533  dihjustlem  40543  dihord2cN  40548  dihlsscpre  40561  dih1dimb2  40568  dihvalcq2  40574  dihopelvalcpre  40575  dihord6b  40587  dih11  40592  dihmeetlem1N  40617  dihglblem2N  40621  dihglblem3N  40622  dihmeetlem2N  40626  dihglbcpreN  40627  dihmeetcN  40629  dihmeetbclemN  40631  dihmeetlem4preN  40633  dihmeetlem9N  40642  dihmeetlem20N  40653  dihlspsnssN  40659  dihlspsnat  40660  dihatlat  40661  dihglblem6  40667  dihmeet  40670  dochss  40692  hdmapval3N  41165  hgmap11  41229  nn0rppwr  41679  remulcand  41766  congtr  42159  fzmaxdif  42175  isnumbasgrplem2  42301  ntrclsk13  43277  ssmapsn  44366  infleinf  44533  suplesup2  44537  supxrunb3  44560  mullimc  44783  mullimcf  44790  islpcn  44806  limsupresxr  44933  liminfresxr  44934  cncfuni  45053  icccncfext  45054  stoweidlem34  45201  stoweidlem59  45226  stirlinglem13  45253  fourierdlem41  45315  fourierdlem42  45316  fourierdlem73  45346  sge0iunmptlemfi  45580  meadjiunlem  45632  ovncvrrp  45731  sssmf  45905  smflimsuplem7  45993  smflimsuplem8  45994  funressneu  46208  lincscm  47265  lincext3  47291  el0ldep  47301  el0ldepsnzr  47302  itscnhlc0xyqsol  47605