Theorem simp1l 1210

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  simp11l  1297  simp21l  1303  simp31l  1309  2f1fvneq  7240  eqfunresadj  7340  tfisi  7835  offsplitfpar  8093  poseq  8133  omeulem2  8547  uniinqs  8774  unxpdomlem3  9198  elfiun  9373  cantnffval  9615  tcrank  9839  cofsmo  10223  isfin2-2  10273  tskint  10740  tskun  10741  tskurn  10744  gruina  10773  dedekind  11343  subaddmulsub  11647  dmdcan  11898  lt2msq1  12073  supmullem1  12159  supmul  12161  xaddass  13249  xaddass2  13250  xlt2add  13260  xmulasslem3  13286  xadddi2r  13298  iccsplit  13486  expaddzlem  14115  expaddz  14116  expmulz  14118  ccatopth2  14727  pfxccat3  14744  resqrtcl  15263  limsupgle  15487  o1add  15624  o1mul  15625  o1sub  15626  bitsfzo  16452  sadfval  16469  smufval  16494  nn0rppwr  16578  prmexpb  16737  4sqlem18  16981  vdwlem10  17009  fsets  17188  setsstruct2  17193  submre  17616  mrelatlub  18577  chnccat  18641  gsmsymgreqlem2  19454  mndodcong  19565  subgabl  19859  gex2abl  19874  ogrpinvlt  20167  cntzsubrng  20596  cntzsubr  20635  abvres  20860  lbsind2  21128  lspsneu  21173  lbsextlem2  21209  lbsextg  21212  lindfind2  21850  matring  22483  maducoeval  22679  maducoeval2  22680  maduf  22681  madurid  22684  gsummatr01  22699  cramerimplem3  22725  cnprest  23329  hausnei2  23393  isreg2  23417  cmpcld  23442  llyrest  23525  nllyrest  23526  csdfil  23934  hausflimlem  24019  ssblps  24462  ssbl  24463  cphassi  25256  cphassir  25257  4cphipval2  25284  cphipval  25285  dvres2  25954  plyadd  26257  plymul  26258  coeeu  26265  vieta1  26353  aalioulem3  26375  aalioulem4  26376  efgh  26583  cxpadd  26721  cxpsub  26724  mulcxp  26727  divcxp  26729  cxple2  26739  cxplt2  26740  cxpcn3lem  26789  angcan  26844  ang180lem5  26855  isosctrlem3  26862  logexprlim  27266  lgssq  27378  abvcxp  27656  padicabv  27671  nosupbnd2lem1  27756  noinfbnd2lem1  27771  nosupinfsep  27773  noetalem1  27782  ltmuls2  28241  brbtwn2  29052  ax5seglem6  29081  axcontlem4  29114  axcontlem8  29118  uhgr2edg  29355  nbgrisvtx  29488  nbupgrres  29511  clwwlkccat  30138  clwwlknonex2lem2  30256  frgrreggt1  30541  chscllem4  31789  cshwrnid  33100  ifscgr  36358  matunitlindflem1  38079  lshpnelb  39572  lfl1  39658  lshpkrlem6  39703  lshpkrex  39706  hlrelat3  40000  atbtwnexOLDN  40035  atbtwnex  40036  3dim3  40057  3atlem5  40075  2llnmat  40112  lvolex3N  40126  lvolnle3at  40170  4atlem11  40197  4atlem12  40200  dalemccea  40271  cdlema2N  40380  paddasslem2  40409  atmod1i1m  40446  lhp2lt  40589  lhp0lt  40591  lhpj1  40610  lhpmcvr4N  40614  lhpelim  40625  lhpmod2i2  40626  lhpmod6i1  40627  cdlemb2  40629  lhple  40630  lhpat  40631  4atex  40664  4atex2-0aOLDN  40666  4atex3  40669  ldilco  40704  ltrncl  40713  ltrn11  40714  ltrnle  40717  ltrncnvleN  40718  ltrnm  40719  ltrnj  40720  ltrncvr  40721  ltrnatb  40725  ltrnel  40727  ltrncnvel  40730  ltrncnv  40734  trlval2  40751  trlcnv  40753  trljat1  40754  trljat2  40755  trl0  40758  ltrnnidn  40762  trlnidatb  40765  cdlemc1  40779  cdlemc2  40780  cdlemc5  40783  cdlemc6  40784  cdlemd3  40788  cdlemd6  40791  cdleme0aa  40798  cdleme0b  40800  cdleme0c  40801  cdleme0e  40805  cdleme0fN  40806  cdleme01N  40809  cdleme02N  40810  cdleme0ex1N  40811  cdleme0moN  40813  cdleme3g  40822  cdleme3h  40823  cdleme3  40825  cdleme4  40826  cdleme4a  40827  cdleme5  40828  cdleme8  40838  cdleme9  40841  cdleme10  40842  cdleme16aN  40847  cdleme11a  40848  cdleme11fN  40852  cdleme11g  40853  cdleme11h  40854  cdleme11j  40855  cdleme11k  40856  cdleme12  40859  cdleme13  40860  cdleme17c  40876  cdleme17d1  40877  cdleme18a  40879  cdleme18b  40880  cdleme18c  40881  cdleme22gb  40882  cdlemeda  40886  cdlemednpq  40887  cdlemednuN  40888  cdleme19c  40893  cdleme20aN  40897  cdleme20bN  40898  cdleme20c  40899  cdleme22aa  40927  cdleme22a  40928  cdleme22b  40929  cdleme22d  40931  cdleme22e  40932  cdleme27cl  40954  cdleme27a  40955  cdleme30a  40966  cdleme42a  41059  cdleme42c  41060  cdleme50laut  41135  cdlemf1  41149  cdlemf  41151  cdlemfnid  41152  trlord  41157  cdlemg2fv2  41188  cdlemg2kq  41190  cdlemg2m  41192  cdlemg4a  41196  cdlemg4d  41201  cdlemg4g  41204  cdlemg4  41205  cdlemg6c  41208  cdlemg7aN  41213  cdlemg8a  41215  cdlemg8b  41216  cdlemg8c  41217  cdlemg9a  41220  cdlemg9b  41221  cdlemg9  41222  cdlemg11aq  41226  cdlemg10c  41227  cdlemg12a  41231  cdlemg12b  41232  cdlemg12c  41233  cdlemg17a  41249  cdlemg18b  41267  cdlemg18c  41268  cdlemg31b0a  41283  cdlemg31a  41285  cdlemg31b  41286  cdlemg31d  41288  cdlemg35  41301  trlcoabs2N  41310  trlcolem  41314  cdlemg44a  41319  trljco  41328  trljco2  41329  tendoco2  41356  tendopltp  41368  cdlemi1  41406  cdlemi2  41407  cdlemj3  41411  tendocan  41412  cdlemk3  41421  cdlemk4  41422  cdlemk5a  41423  cdlemk9  41427  cdlemk9bN  41428  cdlemkvcl  41430  cdlemk10  41431  cdlemk30  41482  cdlemk31  41484  cdlemk39  41504  cdlemkfid1N  41509  cdlemkid1  41510  cdlemkid2  41512  cdlemkfid3N  41513  cdlemk19ylem  41518  cdlemk19xlem  41530  cdlemk19x  41531  cdlemk53b  41544  cdlemk53  41545  cdlemk54  41546  cdlemk55a  41547  cdlemk43N  41551  cdlemk19u1  41557  cdlemk19u  41558  cdleml1N  41564  erngdvlem4  41579  erngdvlem4-rN  41587  dia11N  41636  cdlemm10N  41706  dib11N  41748  cdlemn2  41783  cdlemn10  41794  dihjustlem  41804  dihord2cN  41809  dihlsscpre  41822  dih1dimb2  41829  dihvalcq2  41835  dihopelvalcpre  41836  dihord6b  41848  dih11  41853  dihmeetlem1N  41878  dihglblem2N  41882  dihglblem3N  41883  dihmeetlem2N  41887  dihglbcpreN  41888  dihmeetcN  41890  dihmeetbclemN  41892  dihmeetlem4preN  41894  dihmeetlem9N  41903  dihmeetlem20N  41914  dihlspsnssN  41920  dihlspsnat  41921  dihatlat  41922  dihglblem6  41928  dihmeet  41931  dochss  41953  hdmapval3N  42426  hgmap11  42490  remulcand  43012  congtr  43506  fzmaxdif  43522  isnumbasgrplem2  43645  ntrclsk13  44611  ssmapsn  45756  infleinf  45911  suplesup2  45915  supxrunb3  45938  mullimc  46156  mullimcf  46163  islpcn  46177  limsupresxr  46304  liminfresxr  46305  cncfuni  46424  icccncfext  46425  stoweidlem34  46572  stoweidlem59  46597  stirlinglem13  46624  fourierdlem41  46686  fourierdlem42  46687  fourierdlem73  46717  sge0iunmptlemfi  46951  meadjiunlem  47003  ovncvrrp  47102  sssmf  47276  smflimsuplem7  47364  smflimsuplem8  47365  ormkglobd  47415  funressneu  47605  grlimedgclnbgr  48581  lincscm  49016  lincext3  49042  el0ldep  49052  el0ldepsnzr  49053  itscnhlc0xyqsol  49351  uptr2  49806