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  7194  eqfunresadj  7294  tfisi  7789  offsplitfpar  8049  poseq  8088  omeulem2  8498  uniinqs  8721  unxpdomlem3  9142  elfiun  9314  cantnffval  9553  tcrank  9774  cofsmo  10157  isfin2-2  10207  tskint  10673  tskun  10674  tskurn  10677  gruina  10706  dedekind  11273  subaddmulsub  11577  dmdcan  11828  lt2msq1  12003  supmullem1  12089  supmul  12091  xaddass  13145  xaddass2  13146  xlt2add  13156  xmulasslem3  13182  xadddi2r  13194  iccsplit  13382  expaddzlem  14009  expaddz  14010  expmulz  14012  ccatopth2  14621  pfxccat3  14638  resqrtcl  15157  limsupgle  15381  o1add  15518  o1mul  15519  o1sub  15520  bitsfzo  16343  sadfval  16360  smufval  16385  nn0rppwr  16469  prmexpb  16627  4sqlem18  16871  vdwlem10  16899  fsets  17077  setsstruct2  17082  submre  17504  mrelatlub  18465  chnccat  18529  gsmsymgreqlem2  19341  mndodcong  19452  subgabl  19746  gex2abl  19761  ogrpinvlt  20054  cntzsubrng  20480  cntzsubr  20519  abvres  20744  lbsind2  21013  lspsneu  21058  lbsextlem2  21094  lbsextg  21097  lindfind2  21753  matring  22356  maducoeval  22552  maducoeval2  22553  maduf  22554  madurid  22557  gsummatr01  22572  cramerimplem3  22598  cnprest  23202  hausnei2  23266  isreg2  23290  cmpcld  23315  llyrest  23398  nllyrest  23399  csdfil  23807  hausflimlem  23892  ssblps  24335  ssbl  24336  cphassi  25139  cphassir  25140  4cphipval2  25167  cphipval  25168  dvres2  25838  plyadd  26147  plymul  26148  coeeu  26155  vieta1  26245  aalioulem3  26267  aalioulem4  26268  efgh  26475  cxpadd  26613  cxpsub  26616  mulcxp  26619  divcxp  26621  cxple2  26631  cxplt2  26632  cxpcn3lem  26682  angcan  26737  ang180lem5  26748  isosctrlem3  26755  logexprlim  27161  lgssq  27273  abvcxp  27551  padicabv  27566  nosupbnd2lem1  27652  noinfbnd2lem1  27667  nosupinfsep  27669  noetalem1  27678  sltmul2  28108  brbtwn2  28881  ax5seglem6  28910  axcontlem4  28943  axcontlem8  28947  uhgr2edg  29184  nbgrisvtx  29317  nbupgrres  29340  clwwlkccat  29965  clwwlknonex2lem2  30083  frgrreggt1  30368  chscllem4  31615  cshwrnid  32937  ifscgr  36077  matunitlindflem1  37655  lshpnelb  39022  lfl1  39108  lshpkrlem6  39153  lshpkrex  39156  hlrelat3  39450  atbtwnexOLDN  39485  atbtwnex  39486  3dim3  39507  3atlem5  39525  2llnmat  39562  lvolex3N  39576  lvolnle3at  39620  4atlem11  39647  4atlem12  39650  dalemccea  39721  cdlema2N  39830  paddasslem2  39859  atmod1i1m  39896  lhp2lt  40039  lhp0lt  40041  lhpj1  40060  lhpmcvr4N  40064  lhpelim  40075  lhpmod2i2  40076  lhpmod6i1  40077  cdlemb2  40079  lhple  40080  lhpat  40081  4atex  40114  4atex2-0aOLDN  40116  4atex3  40119  ldilco  40154  ltrncl  40163  ltrn11  40164  ltrnle  40167  ltrncnvleN  40168  ltrnm  40169  ltrnj  40170  ltrncvr  40171  ltrnatb  40175  ltrnel  40177  ltrncnvel  40180  ltrncnv  40184  trlval2  40201  trlcnv  40203  trljat1  40204  trljat2  40205  trl0  40208  ltrnnidn  40212  trlnidatb  40215  cdlemc1  40229  cdlemc2  40230  cdlemc5  40233  cdlemc6  40234  cdlemd3  40238  cdlemd6  40241  cdleme0aa  40248  cdleme0b  40250  cdleme0c  40251  cdleme0e  40255  cdleme0fN  40256  cdleme01N  40259  cdleme02N  40260  cdleme0ex1N  40261  cdleme0moN  40263  cdleme3g  40272  cdleme3h  40273  cdleme3  40275  cdleme4  40276  cdleme4a  40277  cdleme5  40278  cdleme8  40288  cdleme9  40291  cdleme10  40292  cdleme16aN  40297  cdleme11a  40298  cdleme11fN  40302  cdleme11g  40303  cdleme11h  40304  cdleme11j  40305  cdleme11k  40306  cdleme12  40309  cdleme13  40310  cdleme17c  40326  cdleme17d1  40327  cdleme18a  40329  cdleme18b  40330  cdleme18c  40331  cdleme22gb  40332  cdlemeda  40336  cdlemednpq  40337  cdlemednuN  40338  cdleme19c  40343  cdleme20aN  40347  cdleme20bN  40348  cdleme20c  40349  cdleme22aa  40377  cdleme22a  40378  cdleme22b  40379  cdleme22d  40381  cdleme22e  40382  cdleme27cl  40404  cdleme27a  40405  cdleme30a  40416  cdleme42a  40509  cdleme42c  40510  cdleme50laut  40585  cdlemf1  40599  cdlemf  40601  cdlemfnid  40602  trlord  40607  cdlemg2fv2  40638  cdlemg2kq  40640  cdlemg2m  40642  cdlemg4a  40646  cdlemg4d  40651  cdlemg4g  40654  cdlemg4  40655  cdlemg6c  40658  cdlemg7aN  40663  cdlemg8a  40665  cdlemg8b  40666  cdlemg8c  40667  cdlemg9a  40670  cdlemg9b  40671  cdlemg9  40672  cdlemg11aq  40676  cdlemg10c  40677  cdlemg12a  40681  cdlemg12b  40682  cdlemg12c  40683  cdlemg17a  40699  cdlemg18b  40717  cdlemg18c  40718  cdlemg31b0a  40733  cdlemg31a  40735  cdlemg31b  40736  cdlemg31d  40738  cdlemg35  40751  trlcoabs2N  40760  trlcolem  40764  cdlemg44a  40769  trljco  40778  trljco2  40779  tendoco2  40806  tendopltp  40818  cdlemi1  40856  cdlemi2  40857  cdlemj3  40861  tendocan  40862  cdlemk3  40871  cdlemk4  40872  cdlemk5a  40873  cdlemk9  40877  cdlemk9bN  40878  cdlemkvcl  40880  cdlemk10  40881  cdlemk30  40932  cdlemk31  40934  cdlemk39  40954  cdlemkfid1N  40959  cdlemkid1  40960  cdlemkid2  40962  cdlemkfid3N  40963  cdlemk19ylem  40968  cdlemk19xlem  40980  cdlemk19x  40981  cdlemk53b  40994  cdlemk53  40995  cdlemk54  40996  cdlemk55a  40997  cdlemk43N  41001  cdlemk19u1  41007  cdlemk19u  41008  cdleml1N  41014  erngdvlem4  41029  erngdvlem4-rN  41037  dia11N  41086  cdlemm10N  41156  dib11N  41198  cdlemn2  41233  cdlemn10  41244  dihjustlem  41254  dihord2cN  41259  dihlsscpre  41272  dih1dimb2  41279  dihvalcq2  41285  dihopelvalcpre  41286  dihord6b  41298  dih11  41303  dihmeetlem1N  41328  dihglblem2N  41332  dihglblem3N  41333  dihmeetlem2N  41337  dihglbcpreN  41338  dihmeetcN  41340  dihmeetbclemN  41342  dihmeetlem4preN  41344  dihmeetlem9N  41353  dihmeetlem20N  41364  dihlspsnssN  41370  dihlspsnat  41371  dihatlat  41372  dihglblem6  41378  dihmeet  41381  dochss  41403  hdmapval3N  41876  hgmap11  41940  remulcand  42471  congtr  42997  fzmaxdif  43013  isnumbasgrplem2  43136  ntrclsk13  44103  ssmapsn  45252  infleinf  45409  suplesup2  45413  supxrunb3  45436  mullimc  45655  mullimcf  45662  islpcn  45676  limsupresxr  45803  liminfresxr  45804  cncfuni  45923  icccncfext  45924  stoweidlem34  46071  stoweidlem59  46096  stirlinglem13  46123  fourierdlem41  46185  fourierdlem42  46186  fourierdlem73  46216  sge0iunmptlemfi  46450  meadjiunlem  46502  ovncvrrp  46601  sssmf  46775  smflimsuplem7  46863  smflimsuplem8  46864  ormkglobd  46912  funressneu  47077  grlimedgclnbgr  48025  lincscm  48461  lincext3  48487  el0ldep  48497  el0ldepsnzr  48498  itscnhlc0xyqsol  48796  uptr2  49252