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

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

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 1105

This theorem is referenced by:  simp11l  1303  simp21l  1309  simp31l  1315  2f1fvneq  7260  eqfunresadj  7360  tfisi  7856  offsplitfpar  8115  poseq  8155  omeulem2  8569  uniinqs  8796  unxpdomlem3  9219  elfiun  9391  cantnffval  9633  tcrank  9857  cofsmo  10254  isfin2-2  10304  tskint  10771  tskun  10772  tskurn  10775  gruina  10804  dedekind  11374  subaddmulsub  11678  dmdcan  11926  lt2msq1  12100  supmullem1  12186  supmul  12188  xaddass  13276  xaddass2  13277  xlt2add  13287  xmulasslem3  13313  xadddi2r  13325  iccsplit  13513  expaddzlem  14143  expaddz  14144  expmulz  14146  ccatopth2  14756  pfxccat3  14773  resqrtcl  15306  limsupgle  15530  o1add  15667  o1mul  15668  o1sub  15669  bitsfzo  16494  sadfval  16511  smufval  16536  nn0rppwr  16620  prmexpb  16779  4sqlem18  17023  vdwlem10  17051  fsets  17230  setsstruct2  17235  submre  17658  mrelatlub  18619  chnccat  18683  gsmsymgreqlem2  19502  mndodcong  19613  subgabl  19907  gex2abl  19922  ogrpinvlt  20215  rng1zrlem  20260  cntzsubrng  20653  cntzsubr  20692  abvres  20915  lbsind2  21183  lspsneu  21228  lbsextlem2  21264  lbsextg  21267  lindfind2  21949  matring  22581  maducoeval  22777  maducoeval2  22778  maduf  22779  madurid  22782  gsummatr01  22797  cramerimplem3  22823  cnprest  23427  hausnei2  23491  isreg2  23515  cmpcld  23540  llyrest  23623  nllyrest  23624  csdfil  24032  hausflimlem  24117  ssblps  24560  ssbl  24561  cphassi  25354  cphassir  25355  4cphipval2  25382  cphipval  25383  dvres2  26052  plyadd  26355  plymul  26356  coeeu  26363  vieta1  26454  aalioulem3  26476  aalioulem4  26477  efgh  26684  cxpadd  26822  cxpsub  26825  mulcxp  26828  divcxp  26830  cxple2  26840  cxplt2  26841  cxpcn3lem  26890  angcan  26945  ang180lem5  26956  isosctrlem3  26963  logexprlim  27367  lgssq  27479  abvcxp  27757  padicabv  27772  nosupbnd2lem1  27857  noinfbnd2lem1  27872  nosupinfsep  27874  noetalem1  27883  ltmuls2  28342  brbtwn2  29233  ax5seglem6  29262  axcontlem4  29295  axcontlem8  29299  uhgr2edg  29536  nbgrisvtx  29669  nbupgrres  29692  clwwlkccat  30319  clwwlknonex2lem2  30437  frgrreggt1  30722  chscllem4  31970  cshwrnid  33259  ifscgr  36514  matunitlindflem1  38245  lshpnelb  39736  lfl1  39822  lshpkrlem6  39867  lshpkrex  39870  hlrelat3  40164  atbtwnexOLDN  40199  atbtwnex  40200  3dim3  40221  3atlem5  40239  2llnmat  40276  lvolex3N  40290  lvolnle3at  40334  4atlem11  40361  4atlem12  40364  dalemccea  40435  cdlema2N  40544  paddasslem2  40573  atmod1i1m  40610  lhp2lt  40753  lhp0lt  40755  lhpj1  40774  lhpmcvr4N  40778  lhpelim  40789  lhpmod2i2  40790  lhpmod6i1  40791  cdlemb2  40793  lhple  40794  lhpat  40795  4atex  40828  4atex2-0aOLDN  40830  4atex3  40833  ldilco  40868  ltrncl  40877  ltrn11  40878  ltrnle  40881  ltrncnvleN  40882  ltrnm  40883  ltrnj  40884  ltrncvr  40885  ltrnatb  40889  ltrnel  40891  ltrncnvel  40894  ltrncnv  40898  trlval2  40915  trlcnv  40917  trljat1  40918  trljat2  40919  trl0  40922  ltrnnidn  40926  trlnidatb  40929  cdlemc1  40943  cdlemc2  40944  cdlemc5  40947  cdlemc6  40948  cdlemd3  40952  cdlemd6  40955  cdleme0aa  40962  cdleme0b  40964  cdleme0c  40965  cdleme0e  40969  cdleme0fN  40970  cdleme01N  40973  cdleme02N  40974  cdleme0ex1N  40975  cdleme0moN  40977  cdleme3g  40986  cdleme3h  40987  cdleme3  40989  cdleme4  40990  cdleme4a  40991  cdleme5  40992  cdleme8  41002  cdleme9  41005  cdleme10  41006  cdleme16aN  41011  cdleme11a  41012  cdleme11fN  41016  cdleme11g  41017  cdleme11h  41018  cdleme11j  41019  cdleme11k  41020  cdleme12  41023  cdleme13  41024  cdleme17c  41040  cdleme17d1  41041  cdleme18a  41043  cdleme18b  41044  cdleme18c  41045  cdleme22gb  41046  cdlemeda  41050  cdlemednpq  41051  cdlemednuN  41052  cdleme19c  41057  cdleme20aN  41061  cdleme20bN  41062  cdleme20c  41063  cdleme22aa  41091  cdleme22a  41092  cdleme22b  41093  cdleme22d  41095  cdleme22e  41096  cdleme27cl  41118  cdleme27a  41119  cdleme30a  41130  cdleme42a  41223  cdleme42c  41224  cdleme50laut  41299  cdlemf1  41313  cdlemf  41315  cdlemfnid  41316  trlord  41321  cdlemg2fv2  41352  cdlemg2kq  41354  cdlemg2m  41356  cdlemg4a  41360  cdlemg4d  41365  cdlemg4g  41368  cdlemg4  41369  cdlemg6c  41372  cdlemg7aN  41377  cdlemg8a  41379  cdlemg8b  41380  cdlemg8c  41381  cdlemg9a  41384  cdlemg9b  41385  cdlemg9  41386  cdlemg11aq  41390  cdlemg10c  41391  cdlemg12a  41395  cdlemg12b  41396  cdlemg12c  41397  cdlemg17a  41413  cdlemg18b  41431  cdlemg18c  41432  cdlemg31b0a  41447  cdlemg31a  41449  cdlemg31b  41450  cdlemg31d  41452  cdlemg35  41465  trlcoabs2N  41474  trlcolem  41478  cdlemg44a  41483  trljco  41492  trljco2  41493  tendoco2  41520  tendopltp  41532  cdlemi1  41570  cdlemi2  41571  cdlemj3  41575  tendocan  41576  cdlemk3  41585  cdlemk4  41586  cdlemk5a  41587  cdlemk9  41591  cdlemk9bN  41592  cdlemkvcl  41594  cdlemk10  41595  cdlemk30  41646  cdlemk31  41648  cdlemk39  41668  cdlemkfid1N  41673  cdlemkid1  41674  cdlemkid2  41676  cdlemkfid3N  41677  cdlemk19ylem  41682  cdlemk19xlem  41694  cdlemk19x  41695  cdlemk53b  41708  cdlemk53  41709  cdlemk54  41710  cdlemk55a  41711  cdlemk43N  41715  cdlemk19u1  41721  cdlemk19u  41722  cdleml1N  41728  erngdvlem4  41743  erngdvlem4-rN  41751  dia11N  41800  cdlemm10N  41870  dib11N  41912  cdlemn2  41947  cdlemn10  41958  dihjustlem  41968  dihord2cN  41973  dihlsscpre  41986  dih1dimb2  41993  dihvalcq2  41999  dihopelvalcpre  42000  dihord6b  42012  dih11  42017  dihmeetlem1N  42042  dihglblem2N  42046  dihglblem3N  42047  dihmeetlem2N  42051  dihglbcpreN  42052  dihmeetcN  42054  dihmeetbclemN  42056  dihmeetlem4preN  42058  dihmeetlem9N  42067  dihmeetlem20N  42078  dihlspsnssN  42084  dihlspsnat  42085  dihatlat  42086  dihglblem6  42092  dihmeet  42095  dochss  42117  hdmapval3N  42590  hgmap11  42654  remulcand  43178  congtr  43672  fzmaxdif  43688  isnumbasgrplem2  43811  ntrclsk13  44777  ssmapsn  45912  infleinf  46067  suplesup2  46071  supxrunb3  46094  mullimc  46312  mullimcf  46319  islpcn  46333  limsupresxr  46460  liminfresxr  46461  cncfuni  46580  icccncfext  46581  stoweidlem34  46728  stoweidlem59  46753  stirlinglem13  46780  fourierdlem41  46842  fourierdlem42  46843  fourierdlem73  46873  sge0iunmptlemfi  47107  meadjiunlem  47159  ovncvrrp  47258  sssmf  47432  smflimsuplem7  47520  smflimsuplem8  47521  ormkglobd  47571  funressneu  47761  grlimedgclnbgr  48737  lincscm  49187  lincext3  49213  el0ldep  49223  el0ldepsnzr  49224  itscnhlc0xyqsol  49522  uptr2  49976