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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp11l  1285  simp21l  1291  simp31l  1297  2f1fvneq  7235  eqfunresadj  7335  tfisi  7835  offsplitfpar  8098  poseq  8137  omeulem2  8547  uniinqs  8770  unxpdomlem3  9199  elfiun  9381  cantnffval  9616  tcrank  9837  cofsmo  10222  isfin2-2  10272  tskint  10738  tskun  10739  tskurn  10742  gruina  10771  dedekind  11337  subaddmulsub  11641  dmdcan  11892  lt2msq1  12067  supmullem1  12153  supmul  12155  xaddass  13209  xaddass2  13210  xlt2add  13220  xmulasslem3  13246  xadddi2r  13258  iccsplit  13446  expaddzlem  14070  expaddz  14071  expmulz  14073  ccatopth2  14682  pfxccat3  14699  resqrtcl  15219  limsupgle  15443  o1add  15580  o1mul  15581  o1sub  15582  bitsfzo  16405  sadfval  16422  smufval  16447  nn0rppwr  16531  prmexpb  16689  4sqlem18  16933  vdwlem10  16961  fsets  17139  setsstruct2  17144  submre  17566  mrelatlub  18521  gsmsymgreqlem2  19361  mndodcong  19472  subgabl  19766  gex2abl  19781  cntzsubrng  20476  cntzsubr  20515  abvres  20740  lbsind2  20988  lspsneu  21033  lbsextlem2  21069  lbsextg  21072  lindfind2  21727  matring  22330  maducoeval  22526  maducoeval2  22527  maduf  22528  madurid  22531  gsummatr01  22546  cramerimplem3  22572  cnprest  23176  hausnei2  23240  isreg2  23264  cmpcld  23289  llyrest  23372  nllyrest  23373  csdfil  23781  hausflimlem  23866  ssblps  24310  ssbl  24311  cphassi  25114  cphassir  25115  4cphipval2  25142  cphipval  25143  dvres2  25813  plyadd  26122  plymul  26123  coeeu  26130  vieta1  26220  aalioulem3  26242  aalioulem4  26243  efgh  26450  cxpadd  26588  cxpsub  26591  mulcxp  26594  divcxp  26596  cxple2  26606  cxplt2  26607  cxpcn3lem  26657  angcan  26712  ang180lem5  26723  isosctrlem3  26730  logexprlim  27136  lgssq  27248  abvcxp  27526  padicabv  27541  nosupbnd2lem1  27627  noinfbnd2lem1  27642  nosupinfsep  27644  noetalem1  27653  sltmul2  28074  brbtwn2  28832  ax5seglem6  28861  axcontlem4  28894  axcontlem8  28898  uhgr2edg  29135  nbgrisvtx  29268  nbupgrres  29291  clwwlkccat  29919  clwwlknonex2lem2  30037  frgrreggt1  30322  chscllem4  31569  cshwrnid  32883  ogrpinvlt  33037  ifscgr  36032  matunitlindflem1  37610  lshpnelb  38977  lfl1  39063  lshpkrlem6  39108  lshpkrex  39111  hlrelat3  39406  atbtwnexOLDN  39441  atbtwnex  39442  3dim3  39463  3atlem5  39481  2llnmat  39518  lvolex3N  39532  lvolnle3at  39576  4atlem11  39603  4atlem12  39606  dalemccea  39677  cdlema2N  39786  paddasslem2  39815  atmod1i1m  39852  lhp2lt  39995  lhp0lt  39997  lhpj1  40016  lhpmcvr4N  40020  lhpelim  40031  lhpmod2i2  40032  lhpmod6i1  40033  cdlemb2  40035  lhple  40036  lhpat  40037  4atex  40070  4atex2-0aOLDN  40072  4atex3  40075  ldilco  40110  ltrncl  40119  ltrn11  40120  ltrnle  40123  ltrncnvleN  40124  ltrnm  40125  ltrnj  40126  ltrncvr  40127  ltrnatb  40131  ltrnel  40133  ltrncnvel  40136  ltrncnv  40140  trlval2  40157  trlcnv  40159  trljat1  40160  trljat2  40161  trl0  40164  ltrnnidn  40168  trlnidatb  40171  cdlemc1  40185  cdlemc2  40186  cdlemc5  40189  cdlemc6  40190  cdlemd3  40194  cdlemd6  40197  cdleme0aa  40204  cdleme0b  40206  cdleme0c  40207  cdleme0e  40211  cdleme0fN  40212  cdleme01N  40215  cdleme02N  40216  cdleme0ex1N  40217  cdleme0moN  40219  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme4  40232  cdleme4a  40233  cdleme5  40234  cdleme8  40244  cdleme9  40247  cdleme10  40248  cdleme16aN  40253  cdleme11a  40254  cdleme11fN  40258  cdleme11g  40259  cdleme11h  40260  cdleme11j  40261  cdleme11k  40262  cdleme12  40265  cdleme13  40266  cdleme17c  40282  cdleme17d1  40283  cdleme18a  40285  cdleme18b  40286  cdleme18c  40287  cdleme22gb  40288  cdlemeda  40292  cdlemednpq  40293  cdlemednuN  40294  cdleme19c  40299  cdleme20aN  40303  cdleme20bN  40304  cdleme20c  40305  cdleme22aa  40333  cdleme22a  40334  cdleme22b  40335  cdleme22d  40337  cdleme22e  40338  cdleme27cl  40360  cdleme27a  40361  cdleme30a  40372  cdleme42a  40465  cdleme42c  40466  cdleme50laut  40541  cdlemf1  40555  cdlemf  40557  cdlemfnid  40558  trlord  40563  cdlemg2fv2  40594  cdlemg2kq  40596  cdlemg2m  40598  cdlemg4a  40602  cdlemg4d  40607  cdlemg4g  40610  cdlemg4  40611  cdlemg6c  40614  cdlemg7aN  40619  cdlemg8a  40621  cdlemg8b  40622  cdlemg8c  40623  cdlemg9a  40626  cdlemg9b  40627  cdlemg9  40628  cdlemg11aq  40632  cdlemg10c  40633  cdlemg12a  40637  cdlemg12b  40638  cdlemg12c  40639  cdlemg17a  40655  cdlemg18b  40673  cdlemg18c  40674  cdlemg31b0a  40689  cdlemg31a  40691  cdlemg31b  40692  cdlemg31d  40694  cdlemg35  40707  trlcoabs2N  40716  trlcolem  40720  cdlemg44a  40725  trljco  40734  trljco2  40735  tendoco2  40762  tendopltp  40774  cdlemi1  40812  cdlemi2  40813  cdlemj3  40817  tendocan  40818  cdlemk3  40827  cdlemk4  40828  cdlemk5a  40829  cdlemk9  40833  cdlemk9bN  40834  cdlemkvcl  40836  cdlemk10  40837  cdlemk30  40888  cdlemk31  40890  cdlemk39  40910  cdlemkfid1N  40915  cdlemkid1  40916  cdlemkid2  40918  cdlemkfid3N  40919  cdlemk19ylem  40924  cdlemk19xlem  40936  cdlemk19x  40937  cdlemk53b  40950  cdlemk53  40951  cdlemk54  40952  cdlemk55a  40953  cdlemk43N  40957  cdlemk19u1  40963  cdlemk19u  40964  cdleml1N  40970  erngdvlem4  40985  erngdvlem4-rN  40993  dia11N  41042  cdlemm10N  41112  dib11N  41154  cdlemn2  41189  cdlemn10  41200  dihjustlem  41210  dihord2cN  41215  dihlsscpre  41228  dih1dimb2  41235  dihvalcq2  41241  dihopelvalcpre  41242  dihord6b  41254  dih11  41259  dihmeetlem1N  41284  dihglblem2N  41288  dihglblem3N  41289  dihmeetlem2N  41293  dihglbcpreN  41294  dihmeetcN  41296  dihmeetbclemN  41298  dihmeetlem4preN  41300  dihmeetlem9N  41309  dihmeetlem20N  41320  dihlspsnssN  41326  dihlspsnat  41327  dihatlat  41328  dihglblem6  41334  dihmeet  41337  dochss  41359  hdmapval3N  41832  hgmap11  41896  remulcand  42427  congtr  42954  fzmaxdif  42970  isnumbasgrplem2  43093  ntrclsk13  44060  ssmapsn  45210  infleinf  45368  suplesup2  45372  supxrunb3  45395  mullimc  45614  mullimcf  45621  islpcn  45637  limsupresxr  45764  liminfresxr  45765  cncfuni  45884  icccncfext  45885  stoweidlem34  46032  stoweidlem59  46057  stirlinglem13  46084  fourierdlem41  46146  fourierdlem42  46147  fourierdlem73  46177  sge0iunmptlemfi  46411  meadjiunlem  46463  ovncvrrp  46562  sssmf  46736  smflimsuplem7  46824  smflimsuplem8  46825  ormkglobd  46873  funressneu  47048  lincscm  48419  lincext3  48445  el0ldep  48455  el0ldepsnzr  48456  itscnhlc0xyqsol  48754  uptr2  49210