Theorem simp1l 1198

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  simp11l  1285  simp21l  1291  simp31l  1297  eqfunresadj  7357  tfisi  7848  offsplitfpar  8105  poseq  8144  omeulem2  8583  uniinqs  8791  unxpdomlem3  9252  elfiun  9425  cantnffval  9658  tcrank  9879  cofsmo  10264  isfin2-2  10314  tskint  10780  tskun  10781  tskurn  10784  gruina  10813  dedekind  11377  subaddmulsub  11677  dmdcan  11924  lt2msq1  12098  supmullem1  12184  supmul  12186  xaddass  13228  xaddass2  13229  xlt2add  13239  xmulasslem3  13265  xadddi2r  13277  iccsplit  13462  expaddzlem  14071  expaddz  14072  expmulz  14074  ccatopth2  14667  pfxccat3  14684  resqrtcl  15200  limsupgle  15421  o1add  15558  o1mul  15559  o1sub  15560  bitsfzo  16376  sadfval  16393  smufval  16418  prmexpb  16657  4sqlem18  16895  vdwlem10  16923  fsets  17102  setsstruct2  17107  submre  17549  mrelatlub  18515  gsmsymgreqlem2  19299  mndodcong  19410  subgabl  19704  gex2abl  19719  cntzsubr  20353  abvres  20447  lbsind2  20692  lspsneu  20736  lbsextlem2  20772  lbsextg  20775  lindfind2  21373  matring  21945  maducoeval  22141  maducoeval2  22142  maduf  22143  madurid  22146  gsummatr01  22161  cramerimplem3  22187  cnprest  22793  hausnei2  22857  isreg2  22881  cmpcld  22906  llyrest  22989  nllyrest  22990  csdfil  23398  hausflimlem  23483  ssblps  23928  ssbl  23929  cphassi  24731  cphassir  24732  4cphipval2  24759  cphipval  24760  dvres2  25429  plyadd  25731  plymul  25732  coeeu  25739  vieta1  25825  aalioulem3  25847  aalioulem4  25848  efgh  26050  cxpadd  26187  cxpsub  26190  mulcxp  26193  divcxp  26195  cxple2  26205  cxplt2  26206  cxpcn3lem  26255  angcan  26307  ang180lem5  26318  isosctrlem3  26325  logexprlim  26728  lgssq  26840  abvcxp  27118  padicabv  27133  nosupbnd2lem1  27218  noinfbnd2lem1  27233  nosupinfsep  27235  noetalem1  27244  sltmul2  27623  brbtwn2  28163  ax5seglem6  28192  axcontlem4  28225  axcontlem8  28229  uhgr2edg  28465  nbgrisvtx  28598  nbupgrres  28621  clwwlkccat  29243  clwwlknonex2lem2  29361  frgrreggt1  29646  chscllem4  30893  cshwrnid  32125  ogrpinvlt  32241  ifscgr  35016  matunitlindflem1  36484  lshpnelb  37854  lfl1  37940  lshpkrlem6  37985  lshpkrex  37988  hlrelat3  38283  atbtwnexOLDN  38318  atbtwnex  38319  3dim3  38340  3atlem5  38358  2llnmat  38395  lvolex3N  38409  lvolnle3at  38453  4atlem11  38480  4atlem12  38483  dalemccea  38554  cdlema2N  38663  paddasslem2  38692  atmod1i1m  38729  lhp2lt  38872  lhp0lt  38874  lhpj1  38893  lhpmcvr4N  38897  lhpelim  38908  lhpmod2i2  38909  lhpmod6i1  38910  cdlemb2  38912  lhple  38913  lhpat  38914  4atex  38947  4atex2-0aOLDN  38949  4atex3  38952  ldilco  38987  ltrncl  38996  ltrn11  38997  ltrnle  39000  ltrncnvleN  39001  ltrnm  39002  ltrnj  39003  ltrncvr  39004  ltrnatb  39008  ltrnel  39010  ltrncnvel  39013  ltrncnv  39017  trlval2  39034  trlcnv  39036  trljat1  39037  trljat2  39038  trl0  39041  ltrnnidn  39045  trlnidatb  39048  cdlemc1  39062  cdlemc2  39063  cdlemc5  39066  cdlemc6  39067  cdlemd3  39071  cdlemd6  39074  cdleme0aa  39081  cdleme0b  39083  cdleme0c  39084  cdleme0e  39088  cdleme0fN  39089  cdleme01N  39092  cdleme02N  39093  cdleme0ex1N  39094  cdleme0moN  39096  cdleme3g  39105  cdleme3h  39106  cdleme3  39108  cdleme4  39109  cdleme4a  39110  cdleme5  39111  cdleme8  39121  cdleme9  39124  cdleme10  39125  cdleme16aN  39130  cdleme11a  39131  cdleme11fN  39135  cdleme11g  39136  cdleme11h  39137  cdleme11j  39138  cdleme11k  39139  cdleme12  39142  cdleme13  39143  cdleme17c  39159  cdleme17d1  39160  cdleme18a  39162  cdleme18b  39163  cdleme18c  39164  cdleme22gb  39165  cdlemeda  39169  cdlemednpq  39170  cdlemednuN  39171  cdleme19c  39176  cdleme20aN  39180  cdleme20bN  39181  cdleme20c  39182  cdleme22aa  39210  cdleme22a  39211  cdleme22b  39212  cdleme22d  39214  cdleme22e  39215  cdleme27cl  39237  cdleme27a  39238  cdleme30a  39249  cdleme42a  39342  cdleme42c  39343  cdleme50laut  39418  cdlemf1  39432  cdlemf  39434  cdlemfnid  39435  trlord  39440  cdlemg2fv2  39471  cdlemg2kq  39473  cdlemg2m  39475  cdlemg4a  39479  cdlemg4d  39484  cdlemg4g  39487  cdlemg4  39488  cdlemg6c  39491  cdlemg7aN  39496  cdlemg8a  39498  cdlemg8b  39499  cdlemg8c  39500  cdlemg9a  39503  cdlemg9b  39504  cdlemg9  39505  cdlemg11aq  39509  cdlemg10c  39510  cdlemg12a  39514  cdlemg12b  39515  cdlemg12c  39516  cdlemg17a  39532  cdlemg18b  39550  cdlemg18c  39551  cdlemg31b0a  39566  cdlemg31a  39568  cdlemg31b  39569  cdlemg31d  39571  cdlemg35  39584  trlcoabs2N  39593  trlcolem  39597  cdlemg44a  39602  trljco  39611  trljco2  39612  tendoco2  39639  tendopltp  39651  cdlemi1  39689  cdlemi2  39690  cdlemj3  39694  tendocan  39695  cdlemk3  39704  cdlemk4  39705  cdlemk5a  39706  cdlemk9  39710  cdlemk9bN  39711  cdlemkvcl  39713  cdlemk10  39714  cdlemk30  39765  cdlemk31  39767  cdlemk39  39787  cdlemkfid1N  39792  cdlemkid1  39793  cdlemkid2  39795  cdlemkfid3N  39796  cdlemk19ylem  39801  cdlemk19xlem  39813  cdlemk19x  39814  cdlemk53b  39827  cdlemk53  39828  cdlemk54  39829  cdlemk55a  39830  cdlemk43N  39834  cdlemk19u1  39840  cdlemk19u  39841  cdleml1N  39847  erngdvlem4  39862  erngdvlem4-rN  39870  dia11N  39919  cdlemm10N  39989  dib11N  40031  cdlemn2  40066  cdlemn10  40077  dihjustlem  40087  dihord2cN  40092  dihlsscpre  40105  dih1dimb2  40112  dihvalcq2  40118  dihopelvalcpre  40119  dihord6b  40131  dih11  40136  dihmeetlem1N  40161  dihglblem2N  40165  dihglblem3N  40166  dihmeetlem2N  40170  dihglbcpreN  40171  dihmeetcN  40173  dihmeetbclemN  40175  dihmeetlem4preN  40177  dihmeetlem9N  40186  dihmeetlem20N  40197  dihlspsnssN  40203  dihlspsnat  40204  dihatlat  40205  dihglblem6  40211  dihmeet  40214  dochss  40236  hdmapval3N  40709  hgmap11  40773  nn0rppwr  41224  remulcand  41311  congtr  41704  fzmaxdif  41720  isnumbasgrplem2  41846  ntrclsk13  42822  ssmapsn  43915  infleinf  44082  suplesup2  44086  supxrunb3  44109  mullimc  44332  mullimcf  44339  islpcn  44355  limsupresxr  44482  liminfresxr  44483  cncfuni  44602  icccncfext  44603  stoweidlem34  44750  stoweidlem59  44775  stirlinglem13  44802  fourierdlem41  44864  fourierdlem42  44865  fourierdlem73  44895  sge0iunmptlemfi  45129  meadjiunlem  45181  ovncvrrp  45280  sssmf  45454  smflimsuplem7  45542  smflimsuplem8  45543  funressneu  45757  cntzsubrng  46746  lincscm  47111  lincext3  47137  el0ldep  47147  el0ldepsnzr  47148  itscnhlc0xyqsol  47451