Theorem simp1l 1199

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 1134	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp11l  1286  simp21l  1292  simp31l  1298  2f1fvneq  7208  eqfunresadj  7308  tfisi  7803  offsplitfpar  8062  poseq  8101  omeulem2  8511  uniinqs  8737  unxpdomlem3  9161  elfiun  9336  cantnffval  9575  tcrank  9799  cofsmo  10182  isfin2-2  10232  tskint  10699  tskun  10700  tskurn  10703  gruina  10732  dedekind  11300  subaddmulsub  11604  dmdcan  11856  lt2msq1  12031  supmullem1  12117  supmul  12119  xaddass  13192  xaddass2  13193  xlt2add  13203  xmulasslem3  13229  xadddi2r  13241  iccsplit  13429  expaddzlem  14058  expaddz  14059  expmulz  14061  ccatopth2  14670  pfxccat3  14687  resqrtcl  15206  limsupgle  15430  o1add  15567  o1mul  15568  o1sub  15569  bitsfzo  16395  sadfval  16412  smufval  16437  nn0rppwr  16521  prmexpb  16680  4sqlem18  16924  vdwlem10  16952  fsets  17130  setsstruct2  17135  submre  17558  mrelatlub  18519  chnccat  18583  gsmsymgreqlem2  19397  mndodcong  19508  subgabl  19802  gex2abl  19817  ogrpinvlt  20110  cntzsubrng  20535  cntzsubr  20574  abvres  20799  lbsind2  21068  lspsneu  21113  lbsextlem2  21149  lbsextg  21152  lindfind2  21808  matring  22418  maducoeval  22614  maducoeval2  22615  maduf  22616  madurid  22619  gsummatr01  22634  cramerimplem3  22660  cnprest  23264  hausnei2  23328  isreg2  23352  cmpcld  23377  llyrest  23460  nllyrest  23461  csdfil  23869  hausflimlem  23954  ssblps  24397  ssbl  24398  cphassi  25191  cphassir  25192  4cphipval2  25219  cphipval  25220  dvres2  25889  plyadd  26192  plymul  26193  coeeu  26200  vieta1  26289  aalioulem3  26311  aalioulem4  26312  efgh  26518  cxpadd  26656  cxpsub  26659  mulcxp  26662  divcxp  26664  cxple2  26674  cxplt2  26675  cxpcn3lem  26724  angcan  26779  ang180lem5  26790  isosctrlem3  26797  logexprlim  27202  lgssq  27314  abvcxp  27592  padicabv  27607  nosupbnd2lem1  27693  noinfbnd2lem1  27708  nosupinfsep  27710  noetalem1  27719  ltmuls2  28177  brbtwn2  28988  ax5seglem6  29017  axcontlem4  29050  axcontlem8  29054  uhgr2edg  29291  nbgrisvtx  29424  nbupgrres  29447  clwwlkccat  30075  clwwlknonex2lem2  30193  frgrreggt1  30478  chscllem4  31726  cshwrnid  33036  ifscgr  36242  matunitlindflem1  37951  lshpnelb  39444  lfl1  39530  lshpkrlem6  39575  lshpkrex  39578  hlrelat3  39872  atbtwnexOLDN  39907  atbtwnex  39908  3dim3  39929  3atlem5  39947  2llnmat  39984  lvolex3N  39998  lvolnle3at  40042  4atlem11  40069  4atlem12  40072  dalemccea  40143  cdlema2N  40252  paddasslem2  40281  atmod1i1m  40318  lhp2lt  40461  lhp0lt  40463  lhpj1  40482  lhpmcvr4N  40486  lhpelim  40497  lhpmod2i2  40498  lhpmod6i1  40499  cdlemb2  40501  lhple  40502  lhpat  40503  4atex  40536  4atex2-0aOLDN  40538  4atex3  40541  ldilco  40576  ltrncl  40585  ltrn11  40586  ltrnle  40589  ltrncnvleN  40590  ltrnm  40591  ltrnj  40592  ltrncvr  40593  ltrnatb  40597  ltrnel  40599  ltrncnvel  40602  ltrncnv  40606  trlval2  40623  trlcnv  40625  trljat1  40626  trljat2  40627  trl0  40630  ltrnnidn  40634  trlnidatb  40637  cdlemc1  40651  cdlemc2  40652  cdlemc5  40655  cdlemc6  40656  cdlemd3  40660  cdlemd6  40663  cdleme0aa  40670  cdleme0b  40672  cdleme0c  40673  cdleme0e  40677  cdleme0fN  40678  cdleme01N  40681  cdleme02N  40682  cdleme0ex1N  40683  cdleme0moN  40685  cdleme3g  40694  cdleme3h  40695  cdleme3  40697  cdleme4  40698  cdleme4a  40699  cdleme5  40700  cdleme8  40710  cdleme9  40713  cdleme10  40714  cdleme16aN  40719  cdleme11a  40720  cdleme11fN  40724  cdleme11g  40725  cdleme11h  40726  cdleme11j  40727  cdleme11k  40728  cdleme12  40731  cdleme13  40732  cdleme17c  40748  cdleme17d1  40749  cdleme18a  40751  cdleme18b  40752  cdleme18c  40753  cdleme22gb  40754  cdlemeda  40758  cdlemednpq  40759  cdlemednuN  40760  cdleme19c  40765  cdleme20aN  40769  cdleme20bN  40770  cdleme20c  40771  cdleme22aa  40799  cdleme22a  40800  cdleme22b  40801  cdleme22d  40803  cdleme22e  40804  cdleme27cl  40826  cdleme27a  40827  cdleme30a  40838  cdleme42a  40931  cdleme42c  40932  cdleme50laut  41007  cdlemf1  41021  cdlemf  41023  cdlemfnid  41024  trlord  41029  cdlemg2fv2  41060  cdlemg2kq  41062  cdlemg2m  41064  cdlemg4a  41068  cdlemg4d  41073  cdlemg4g  41076  cdlemg4  41077  cdlemg6c  41080  cdlemg7aN  41085  cdlemg8a  41087  cdlemg8b  41088  cdlemg8c  41089  cdlemg9a  41092  cdlemg9b  41093  cdlemg9  41094  cdlemg11aq  41098  cdlemg10c  41099  cdlemg12a  41103  cdlemg12b  41104  cdlemg12c  41105  cdlemg17a  41121  cdlemg18b  41139  cdlemg18c  41140  cdlemg31b0a  41155  cdlemg31a  41157  cdlemg31b  41158  cdlemg31d  41160  cdlemg35  41173  trlcoabs2N  41182  trlcolem  41186  cdlemg44a  41191  trljco  41200  trljco2  41201  tendoco2  41228  tendopltp  41240  cdlemi1  41278  cdlemi2  41279  cdlemj3  41283  tendocan  41284  cdlemk3  41293  cdlemk4  41294  cdlemk5a  41295  cdlemk9  41299  cdlemk9bN  41300  cdlemkvcl  41302  cdlemk10  41303  cdlemk30  41354  cdlemk31  41356  cdlemk39  41376  cdlemkfid1N  41381  cdlemkid1  41382  cdlemkid2  41384  cdlemkfid3N  41385  cdlemk19ylem  41390  cdlemk19xlem  41402  cdlemk19x  41403  cdlemk53b  41416  cdlemk53  41417  cdlemk54  41418  cdlemk55a  41419  cdlemk43N  41423  cdlemk19u1  41429  cdlemk19u  41430  cdleml1N  41436  erngdvlem4  41451  erngdvlem4-rN  41459  dia11N  41508  cdlemm10N  41578  dib11N  41620  cdlemn2  41655  cdlemn10  41666  dihjustlem  41676  dihord2cN  41681  dihlsscpre  41694  dih1dimb2  41701  dihvalcq2  41707  dihopelvalcpre  41708  dihord6b  41720  dih11  41725  dihmeetlem1N  41750  dihglblem2N  41754  dihglblem3N  41755  dihmeetlem2N  41759  dihglbcpreN  41760  dihmeetcN  41762  dihmeetbclemN  41764  dihmeetlem4preN  41766  dihmeetlem9N  41775  dihmeetlem20N  41786  dihlspsnssN  41792  dihlspsnat  41793  dihatlat  41794  dihglblem6  41800  dihmeet  41803  dochss  41825  hdmapval3N  42298  hgmap11  42362  remulcand  42885  congtr  43411  fzmaxdif  43427  isnumbasgrplem2  43550  ntrclsk13  44516  ssmapsn  45663  infleinf  45819  suplesup2  45823  supxrunb3  45846  mullimc  46064  mullimcf  46071  islpcn  46085  limsupresxr  46212  liminfresxr  46213  cncfuni  46332  icccncfext  46333  stoweidlem34  46480  stoweidlem59  46505  stirlinglem13  46532  fourierdlem41  46594  fourierdlem42  46595  fourierdlem73  46625  sge0iunmptlemfi  46859  meadjiunlem  46911  ovncvrrp  47010  sssmf  47184  smflimsuplem7  47272  smflimsuplem8  47273  ormkglobd  47321  funressneu  47507  grlimedgclnbgr  48483  lincscm  48918  lincext3  48944  el0ldep  48954  el0ldepsnzr  48955  itscnhlc0xyqsol  49253  uptr2  49708