Theorem simp1l 1216

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp11l  1303  simp21l  1309  simp31l  1315  2f1fvneq  7287  eqfunresadj  7393  tfisi  7894  offsplitfpar  8157  poseq  8202  omeulem2  8619  uniinqs  8846  unxpdomlem3  9277  elfiun  9449  cantnffval  9691  tcrank  9928  cofsmo  10374  isfin2-2  10424  tskint  10897  tskun  10898  tskurn  10901  gruina  10930  dedekind  11500  subaddmulsub  11806  dmdcan  12054  lt2msq1  12228  supmullem1  12314  supmul  12316  xaddass  13406  xaddass2  13407  xlt2add  13417  xmulasslem3  13443  xadddi2r  13455  iccsplit  13643  expaddzlem  14275  expaddz  14276  expmulz  14278  ccatopth2  14894  pfxccat3  14911  resqrtcl  15449  limsupgle  15673  o1add  15810  o1mul  15811  o1sub  15812  bitsfzo  16634  sadfval  16651  smufval  16676  nn0rppwr  16764  prmexpb  16924  4sqlem18  17169  vdwlem10  17197  fsets  17376  setsstruct2  17381  submre  17804  mrelatlub  18765  chnccat  18829  gsmsymgreqlem2  19675  mndodcong  19786  subgabl  20080  gex2abl  20095  ogrpinvlt  20388  rng1zrlem  20433  cntzsubrng  20849  cntzsubr  20888  abvres  21118  lbsind2  21386  lspsneu  21431  lbsextlem2  21467  lbsextg  21470  lindfind2  22154  matring  22788  maducoeval  22984  maducoeval2  22985  maduf  22986  madurid  22989  gsummatr01  23004  matunitlindflem1  23024  cramerimplem3  23033  cnprest  23637  hausnei2  23701  isreg2  23725  cmpcld  23750  llyrest  23834  nllyrest  23835  csdfil  24243  hausflimlem  24328  ssblps  24771  ssbl  24772  cphassi  25565  cphassir  25566  4cphipval2  25593  cphipval  25594  dvres2  26262  plyadd  26566  plymul  26567  coeeu  26574  vieta1  26665  aalioulem3  26691  aalioulem4  26692  efgh  26899  cxpadd  27037  cxpsub  27040  mulcxp  27043  divcxp  27045  cxple2  27055  cxplt2  27056  cxpcn3lem  27105  angcan  27160  ang180lem5  27171  isosctrlem3  27178  logexprlim  27582  lgssq  27694  abvcxp  27972  padicabv  27987  nosupbnd2lem1  28102  noinfbnd2lem1  28117  nosupinfsep  28119  noetalem1  28128  ltmuls2  28587  brbtwn2  29513  ax5seglem6  29542  axcontlem4  29575  axcontlem8  29579  uhgr2edg  29819  nbgrisvtx  29952  nbupgrres  29975  clwwlkccat  30611  clwwlknonex2lem2  30729  frgrreggt1  31024  chscllem4  32272  cshwrnid  33592  ifscgr  36987  lshpnelb  40233  lfl1  40319  lshpkrlem6  40364  lshpkrex  40367  hlrelat3  40661  atbtwnexOLDN  40696  atbtwnex  40697  3dim3  40718  3atlem5  40736  2llnmat  40773  lvolex3N  40787  lvolnle3at  40831  4atlem11  40858  4atlem12  40861  dalemccea  40932  cdlema2N  41041  paddasslem2  41070  atmod1i1m  41107  lhp2lt  41250  lhp0lt  41252  lhpj1  41271  lhpmcvr4N  41275  lhpelim  41286  lhpmod2i2  41287  lhpmod6i1  41288  cdlemb2  41290  lhple  41291  lhpat  41292  4atex  41325  4atex2-0aOLDN  41327  4atex3  41330  ldilco  41365  ltrncl  41374  ltrn11  41375  ltrnle  41378  ltrncnvleN  41379  ltrnm  41380  ltrnj  41381  ltrncvr  41382  ltrnatb  41386  ltrnel  41388  ltrncnvel  41391  ltrncnv  41395  trlval2  41412  trlcnv  41414  trljat1  41415  trljat2  41416  trl0  41419  ltrnnidn  41423  trlnidatb  41426  cdlemc1  41440  cdlemc2  41441  cdlemc5  41444  cdlemc6  41445  cdlemd3  41449  cdlemd6  41452  cdleme0aa  41459  cdleme0b  41461  cdleme0c  41462  cdleme0e  41466  cdleme0fN  41467  cdleme01N  41470  cdleme02N  41471  cdleme0ex1N  41472  cdleme0moN  41474  cdleme3g  41483  cdleme3h  41484  cdleme3  41486  cdleme4  41487  cdleme4a  41488  cdleme5  41489  cdleme8  41499  cdleme9  41502  cdleme10  41503  cdleme16aN  41508  cdleme11a  41509  cdleme11fN  41513  cdleme11g  41514  cdleme11h  41515  cdleme11j  41516  cdleme11k  41517  cdleme12  41520  cdleme13  41521  cdleme17c  41537  cdleme17d1  41538  cdleme18a  41540  cdleme18b  41541  cdleme18c  41542  cdleme22gb  41543  cdlemeda  41547  cdlemednpq  41548  cdlemednuN  41549  cdleme19c  41554  cdleme20aN  41558  cdleme20bN  41559  cdleme20c  41560  cdleme22aa  41588  cdleme22a  41589  cdleme22b  41590  cdleme22d  41592  cdleme22e  41593  cdleme27cl  41615  cdleme27a  41616  cdleme30a  41627  cdleme42a  41720  cdleme42c  41721  cdleme50laut  41796  cdlemf1  41810  cdlemf  41812  cdlemfnid  41813  trlord  41818  cdlemg2fv2  41849  cdlemg2kq  41851  cdlemg2m  41853  cdlemg4a  41857  cdlemg4d  41862  cdlemg4g  41865  cdlemg4  41866  cdlemg6c  41869  cdlemg7aN  41874  cdlemg8a  41876  cdlemg8b  41877  cdlemg8c  41878  cdlemg9a  41881  cdlemg9b  41882  cdlemg9  41883  cdlemg11aq  41887  cdlemg10c  41888  cdlemg12a  41892  cdlemg12b  41893  cdlemg12c  41894  cdlemg17a  41910  cdlemg18b  41928  cdlemg18c  41929  cdlemg31b0a  41944  cdlemg31a  41946  cdlemg31b  41947  cdlemg31d  41949  cdlemg35  41962  trlcoabs2N  41971  trlcolem  41975  cdlemg44a  41980  trljco  41989  trljco2  41990  tendoco2  42017  tendopltp  42029  cdlemi1  42067  cdlemi2  42068  cdlemj3  42072  tendocan  42073  cdlemk3  42082  cdlemk4  42083  cdlemk5a  42084  cdlemk9  42088  cdlemk9bN  42089  cdlemkvcl  42091  cdlemk10  42092  cdlemk30  42143  cdlemk31  42145  cdlemk39  42165  cdlemkfid1N  42170  cdlemkid1  42171  cdlemkid2  42173  cdlemkfid3N  42174  cdlemk19ylem  42179  cdlemk19xlem  42191  cdlemk19x  42192  cdlemk53b  42205  cdlemk53  42206  cdlemk54  42207  cdlemk55a  42208  cdlemk43N  42212  cdlemk19u1  42218  cdlemk19u  42219  cdleml1N  42225  erngdvlem4  42240  erngdvlem4-rN  42248  dia11N  42297  cdlemm10N  42367  dib11N  42409  cdlemn2  42444  cdlemn10  42455  dihjustlem  42465  dihord2cN  42470  dihlsscpre  42483  dih1dimb2  42490  dihvalcq2  42496  dihopelvalcpre  42497  dihord6b  42509  dih11  42514  dihmeetlem1N  42539  dihglblem2N  42543  dihglblem3N  42544  dihmeetlem2N  42548  dihglbcpreN  42549  dihmeetcN  42551  dihmeetbclemN  42553  dihmeetlem4preN  42555  dihmeetlem9N  42564  dihmeetlem20N  42575  dihlspsnssN  42581  dihlspsnat  42582  dihatlat  42583  dihglblem6  42589  dihmeet  42592  dochss  42614  hdmapval3N  43087  hgmap11  43151  remulcand  43683  congtr  44165  fzmaxdif  44181  isnumbasgrplem2  44298  ntrclsk13  45263  ssmapsn  46434  infleinf  46588  suplesup2  46592  supxrunb3  46615  mullimc  46833  mullimcf  46840  islpcn  46854  limsupresxr  46981  liminfresxr  46982  cncfuni  47101  icccncfext  47102  stoweidlem34  47249  stoweidlem59  47274  stirlinglem13  47301  fourierdlem41  47363  fourierdlem42  47364  fourierdlem73  47394  sge0iunmptlemfi  47628  meadjiunlem  47680  ovncvrrp  47779  sssmf  47953  smflimsuplem7  48041  smflimsuplem8  48042  ormkglobd  48092  funressneu  48322  grlimedgclnbgr  49298  lincscm  49747  lincext3  49773  el0ldep  49783  el0ldepsnzr  49784  itscnhlc0xyqsol  50082  uptr2  50542