Theorem simp1l 1196

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp11l  1283  simp21l  1289  simp31l  1295  tfisi  7714  offsplitfpar  7969  omeulem2  8423  uniinqs  8595  unxpdomlem3  9038  elfiun  9198  cantnffval  9430  tcrank  9651  cofsmo  10034  isfin2-2  10084  tskint  10550  tskun  10551  tskurn  10554  gruina  10583  dedekind  11147  subaddmulsub  11447  dmdcan  11694  lt2msq1  11868  supmullem1  11954  supmul  11956  xaddass  12992  xaddass2  12993  xlt2add  13003  xmulasslem3  13029  xadddi2r  13041  iccsplit  13226  expaddzlem  13835  expaddz  13836  expmulz  13838  ccatopth2  14439  pfxccat3  14456  resqrtcl  14974  limsupgle  15195  o1add  15332  o1mul  15333  o1sub  15334  bitsfzo  16151  sadfval  16168  smufval  16193  prmexpb  16434  4sqlem18  16672  vdwlem10  16700  fsets  16879  setsstruct2  16884  submre  17323  mrelatlub  18289  gsmsymgreqlem2  19048  mndodcong  19159  subgabl  19446  gex2abl  19461  cntzsubr  20066  abvres  20108  lbsind2  20352  lspsneu  20394  lbsextlem2  20430  lbsextg  20433  lindfind2  21034  matring  21601  maducoeval  21797  maducoeval2  21798  maduf  21799  madurid  21802  gsummatr01  21817  cramerimplem3  21843  cnprest  22449  hausnei2  22513  isreg2  22537  cmpcld  22562  llyrest  22645  nllyrest  22646  csdfil  23054  hausflimlem  23139  ssblps  23584  ssbl  23585  cphassi  24387  cphassir  24388  4cphipval2  24415  cphipval  24416  dvres2  25085  plyadd  25387  plymul  25388  coeeu  25395  vieta1  25481  aalioulem3  25503  aalioulem4  25504  efgh  25706  cxpadd  25843  cxpsub  25846  mulcxp  25849  divcxp  25851  cxple2  25861  cxplt2  25862  cxpcn3lem  25909  angcan  25961  ang180lem5  25972  isosctrlem3  25979  logexprlim  26382  lgssq  26494  abvcxp  26772  padicabv  26787  brbtwn2  27282  ax5seglem6  27311  axcontlem4  27344  axcontlem8  27348  uhgr2edg  27584  nbgrisvtx  27717  nbupgrres  27740  clwwlkccat  28363  clwwlknonex2lem2  28481  frgrreggt1  28766  chscllem4  30011  cshwrnid  31242  ogrpinvlt  31358  eqfunresadj  33744  poseq  33811  nosupbnd2lem1  33927  noinfbnd2lem1  33942  nosupinfsep  33944  noetalem1  33953  ifscgr  34355  matunitlindflem1  35782  lshpnelb  37005  lfl1  37091  lshpkrlem6  37136  lshpkrex  37139  hlrelat3  37433  atbtwnexOLDN  37468  atbtwnex  37469  3dim3  37490  3atlem5  37508  2llnmat  37545  lvolex3N  37559  lvolnle3at  37603  4atlem11  37630  4atlem12  37633  dalemccea  37704  cdlema2N  37813  paddasslem2  37842  atmod1i1m  37879  lhp2lt  38022  lhp0lt  38024  lhpj1  38043  lhpmcvr4N  38047  lhpelim  38058  lhpmod2i2  38059  lhpmod6i1  38060  cdlemb2  38062  lhple  38063  lhpat  38064  4atex  38097  4atex2-0aOLDN  38099  4atex3  38102  ldilco  38137  ltrncl  38146  ltrn11  38147  ltrnle  38150  ltrncnvleN  38151  ltrnm  38152  ltrnj  38153  ltrncvr  38154  ltrnatb  38158  ltrnel  38160  ltrncnvel  38163  ltrncnv  38167  trlval2  38184  trlcnv  38186  trljat1  38187  trljat2  38188  trl0  38191  ltrnnidn  38195  trlnidatb  38198  cdlemc1  38212  cdlemc2  38213  cdlemc5  38216  cdlemc6  38217  cdlemd3  38221  cdlemd6  38224  cdleme0aa  38231  cdleme0b  38233  cdleme0c  38234  cdleme0e  38238  cdleme0fN  38239  cdleme01N  38242  cdleme02N  38243  cdleme0ex1N  38244  cdleme0moN  38246  cdleme3g  38255  cdleme3h  38256  cdleme3  38258  cdleme4  38259  cdleme4a  38260  cdleme5  38261  cdleme8  38271  cdleme9  38274  cdleme10  38275  cdleme16aN  38280  cdleme11a  38281  cdleme11fN  38285  cdleme11g  38286  cdleme11h  38287  cdleme11j  38288  cdleme11k  38289  cdleme12  38292  cdleme13  38293  cdleme17c  38309  cdleme17d1  38310  cdleme18a  38312  cdleme18b  38313  cdleme18c  38314  cdleme22gb  38315  cdlemeda  38319  cdlemednpq  38320  cdlemednuN  38321  cdleme19c  38326  cdleme20aN  38330  cdleme20bN  38331  cdleme20c  38332  cdleme22aa  38360  cdleme22a  38361  cdleme22b  38362  cdleme22d  38364  cdleme22e  38365  cdleme27cl  38387  cdleme27a  38388  cdleme30a  38399  cdleme42a  38492  cdleme42c  38493  cdleme50laut  38568  cdlemf1  38582  cdlemf  38584  cdlemfnid  38585  trlord  38590  cdlemg2fv2  38621  cdlemg2kq  38623  cdlemg2m  38625  cdlemg4a  38629  cdlemg4d  38634  cdlemg4g  38637  cdlemg4  38638  cdlemg6c  38641  cdlemg7aN  38646  cdlemg8a  38648  cdlemg8b  38649  cdlemg8c  38650  cdlemg9a  38653  cdlemg9b  38654  cdlemg9  38655  cdlemg11aq  38659  cdlemg10c  38660  cdlemg12a  38664  cdlemg12b  38665  cdlemg12c  38666  cdlemg17a  38682  cdlemg18b  38700  cdlemg18c  38701  cdlemg31b0a  38716  cdlemg31a  38718  cdlemg31b  38719  cdlemg31d  38721  cdlemg35  38734  trlcoabs2N  38743  trlcolem  38747  cdlemg44a  38752  trljco  38761  trljco2  38762  tendoco2  38789  tendopltp  38801  cdlemi1  38839  cdlemi2  38840  cdlemj3  38844  tendocan  38845  cdlemk3  38854  cdlemk4  38855  cdlemk5a  38856  cdlemk9  38860  cdlemk9bN  38861  cdlemkvcl  38863  cdlemk10  38864  cdlemk30  38915  cdlemk31  38917  cdlemk39  38937  cdlemkfid1N  38942  cdlemkid1  38943  cdlemkid2  38945  cdlemkfid3N  38946  cdlemk19ylem  38951  cdlemk19xlem  38963  cdlemk19x  38964  cdlemk53b  38977  cdlemk53  38978  cdlemk54  38979  cdlemk55a  38980  cdlemk43N  38984  cdlemk19u1  38990  cdlemk19u  38991  cdleml1N  38997  erngdvlem4  39012  erngdvlem4-rN  39020  dia11N  39069  cdlemm10N  39139  dib11N  39181  cdlemn2  39216  cdlemn10  39227  dihjustlem  39237  dihord2cN  39242  dihlsscpre  39255  dih1dimb2  39262  dihvalcq2  39268  dihopelvalcpre  39269  dihord6b  39281  dih11  39286  dihmeetlem1N  39311  dihglblem2N  39315  dihglblem3N  39316  dihmeetlem2N  39320  dihglbcpreN  39321  dihmeetcN  39323  dihmeetbclemN  39325  dihmeetlem4preN  39327  dihmeetlem9N  39336  dihmeetlem20N  39347  dihlspsnssN  39353  dihlspsnat  39354  dihatlat  39355  dihglblem6  39361  dihmeet  39364  dochss  39386  hdmapval3N  39859  hgmap11  39923  nn0rppwr  40340  remulcand  40427  congtr  40794  fzmaxdif  40810  isnumbasgrplem2  40936  ntrclsk13  41688  ssmapsn  42763  infleinf  42918  suplesup2  42922  supxrunb3  42946  mullimc  43164  mullimcf  43171  islpcn  43187  limsupresxr  43314  liminfresxr  43315  cncfuni  43434  icccncfext  43435  stoweidlem34  43582  stoweidlem59  43607  stirlinglem13  43634  fourierdlem41  43696  fourierdlem42  43697  fourierdlem73  43727  sge0iunmptlemfi  43958  meadjiunlem  44010  ovncvrrp  44109  sssmf  44283  smflimsuplem7  44370  smflimsuplem8  44371  funressneu  44552  lincscm  45782  lincext3  45808  el0ldep  45818  el0ldepsnzr  45819  itscnhlc0xyqsol  46122