Theorem simp1l 1195

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 1131	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

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

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 396  df-3an 1087

This theorem is referenced by:  simp11l  1282  simp21l  1288  simp31l  1294  tfisi  7680  offsplitfpar  7931  omeulem2  8376  uniinqs  8544  unxpdomlem3  8958  elfiun  9119  cantnffval  9351  tcrank  9573  cofsmo  9956  isfin2-2  10006  tskint  10472  tskun  10473  tskurn  10476  gruina  10505  dedekind  11068  subaddmulsub  11368  dmdcan  11615  lt2msq1  11789  supmullem1  11875  supmul  11877  xaddass  12912  xaddass2  12913  xlt2add  12923  xmulasslem3  12949  xadddi2r  12961  iccsplit  13146  expaddzlem  13754  expaddz  13755  expmulz  13757  ccatopth2  14358  pfxccat3  14375  resqrtcl  14893  limsupgle  15114  o1add  15251  o1mul  15252  o1sub  15253  bitsfzo  16070  sadfval  16087  smufval  16112  prmexpb  16353  4sqlem18  16591  vdwlem10  16619  fsets  16798  setsstruct2  16803  submre  17231  mrelatlub  18195  gsmsymgreqlem2  18954  mndodcong  19065  subgabl  19352  gex2abl  19367  cntzsubr  19972  abvres  20014  lbsind2  20258  lspsneu  20300  lbsextlem2  20336  lbsextg  20339  lindfind2  20935  matring  21500  maducoeval  21696  maducoeval2  21697  maduf  21698  madurid  21701  gsummatr01  21716  cramerimplem3  21742  cnprest  22348  hausnei2  22412  isreg2  22436  cmpcld  22461  llyrest  22544  nllyrest  22545  csdfil  22953  hausflimlem  23038  ssblps  23483  ssbl  23484  cphassi  24283  cphassir  24284  4cphipval2  24311  cphipval  24312  dvres2  24981  plyadd  25283  plymul  25284  coeeu  25291  vieta1  25377  aalioulem3  25399  aalioulem4  25400  efgh  25602  cxpadd  25739  cxpsub  25742  mulcxp  25745  divcxp  25747  cxple2  25757  cxplt2  25758  cxpcn3lem  25805  angcan  25857  ang180lem5  25868  isosctrlem3  25875  logexprlim  26278  lgssq  26390  abvcxp  26668  padicabv  26683  brbtwn2  27176  ax5seglem6  27205  axcontlem4  27238  axcontlem8  27242  uhgr2edg  27478  nbgrisvtx  27611  nbupgrres  27634  clwwlkccat  28255  clwwlknonex2lem2  28373  frgrreggt1  28658  chscllem4  29903  cshwrnid  31135  ogrpinvlt  31251  eqfunresadj  33641  poseq  33729  nosupbnd2lem1  33845  noinfbnd2lem1  33860  nosupinfsep  33862  noetalem1  33871  ifscgr  34273  matunitlindflem1  35700  lshpnelb  36925  lfl1  37011  lshpkrlem6  37056  lshpkrex  37059  hlrelat3  37353  atbtwnexOLDN  37388  atbtwnex  37389  3dim3  37410  3atlem5  37428  2llnmat  37465  lvolex3N  37479  lvolnle3at  37523  4atlem11  37550  4atlem12  37553  dalemccea  37624  cdlema2N  37733  paddasslem2  37762  atmod1i1m  37799  lhp2lt  37942  lhp0lt  37944  lhpj1  37963  lhpmcvr4N  37967  lhpelim  37978  lhpmod2i2  37979  lhpmod6i1  37980  cdlemb2  37982  lhple  37983  lhpat  37984  4atex  38017  4atex2-0aOLDN  38019  4atex3  38022  ldilco  38057  ltrncl  38066  ltrn11  38067  ltrnle  38070  ltrncnvleN  38071  ltrnm  38072  ltrnj  38073  ltrncvr  38074  ltrnatb  38078  ltrnel  38080  ltrncnvel  38083  ltrncnv  38087  trlval2  38104  trlcnv  38106  trljat1  38107  trljat2  38108  trl0  38111  ltrnnidn  38115  trlnidatb  38118  cdlemc1  38132  cdlemc2  38133  cdlemc5  38136  cdlemc6  38137  cdlemd3  38141  cdlemd6  38144  cdleme0aa  38151  cdleme0b  38153  cdleme0c  38154  cdleme0e  38158  cdleme0fN  38159  cdleme01N  38162  cdleme02N  38163  cdleme0ex1N  38164  cdleme0moN  38166  cdleme3g  38175  cdleme3h  38176  cdleme3  38178  cdleme4  38179  cdleme4a  38180  cdleme5  38181  cdleme8  38191  cdleme9  38194  cdleme10  38195  cdleme16aN  38200  cdleme11a  38201  cdleme11fN  38205  cdleme11g  38206  cdleme11h  38207  cdleme11j  38208  cdleme11k  38209  cdleme12  38212  cdleme13  38213  cdleme17c  38229  cdleme17d1  38230  cdleme18a  38232  cdleme18b  38233  cdleme18c  38234  cdleme22gb  38235  cdlemeda  38239  cdlemednpq  38240  cdlemednuN  38241  cdleme19c  38246  cdleme20aN  38250  cdleme20bN  38251  cdleme20c  38252  cdleme22aa  38280  cdleme22a  38281  cdleme22b  38282  cdleme22d  38284  cdleme22e  38285  cdleme27cl  38307  cdleme27a  38308  cdleme30a  38319  cdleme42a  38412  cdleme42c  38413  cdleme50laut  38488  cdlemf1  38502  cdlemf  38504  cdlemfnid  38505  trlord  38510  cdlemg2fv2  38541  cdlemg2kq  38543  cdlemg2m  38545  cdlemg4a  38549  cdlemg4d  38554  cdlemg4g  38557  cdlemg4  38558  cdlemg6c  38561  cdlemg7aN  38566  cdlemg8a  38568  cdlemg8b  38569  cdlemg8c  38570  cdlemg9a  38573  cdlemg9b  38574  cdlemg9  38575  cdlemg11aq  38579  cdlemg10c  38580  cdlemg12a  38584  cdlemg12b  38585  cdlemg12c  38586  cdlemg17a  38602  cdlemg18b  38620  cdlemg18c  38621  cdlemg31b0a  38636  cdlemg31a  38638  cdlemg31b  38639  cdlemg31d  38641  cdlemg35  38654  trlcoabs2N  38663  trlcolem  38667  cdlemg44a  38672  trljco  38681  trljco2  38682  tendoco2  38709  tendopltp  38721  cdlemi1  38759  cdlemi2  38760  cdlemj3  38764  tendocan  38765  cdlemk3  38774  cdlemk4  38775  cdlemk5a  38776  cdlemk9  38780  cdlemk9bN  38781  cdlemkvcl  38783  cdlemk10  38784  cdlemk30  38835  cdlemk31  38837  cdlemk39  38857  cdlemkfid1N  38862  cdlemkid1  38863  cdlemkid2  38865  cdlemkfid3N  38866  cdlemk19ylem  38871  cdlemk19xlem  38883  cdlemk19x  38884  cdlemk53b  38897  cdlemk53  38898  cdlemk54  38899  cdlemk55a  38900  cdlemk43N  38904  cdlemk19u1  38910  cdlemk19u  38911  cdleml1N  38917  erngdvlem4  38932  erngdvlem4-rN  38940  dia11N  38989  cdlemm10N  39059  dib11N  39101  cdlemn2  39136  cdlemn10  39147  dihjustlem  39157  dihord2cN  39162  dihlsscpre  39175  dih1dimb2  39182  dihvalcq2  39188  dihopelvalcpre  39189  dihord6b  39201  dih11  39206  dihmeetlem1N  39231  dihglblem2N  39235  dihglblem3N  39236  dihmeetlem2N  39240  dihglbcpreN  39241  dihmeetcN  39243  dihmeetbclemN  39245  dihmeetlem4preN  39247  dihmeetlem9N  39256  dihmeetlem20N  39267  dihlspsnssN  39273  dihlspsnat  39274  dihatlat  39275  dihglblem6  39281  dihmeet  39284  dochss  39306  hdmapval3N  39779  hgmap11  39843  nn0rppwr  40254  remulcand  40341  congtr  40703  fzmaxdif  40719  isnumbasgrplem2  40845  ntrclsk13  41570  ssmapsn  42645  infleinf  42801  suplesup2  42805  supxrunb3  42829  mullimc  43047  mullimcf  43054  islpcn  43070  limsupresxr  43197  liminfresxr  43198  cncfuni  43317  icccncfext  43318  stoweidlem34  43465  stoweidlem59  43490  stirlinglem13  43517  fourierdlem41  43579  fourierdlem42  43580  fourierdlem73  43610  sge0iunmptlemfi  43841  meadjiunlem  43893  ovncvrrp  43992  sssmf  44161  smflimsuplem7  44246  smflimsuplem8  44247  funressneu  44428  lincscm  45659  lincext3  45685  el0ldep  45695  el0ldepsnzr  45696  itscnhlc0xyqsol  45999