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  8130  poseq  8175  omeulem2  8591  uniinqs  8818  unxpdomlem3  9249  elfiun  9422  cantnffval  9664  tcrank  9901  cofsmo  10347  isfin2-2  10397  tskint  10870  tskun  10871  tskurn  10874  gruina  10903  dedekind  11473  subaddmulsub  11779  dmdcan  12027  lt2msq1  12201  supmullem1  12287  supmul  12289  xaddass  13379  xaddass2  13380  xlt2add  13390  xmulasslem3  13416  xadddi2r  13428  iccsplit  13616  expaddzlem  14248  expaddz  14249  expmulz  14251  ccatopth2  14866  pfxccat3  14883  resqrtcl  15420  limsupgle  15644  o1add  15781  o1mul  15782  o1sub  15783  bitsfzo  16605  sadfval  16622  smufval  16647  nn0rppwr  16735  prmexpb  16895  4sqlem18  17140  vdwlem10  17168  fsets  17347  setsstruct2  17352  submre  17775  mrelatlub  18736  chnccat  18800  gsmsymgreqlem2  19645  mndodcong  19756  subgabl  20050  gex2abl  20065  ogrpinvlt  20358  rng1zrlem  20403  cntzsubrng  20819  cntzsubr  20858  abvres  21088  lbsind2  21356  lspsneu  21401  lbsextlem2  21437  lbsextg  21440  lindfind2  22124  matring  22758  maducoeval  22954  maducoeval2  22955  maduf  22956  madurid  22959  gsummatr01  22974  matunitlindflem1  22994  cramerimplem3  23003  cnprest  23607  hausnei2  23671  isreg2  23695  cmpcld  23720  llyrest  23804  nllyrest  23805  csdfil  24213  hausflimlem  24298  ssblps  24741  ssbl  24742  cphassi  25535  cphassir  25536  4cphipval2  25563  cphipval  25564  dvres2  26232  plyadd  26536  plymul  26537  coeeu  26544  vieta1  26635  aalioulem3  26661  aalioulem4  26662  efgh  26869  cxpadd  27007  cxpsub  27010  mulcxp  27013  divcxp  27015  cxple2  27025  cxplt2  27026  cxpcn3lem  27075  angcan  27130  ang180lem5  27141  isosctrlem3  27148  logexprlim  27552  lgssq  27664  abvcxp  27942  padicabv  27957  nosupbnd2lem1  28072  noinfbnd2lem1  28087  nosupinfsep  28089  noetalem1  28098  ltmuls2  28557  brbtwn2  29483  ax5seglem6  29512  axcontlem4  29545  axcontlem8  29549  uhgr2edg  29789  nbgrisvtx  29922  nbupgrres  29945  clwwlkccat  30581  clwwlknonex2lem2  30699  frgrreggt1  30994  chscllem4  32242  cshwrnid  33564  ifscgr  36851  lshpnelb  40084  lfl1  40170  lshpkrlem6  40215  lshpkrex  40218  hlrelat3  40512  atbtwnexOLDN  40547  atbtwnex  40548  3dim3  40569  3atlem5  40587  2llnmat  40624  lvolex3N  40638  lvolnle3at  40682  4atlem11  40709  4atlem12  40712  dalemccea  40783  cdlema2N  40892  paddasslem2  40921  atmod1i1m  40958  lhp2lt  41101  lhp0lt  41103  lhpj1  41122  lhpmcvr4N  41126  lhpelim  41137  lhpmod2i2  41138  lhpmod6i1  41139  cdlemb2  41141  lhple  41142  lhpat  41143  4atex  41176  4atex2-0aOLDN  41178  4atex3  41181  ldilco  41216  ltrncl  41225  ltrn11  41226  ltrnle  41229  ltrncnvleN  41230  ltrnm  41231  ltrnj  41232  ltrncvr  41233  ltrnatb  41237  ltrnel  41239  ltrncnvel  41242  ltrncnv  41246  trlval2  41263  trlcnv  41265  trljat1  41266  trljat2  41267  trl0  41270  ltrnnidn  41274  trlnidatb  41277  cdlemc1  41291  cdlemc2  41292  cdlemc5  41295  cdlemc6  41296  cdlemd3  41300  cdlemd6  41303  cdleme0aa  41310  cdleme0b  41312  cdleme0c  41313  cdleme0e  41317  cdleme0fN  41318  cdleme01N  41321  cdleme02N  41322  cdleme0ex1N  41323  cdleme0moN  41325  cdleme3g  41334  cdleme3h  41335  cdleme3  41337  cdleme4  41338  cdleme4a  41339  cdleme5  41340  cdleme8  41350  cdleme9  41353  cdleme10  41354  cdleme16aN  41359  cdleme11a  41360  cdleme11fN  41364  cdleme11g  41365  cdleme11h  41366  cdleme11j  41367  cdleme11k  41368  cdleme12  41371  cdleme13  41372  cdleme17c  41388  cdleme17d1  41389  cdleme18a  41391  cdleme18b  41392  cdleme18c  41393  cdleme22gb  41394  cdlemeda  41398  cdlemednpq  41399  cdlemednuN  41400  cdleme19c  41405  cdleme20aN  41409  cdleme20bN  41410  cdleme20c  41411  cdleme22aa  41439  cdleme22a  41440  cdleme22b  41441  cdleme22d  41443  cdleme22e  41444  cdleme27cl  41466  cdleme27a  41467  cdleme30a  41478  cdleme42a  41571  cdleme42c  41572  cdleme50laut  41647  cdlemf1  41661  cdlemf  41663  cdlemfnid  41664  trlord  41669  cdlemg2fv2  41700  cdlemg2kq  41702  cdlemg2m  41704  cdlemg4a  41708  cdlemg4d  41713  cdlemg4g  41716  cdlemg4  41717  cdlemg6c  41720  cdlemg7aN  41725  cdlemg8a  41727  cdlemg8b  41728  cdlemg8c  41729  cdlemg9a  41732  cdlemg9b  41733  cdlemg9  41734  cdlemg11aq  41738  cdlemg10c  41739  cdlemg12a  41743  cdlemg12b  41744  cdlemg12c  41745  cdlemg17a  41761  cdlemg18b  41779  cdlemg18c  41780  cdlemg31b0a  41795  cdlemg31a  41797  cdlemg31b  41798  cdlemg31d  41800  cdlemg35  41813  trlcoabs2N  41822  trlcolem  41826  cdlemg44a  41831  trljco  41840  trljco2  41841  tendoco2  41868  tendopltp  41880  cdlemi1  41918  cdlemi2  41919  cdlemj3  41923  tendocan  41924  cdlemk3  41933  cdlemk4  41934  cdlemk5a  41935  cdlemk9  41939  cdlemk9bN  41940  cdlemkvcl  41942  cdlemk10  41943  cdlemk30  41994  cdlemk31  41996  cdlemk39  42016  cdlemkfid1N  42021  cdlemkid1  42022  cdlemkid2  42024  cdlemkfid3N  42025  cdlemk19ylem  42030  cdlemk19xlem  42042  cdlemk19x  42043  cdlemk53b  42056  cdlemk53  42057  cdlemk54  42058  cdlemk55a  42059  cdlemk43N  42063  cdlemk19u1  42069  cdlemk19u  42070  cdleml1N  42076  erngdvlem4  42091  erngdvlem4-rN  42099  dia11N  42148  cdlemm10N  42218  dib11N  42260  cdlemn2  42295  cdlemn10  42306  dihjustlem  42316  dihord2cN  42321  dihlsscpre  42334  dih1dimb2  42341  dihvalcq2  42347  dihopelvalcpre  42348  dihord6b  42360  dih11  42365  dihmeetlem1N  42390  dihglblem2N  42394  dihglblem3N  42395  dihmeetlem2N  42399  dihglbcpreN  42400  dihmeetcN  42402  dihmeetbclemN  42404  dihmeetlem4preN  42406  dihmeetlem9N  42415  dihmeetlem20N  42426  dihlspsnssN  42432  dihlspsnat  42433  dihatlat  42434  dihglblem6  42440  dihmeet  42443  dochss  42465  hdmapval3N  42938  hgmap11  43002  remulcand  43533  congtr  44014  fzmaxdif  44030  isnumbasgrplem2  44148  ntrclsk13  45113  ssmapsn  46271  infleinf  46425  suplesup2  46429  supxrunb3  46452  mullimc  46670  mullimcf  46677  islpcn  46691  limsupresxr  46818  liminfresxr  46819  cncfuni  46938  icccncfext  46939  stoweidlem34  47086  stoweidlem59  47111  stirlinglem13  47138  fourierdlem41  47200  fourierdlem42  47201  fourierdlem73  47231  sge0iunmptlemfi  47465  meadjiunlem  47517  ovncvrrp  47616  sssmf  47790  smflimsuplem7  47878  smflimsuplem8  47879  ormkglobd  47929  funressneu  48159  grlimedgclnbgr  49135  lincscm  49584  lincext3  49610  el0ldep  49620  el0ldepsnzr  49621  itscnhlc0xyqsol  49919  uptr2  50371