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  7215  eqfunresadj  7315  tfisi  7810  offsplitfpar  8069  poseq  8108  omeulem2  8518  uniinqs  8744  unxpdomlem3  9168  elfiun  9343  cantnffval  9584  tcrank  9808  cofsmo  10191  isfin2-2  10241  tskint  10708  tskun  10709  tskurn  10712  gruina  10741  dedekind  11309  subaddmulsub  11613  dmdcan  11865  lt2msq1  12040  supmullem1  12126  supmul  12128  xaddass  13201  xaddass2  13202  xlt2add  13212  xmulasslem3  13238  xadddi2r  13250  iccsplit  13438  expaddzlem  14067  expaddz  14068  expmulz  14070  ccatopth2  14679  pfxccat3  14696  resqrtcl  15215  limsupgle  15439  o1add  15576  o1mul  15577  o1sub  15578  bitsfzo  16404  sadfval  16421  smufval  16446  nn0rppwr  16530  prmexpb  16689  4sqlem18  16933  vdwlem10  16961  fsets  17139  setsstruct2  17144  submre  17567  mrelatlub  18528  chnccat  18592  gsmsymgreqlem2  19406  mndodcong  19517  subgabl  19811  gex2abl  19826  ogrpinvlt  20119  cntzsubrng  20544  cntzsubr  20583  abvres  20808  lbsind2  21076  lspsneu  21121  lbsextlem2  21157  lbsextg  21160  lindfind2  21798  matring  22408  maducoeval  22604  maducoeval2  22605  maduf  22606  madurid  22609  gsummatr01  22624  cramerimplem3  22650  cnprest  23254  hausnei2  23318  isreg2  23342  cmpcld  23367  llyrest  23450  nllyrest  23451  csdfil  23859  hausflimlem  23944  ssblps  24387  ssbl  24388  cphassi  25181  cphassir  25182  4cphipval2  25209  cphipval  25210  dvres2  25879  plyadd  26182  plymul  26183  coeeu  26190  vieta1  26278  aalioulem3  26300  aalioulem4  26301  efgh  26505  cxpadd  26643  cxpsub  26646  mulcxp  26649  divcxp  26651  cxple2  26661  cxplt2  26662  cxpcn3lem  26711  angcan  26766  ang180lem5  26777  isosctrlem3  26784  logexprlim  27188  lgssq  27300  abvcxp  27578  padicabv  27593  nosupbnd2lem1  27679  noinfbnd2lem1  27694  nosupinfsep  27696  noetalem1  27705  ltmuls2  28163  brbtwn2  28974  ax5seglem6  29003  axcontlem4  29036  axcontlem8  29040  uhgr2edg  29277  nbgrisvtx  29410  nbupgrres  29433  clwwlkccat  30060  clwwlknonex2lem2  30178  frgrreggt1  30463  chscllem4  31711  cshwrnid  33021  ifscgr  36226  matunitlindflem1  37937  lshpnelb  39430  lfl1  39516  lshpkrlem6  39561  lshpkrex  39564  hlrelat3  39858  atbtwnexOLDN  39893  atbtwnex  39894  3dim3  39915  3atlem5  39933  2llnmat  39970  lvolex3N  39984  lvolnle3at  40028  4atlem11  40055  4atlem12  40058  dalemccea  40129  cdlema2N  40238  paddasslem2  40267  atmod1i1m  40304  lhp2lt  40447  lhp0lt  40449  lhpj1  40468  lhpmcvr4N  40472  lhpelim  40483  lhpmod2i2  40484  lhpmod6i1  40485  cdlemb2  40487  lhple  40488  lhpat  40489  4atex  40522  4atex2-0aOLDN  40524  4atex3  40527  ldilco  40562  ltrncl  40571  ltrn11  40572  ltrnle  40575  ltrncnvleN  40576  ltrnm  40577  ltrnj  40578  ltrncvr  40579  ltrnatb  40583  ltrnel  40585  ltrncnvel  40588  ltrncnv  40592  trlval2  40609  trlcnv  40611  trljat1  40612  trljat2  40613  trl0  40616  ltrnnidn  40620  trlnidatb  40623  cdlemc1  40637  cdlemc2  40638  cdlemc5  40641  cdlemc6  40642  cdlemd3  40646  cdlemd6  40649  cdleme0aa  40656  cdleme0b  40658  cdleme0c  40659  cdleme0e  40663  cdleme0fN  40664  cdleme01N  40667  cdleme02N  40668  cdleme0ex1N  40669  cdleme0moN  40671  cdleme3g  40680  cdleme3h  40681  cdleme3  40683  cdleme4  40684  cdleme4a  40685  cdleme5  40686  cdleme8  40696  cdleme9  40699  cdleme10  40700  cdleme16aN  40705  cdleme11a  40706  cdleme11fN  40710  cdleme11g  40711  cdleme11h  40712  cdleme11j  40713  cdleme11k  40714  cdleme12  40717  cdleme13  40718  cdleme17c  40734  cdleme17d1  40735  cdleme18a  40737  cdleme18b  40738  cdleme18c  40739  cdleme22gb  40740  cdlemeda  40744  cdlemednpq  40745  cdlemednuN  40746  cdleme19c  40751  cdleme20aN  40755  cdleme20bN  40756  cdleme20c  40757  cdleme22aa  40785  cdleme22a  40786  cdleme22b  40787  cdleme22d  40789  cdleme22e  40790  cdleme27cl  40812  cdleme27a  40813  cdleme30a  40824  cdleme42a  40917  cdleme42c  40918  cdleme50laut  40993  cdlemf1  41007  cdlemf  41009  cdlemfnid  41010  trlord  41015  cdlemg2fv2  41046  cdlemg2kq  41048  cdlemg2m  41050  cdlemg4a  41054  cdlemg4d  41059  cdlemg4g  41062  cdlemg4  41063  cdlemg6c  41066  cdlemg7aN  41071  cdlemg8a  41073  cdlemg8b  41074  cdlemg8c  41075  cdlemg9a  41078  cdlemg9b  41079  cdlemg9  41080  cdlemg11aq  41084  cdlemg10c  41085  cdlemg12a  41089  cdlemg12b  41090  cdlemg12c  41091  cdlemg17a  41107  cdlemg18b  41125  cdlemg18c  41126  cdlemg31b0a  41141  cdlemg31a  41143  cdlemg31b  41144  cdlemg31d  41146  cdlemg35  41159  trlcoabs2N  41168  trlcolem  41172  cdlemg44a  41177  trljco  41186  trljco2  41187  tendoco2  41214  tendopltp  41226  cdlemi1  41264  cdlemi2  41265  cdlemj3  41269  tendocan  41270  cdlemk3  41279  cdlemk4  41280  cdlemk5a  41281  cdlemk9  41285  cdlemk9bN  41286  cdlemkvcl  41288  cdlemk10  41289  cdlemk30  41340  cdlemk31  41342  cdlemk39  41362  cdlemkfid1N  41367  cdlemkid1  41368  cdlemkid2  41370  cdlemkfid3N  41371  cdlemk19ylem  41376  cdlemk19xlem  41388  cdlemk19x  41389  cdlemk53b  41402  cdlemk53  41403  cdlemk54  41404  cdlemk55a  41405  cdlemk43N  41409  cdlemk19u1  41415  cdlemk19u  41416  cdleml1N  41422  erngdvlem4  41437  erngdvlem4-rN  41445  dia11N  41494  cdlemm10N  41564  dib11N  41606  cdlemn2  41641  cdlemn10  41652  dihjustlem  41662  dihord2cN  41667  dihlsscpre  41680  dih1dimb2  41687  dihvalcq2  41693  dihopelvalcpre  41694  dihord6b  41706  dih11  41711  dihmeetlem1N  41736  dihglblem2N  41740  dihglblem3N  41741  dihmeetlem2N  41745  dihglbcpreN  41746  dihmeetcN  41748  dihmeetbclemN  41750  dihmeetlem4preN  41752  dihmeetlem9N  41761  dihmeetlem20N  41772  dihlspsnssN  41778  dihlspsnat  41779  dihatlat  41780  dihglblem6  41786  dihmeet  41789  dochss  41811  hdmapval3N  42284  hgmap11  42348  remulcand  42871  congtr  43393  fzmaxdif  43409  isnumbasgrplem2  43532  ntrclsk13  44498  ssmapsn  45645  infleinf  45801  suplesup2  45805  supxrunb3  45828  mullimc  46046  mullimcf  46053  islpcn  46067  limsupresxr  46194  liminfresxr  46195  cncfuni  46314  icccncfext  46315  stoweidlem34  46462  stoweidlem59  46487  stirlinglem13  46514  fourierdlem41  46576  fourierdlem42  46577  fourierdlem73  46607  sge0iunmptlemfi  46841  meadjiunlem  46893  ovncvrrp  46992  sssmf  47166  smflimsuplem7  47254  smflimsuplem8  47255  ormkglobd  47305  funressneu  47495  grlimedgclnbgr  48471  lincscm  48906  lincext3  48932  el0ldep  48942  el0ldepsnzr  48943  itscnhlc0xyqsol  49241  uptr2  49696