Theorem simp1l 1214

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simp11l  1301  simp21l  1307  simp31l  1313  2f1fvneq  7248  eqfunresadj  7348  tfisi  7843  offsplitfpar  8102  poseq  8142  omeulem2  8556  uniinqs  8783  unxpdomlem3  9206  elfiun  9378  cantnffval  9620  tcrank  9844  cofsmo  10241  isfin2-2  10291  tskint  10758  tskun  10759  tskurn  10762  gruina  10791  dedekind  11361  subaddmulsub  11665  dmdcan  11916  lt2msq1  12090  supmullem1  12176  supmul  12178  xaddass  13266  xaddass2  13267  xlt2add  13277  xmulasslem3  13303  xadddi2r  13315  iccsplit  13503  expaddzlem  14132  expaddz  14133  expmulz  14135  ccatopth2  14744  pfxccat3  14761  resqrtcl  15294  limsupgle  15518  o1add  15655  o1mul  15656  o1sub  15657  bitsfzo  16483  sadfval  16500  smufval  16525  nn0rppwr  16609  prmexpb  16768  4sqlem18  17012  vdwlem10  17040  fsets  17219  setsstruct2  17224  submre  17647  mrelatlub  18608  chnccat  18672  gsmsymgreqlem2  19492  mndodcong  19603  subgabl  19897  gex2abl  19912  ogrpinvlt  20205  rng1zrlem  20250  cntzsubrng  20643  cntzsubr  20682  abvres  20903  lbsind2  21171  lspsneu  21216  lbsextlem2  21252  lbsextg  21255  lindfind2  21928  matring  22561  maducoeval  22757  maducoeval2  22758  maduf  22759  madurid  22762  gsummatr01  22777  cramerimplem3  22803  cnprest  23407  hausnei2  23471  isreg2  23495  cmpcld  23520  llyrest  23603  nllyrest  23604  csdfil  24012  hausflimlem  24097  ssblps  24540  ssbl  24541  cphassi  25334  cphassir  25335  4cphipval2  25362  cphipval  25363  dvres2  26032  plyadd  26335  plymul  26336  coeeu  26343  vieta1  26434  aalioulem3  26456  aalioulem4  26457  efgh  26664  cxpadd  26802  cxpsub  26805  mulcxp  26808  divcxp  26810  cxple2  26820  cxplt2  26821  cxpcn3lem  26870  angcan  26925  ang180lem5  26936  isosctrlem3  26943  logexprlim  27347  lgssq  27459  abvcxp  27737  padicabv  27752  nosupbnd2lem1  27837  noinfbnd2lem1  27852  nosupinfsep  27854  noetalem1  27863  ltmuls2  28322  brbtwn2  29164  ax5seglem6  29193  axcontlem4  29226  axcontlem8  29230  uhgr2edg  29467  nbgrisvtx  29600  nbupgrres  29623  clwwlkccat  30250  clwwlknonex2lem2  30368  frgrreggt1  30653  chscllem4  31901  cshwrnid  33194  ifscgr  36407  matunitlindflem1  38127  lshpnelb  39620  lfl1  39706  lshpkrlem6  39751  lshpkrex  39754  hlrelat3  40048  atbtwnexOLDN  40083  atbtwnex  40084  3dim3  40105  3atlem5  40123  2llnmat  40160  lvolex3N  40174  lvolnle3at  40218  4atlem11  40245  4atlem12  40248  dalemccea  40319  cdlema2N  40428  paddasslem2  40457  atmod1i1m  40494  lhp2lt  40637  lhp0lt  40639  lhpj1  40658  lhpmcvr4N  40662  lhpelim  40673  lhpmod2i2  40674  lhpmod6i1  40675  cdlemb2  40677  lhple  40678  lhpat  40679  4atex  40712  4atex2-0aOLDN  40714  4atex3  40717  ldilco  40752  ltrncl  40761  ltrn11  40762  ltrnle  40765  ltrncnvleN  40766  ltrnm  40767  ltrnj  40768  ltrncvr  40769  ltrnatb  40773  ltrnel  40775  ltrncnvel  40778  ltrncnv  40782  trlval2  40799  trlcnv  40801  trljat1  40802  trljat2  40803  trl0  40806  ltrnnidn  40810  trlnidatb  40813  cdlemc1  40827  cdlemc2  40828  cdlemc5  40831  cdlemc6  40832  cdlemd3  40836  cdlemd6  40839  cdleme0aa  40846  cdleme0b  40848  cdleme0c  40849  cdleme0e  40853  cdleme0fN  40854  cdleme01N  40857  cdleme02N  40858  cdleme0ex1N  40859  cdleme0moN  40861  cdleme3g  40870  cdleme3h  40871  cdleme3  40873  cdleme4  40874  cdleme4a  40875  cdleme5  40876  cdleme8  40886  cdleme9  40889  cdleme10  40890  cdleme16aN  40895  cdleme11a  40896  cdleme11fN  40900  cdleme11g  40901  cdleme11h  40902  cdleme11j  40903  cdleme11k  40904  cdleme12  40907  cdleme13  40908  cdleme17c  40924  cdleme17d1  40925  cdleme18a  40927  cdleme18b  40928  cdleme18c  40929  cdleme22gb  40930  cdlemeda  40934  cdlemednpq  40935  cdlemednuN  40936  cdleme19c  40941  cdleme20aN  40945  cdleme20bN  40946  cdleme20c  40947  cdleme22aa  40975  cdleme22a  40976  cdleme22b  40977  cdleme22d  40979  cdleme22e  40980  cdleme27cl  41002  cdleme27a  41003  cdleme30a  41014  cdleme42a  41107  cdleme42c  41108  cdleme50laut  41183  cdlemf1  41197  cdlemf  41199  cdlemfnid  41200  trlord  41205  cdlemg2fv2  41236  cdlemg2kq  41238  cdlemg2m  41240  cdlemg4a  41244  cdlemg4d  41249  cdlemg4g  41252  cdlemg4  41253  cdlemg6c  41256  cdlemg7aN  41261  cdlemg8a  41263  cdlemg8b  41264  cdlemg8c  41265  cdlemg9a  41268  cdlemg9b  41269  cdlemg9  41270  cdlemg11aq  41274  cdlemg10c  41275  cdlemg12a  41279  cdlemg12b  41280  cdlemg12c  41281  cdlemg17a  41297  cdlemg18b  41315  cdlemg18c  41316  cdlemg31b0a  41331  cdlemg31a  41333  cdlemg31b  41334  cdlemg31d  41336  cdlemg35  41349  trlcoabs2N  41358  trlcolem  41362  cdlemg44a  41367  trljco  41376  trljco2  41377  tendoco2  41404  tendopltp  41416  cdlemi1  41454  cdlemi2  41455  cdlemj3  41459  tendocan  41460  cdlemk3  41469  cdlemk4  41470  cdlemk5a  41471  cdlemk9  41475  cdlemk9bN  41476  cdlemkvcl  41478  cdlemk10  41479  cdlemk30  41530  cdlemk31  41532  cdlemk39  41552  cdlemkfid1N  41557  cdlemkid1  41558  cdlemkid2  41560  cdlemkfid3N  41561  cdlemk19ylem  41566  cdlemk19xlem  41578  cdlemk19x  41579  cdlemk53b  41592  cdlemk53  41593  cdlemk54  41594  cdlemk55a  41595  cdlemk43N  41599  cdlemk19u1  41605  cdlemk19u  41606  cdleml1N  41612  erngdvlem4  41627  erngdvlem4-rN  41635  dia11N  41684  cdlemm10N  41754  dib11N  41796  cdlemn2  41831  cdlemn10  41842  dihjustlem  41852  dihord2cN  41857  dihlsscpre  41870  dih1dimb2  41877  dihvalcq2  41883  dihopelvalcpre  41884  dihord6b  41896  dih11  41901  dihmeetlem1N  41926  dihglblem2N  41930  dihglblem3N  41931  dihmeetlem2N  41935  dihglbcpreN  41936  dihmeetcN  41938  dihmeetbclemN  41940  dihmeetlem4preN  41942  dihmeetlem9N  41951  dihmeetlem20N  41962  dihlspsnssN  41968  dihlspsnat  41969  dihatlat  41970  dihglblem6  41976  dihmeet  41979  dochss  42001  hdmapval3N  42474  hgmap11  42538  remulcand  43060  congtr  43554  fzmaxdif  43570  isnumbasgrplem2  43693  ntrclsk13  44659  ssmapsn  45790  infleinf  45945  suplesup2  45949  supxrunb3  45972  mullimc  46190  mullimcf  46197  islpcn  46211  limsupresxr  46338  liminfresxr  46339  cncfuni  46458  icccncfext  46459  stoweidlem34  46606  stoweidlem59  46631  stirlinglem13  46658  fourierdlem41  46720  fourierdlem42  46721  fourierdlem73  46751  sge0iunmptlemfi  46985  meadjiunlem  47037  ovncvrrp  47136  sssmf  47310  smflimsuplem7  47398  smflimsuplem8  47399  ormkglobd  47449  funressneu  47639  grlimedgclnbgr  48615  lincscm  49061  lincext3  49087  el0ldep  49097  el0ldepsnzr  49098  itscnhlc0xyqsol  49396  uptr2  49850