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  7264  eqfunresadj  7370  tfisi  7870  offsplitfpar  8132  poseq  8177  omeulem2  8594  uniinqs  8821  unxpdomlem3  9252  elfiun  9425  cantnffval  9667  tcrank  9904  cofsmo  10350  isfin2-2  10400  tskint  10873  tskun  10874  tskurn  10877  gruina  10906  dedekind  11476  subaddmulsub  11782  dmdcan  12030  lt2msq1  12204  supmullem1  12290  supmul  12292  xaddass  13382  xaddass2  13383  xlt2add  13393  xmulasslem3  13419  xadddi2r  13431  iccsplit  13619  expaddzlem  14251  expaddz  14252  expmulz  14254  ccatopth2  14870  pfxccat3  14887  resqrtcl  15425  limsupgle  15649  o1add  15786  o1mul  15787  o1sub  15788  bitsfzo  16610  sadfval  16627  smufval  16652  nn0rppwr  16740  prmexpb  16900  4sqlem18  17145  vdwlem10  17173  fsets  17352  setsstruct2  17357  submre  17780  mrelatlub  18741  chnccat  18805  gsmsymgreqlem2  19650  mndodcong  19761  subgabl  20055  gex2abl  20070  ogrpinvlt  20363  rng1zrlem  20408  cntzsubrng  20824  cntzsubr  20863  abvres  21093  lbsind2  21361  lspsneu  21406  lbsextlem2  21442  lbsextg  21445  lindfind2  22129  matring  22763  maducoeval  22959  maducoeval2  22960  maduf  22961  madurid  22964  gsummatr01  22979  matunitlindflem1  22999  cramerimplem3  23008  cnprest  23612  hausnei2  23676  isreg2  23700  cmpcld  23725  llyrest  23809  nllyrest  23810  csdfil  24218  hausflimlem  24303  ssblps  24746  ssbl  24747  cphassi  25540  cphassir  25541  4cphipval2  25568  cphipval  25569  dvres2  26237  plyadd  26541  plymul  26542  coeeu  26549  vieta1  26640  aalioulem3  26666  aalioulem4  26667  efgh  26874  cxpadd  27012  cxpsub  27015  mulcxp  27018  divcxp  27020  cxple2  27030  cxplt2  27031  cxpcn3lem  27080  angcan  27135  ang180lem5  27146  isosctrlem3  27153  logexprlim  27557  lgssq  27669  abvcxp  27947  padicabv  27962  nosupbnd2lem1  28077  noinfbnd2lem1  28092  nosupinfsep  28094  noetalem1  28103  ltmuls2  28562  brbtwn2  29488  ax5seglem6  29517  axcontlem4  29550  axcontlem8  29554  uhgr2edg  29794  nbgrisvtx  29927  nbupgrres  29950  clwwlkccat  30586  clwwlknonex2lem2  30704  frgrreggt1  30999  chscllem4  32247  cshwrnid  33568  ifscgr  36901  lshpnelb  40134  lfl1  40220  lshpkrlem6  40265  lshpkrex  40268  hlrelat3  40562  atbtwnexOLDN  40597  atbtwnex  40598  3dim3  40619  3atlem5  40637  2llnmat  40674  lvolex3N  40688  lvolnle3at  40732  4atlem11  40759  4atlem12  40762  dalemccea  40833  cdlema2N  40942  paddasslem2  40971  atmod1i1m  41008  lhp2lt  41151  lhp0lt  41153  lhpj1  41172  lhpmcvr4N  41176  lhpelim  41187  lhpmod2i2  41188  lhpmod6i1  41189  cdlemb2  41191  lhple  41192  lhpat  41193  4atex  41226  4atex2-0aOLDN  41228  4atex3  41231  ldilco  41266  ltrncl  41275  ltrn11  41276  ltrnle  41279  ltrncnvleN  41280  ltrnm  41281  ltrnj  41282  ltrncvr  41283  ltrnatb  41287  ltrnel  41289  ltrncnvel  41292  ltrncnv  41296  trlval2  41313  trlcnv  41315  trljat1  41316  trljat2  41317  trl0  41320  ltrnnidn  41324  trlnidatb  41327  cdlemc1  41341  cdlemc2  41342  cdlemc5  41345  cdlemc6  41346  cdlemd3  41350  cdlemd6  41353  cdleme0aa  41360  cdleme0b  41362  cdleme0c  41363  cdleme0e  41367  cdleme0fN  41368  cdleme01N  41371  cdleme02N  41372  cdleme0ex1N  41373  cdleme0moN  41375  cdleme3g  41384  cdleme3h  41385  cdleme3  41387  cdleme4  41388  cdleme4a  41389  cdleme5  41390  cdleme8  41400  cdleme9  41403  cdleme10  41404  cdleme16aN  41409  cdleme11a  41410  cdleme11fN  41414  cdleme11g  41415  cdleme11h  41416  cdleme11j  41417  cdleme11k  41418  cdleme12  41421  cdleme13  41422  cdleme17c  41438  cdleme17d1  41439  cdleme18a  41441  cdleme18b  41442  cdleme18c  41443  cdleme22gb  41444  cdlemeda  41448  cdlemednpq  41449  cdlemednuN  41450  cdleme19c  41455  cdleme20aN  41459  cdleme20bN  41460  cdleme20c  41461  cdleme22aa  41489  cdleme22a  41490  cdleme22b  41491  cdleme22d  41493  cdleme22e  41494  cdleme27cl  41516  cdleme27a  41517  cdleme30a  41528  cdleme42a  41621  cdleme42c  41622  cdleme50laut  41697  cdlemf1  41711  cdlemf  41713  cdlemfnid  41714  trlord  41719  cdlemg2fv2  41750  cdlemg2kq  41752  cdlemg2m  41754  cdlemg4a  41758  cdlemg4d  41763  cdlemg4g  41766  cdlemg4  41767  cdlemg6c  41770  cdlemg7aN  41775  cdlemg8a  41777  cdlemg8b  41778  cdlemg8c  41779  cdlemg9a  41782  cdlemg9b  41783  cdlemg9  41784  cdlemg11aq  41788  cdlemg10c  41789  cdlemg12a  41793  cdlemg12b  41794  cdlemg12c  41795  cdlemg17a  41811  cdlemg18b  41829  cdlemg18c  41830  cdlemg31b0a  41845  cdlemg31a  41847  cdlemg31b  41848  cdlemg31d  41850  cdlemg35  41863  trlcoabs2N  41872  trlcolem  41876  cdlemg44a  41881  trljco  41890  trljco2  41891  tendoco2  41918  tendopltp  41930  cdlemi1  41968  cdlemi2  41969  cdlemj3  41973  tendocan  41974  cdlemk3  41983  cdlemk4  41984  cdlemk5a  41985  cdlemk9  41989  cdlemk9bN  41990  cdlemkvcl  41992  cdlemk10  41993  cdlemk30  42044  cdlemk31  42046  cdlemk39  42066  cdlemkfid1N  42071  cdlemkid1  42072  cdlemkid2  42074  cdlemkfid3N  42075  cdlemk19ylem  42080  cdlemk19xlem  42092  cdlemk19x  42093  cdlemk53b  42106  cdlemk53  42107  cdlemk54  42108  cdlemk55a  42109  cdlemk43N  42113  cdlemk19u1  42119  cdlemk19u  42120  cdleml1N  42126  erngdvlem4  42141  erngdvlem4-rN  42149  dia11N  42198  cdlemm10N  42268  dib11N  42310  cdlemn2  42345  cdlemn10  42356  dihjustlem  42366  dihord2cN  42371  dihlsscpre  42384  dih1dimb2  42391  dihvalcq2  42397  dihopelvalcpre  42398  dihord6b  42410  dih11  42415  dihmeetlem1N  42440  dihglblem2N  42444  dihglblem3N  42445  dihmeetlem2N  42449  dihglbcpreN  42450  dihmeetcN  42452  dihmeetbclemN  42454  dihmeetlem4preN  42456  dihmeetlem9N  42465  dihmeetlem20N  42476  dihlspsnssN  42482  dihlspsnat  42483  dihatlat  42484  dihglblem6  42490  dihmeet  42493  dochss  42515  hdmapval3N  42988  hgmap11  43052  remulcand  43583  congtr  44065  fzmaxdif  44081  isnumbasgrplem2  44199  ntrclsk13  45164  ssmapsn  46322  infleinf  46476  suplesup2  46480  supxrunb3  46503  mullimc  46721  mullimcf  46728  islpcn  46742  limsupresxr  46869  liminfresxr  46870  cncfuni  46989  icccncfext  46990  stoweidlem34  47137  stoweidlem59  47162  stirlinglem13  47189  fourierdlem41  47251  fourierdlem42  47252  fourierdlem73  47282  sge0iunmptlemfi  47516  meadjiunlem  47568  ovncvrrp  47667  sssmf  47841  smflimsuplem7  47929  smflimsuplem8  47930  ormkglobd  47980  funressneu  48210  grlimedgclnbgr  49186  lincscm  49635  lincext3  49661  el0ldep  49671  el0ldepsnzr  49672  itscnhlc0xyqsol  49970  uptr2  50430