Theorem simpl2 1193

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl2	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simpl2

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2	1	3ad2antl2 1187	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

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

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 1089

This theorem is referenced by:  simpl12  1250  simpl22  1253  simpl32  1256  simp1l2  1268  simp2l2  1274  simp3l2  1280  3anandirs  1474  rspc3ev  3639  2nreu  4444  f1prex  7304  weniso  7374  ofmpteq  7720  tfisi  7880  mposn  8128  fprlem1  8325  smogt  8407  smocdmdom  8408  omeulem1  8620  nnmord  8670  nnmword  8671  naddasslem1  8732  naddasslem2  8733  difsnen  9093  enfixsn  9121  mapunen  9186  ac6sfi  9320  ordiso2  9555  wemaplem2  9587  wemapso2lem  9592  en2eqpr  10047  acndom  10091  infmap2  10257  cflim2  10303  cfsmolem  10310  coftr  10313  fin23lem26  10365  isf32lem9  10401  fin1a2lem9  10448  fin1a2lem10  10449  gchdomtri  10669  canth4  10687  gchpwdom  10710  gruima  10842  grudomon  10857  prn0  11029  distrlem4pr  11066  prlem934  11073  addcan  11445  addcan2  11446  divmulass  11945  divmulasscom  11946  ltmul1a  12116  supmul1  12237  uzsupss  12982  xaddass  13291  xleadd1a  13295  xlesubadd  13305  xmulass  13329  xlemul2a  13331  xadddilem  13336  xadddi  13337  ixxdisj  13402  ixxun  13403  ixxlb  13409  icoshftf1o  13514  icodisj  13516  ioounsn  13517  lincmb01cmp  13535  iccf1o  13536  elfz1b  13633  ssfzoulel  13799  fzoopth  13801  modmuladd  13954  modaddmulmod  13979  ltexp2a  14206  leexp2  14211  ltexp2r  14213  exple1  14216  expnlbnd2  14273  mulsubdivbinom2  14301  fun2dmnop0  14543  ccatass  14626  ccatopth  14754  pfxccatin12lem2a  14765  repswpfx  14823  repswccat  14824  cshwidxmodr  14842  2cshw  14851  repsco  14879  s2f1o  14955  limsupgle  15513  limsupgre  15517  addcn2  15630  mulcn2  15632  binomrisefac  16078  dvdsval2  16293  dvdsadd2b  16343  dvdsmod  16366  oexpneg  16382  sadass  16508  gcdass  16584  rplpwr  16595  lcmass  16651  coprmdvds2  16691  rpmulgcd2  16693  rpdvds  16697  coprmprod  16698  cncongr2  16705  rpexp  16759  prmdiveq  16823  hashgcdlem  16825  odzdvds  16833  coprimeprodsq2  16847  pythagtriplem3  16856  pythagtriplem4  16857  pcdvdsb  16907  vdwnnlem1  17033  0ram  17058  ramz2  17062  ramub1lem1  17064  mremre  17647  mrieqv2d  17682  lubss  18558  lubun  18560  clatleglb  18563  clatglbss  18564  mrelatglb  18605  isnsgrp  18736  issubmnd  18774  gsumccat  18854  frmdss2  18876  submefmnd  18908  nmzsubg  19183  ghmnsgima  19258  gsmsymgreqlem1  19448  psgnunilem4  19515  odmodnn0  19558  odnncl  19563  odmod  19564  oddvds  19565  odeq  19568  odmulgid  19572  odmulgeq  19575  odbezout  19576  odf1o1  19590  odf1o2  19591  odngen  19595  gexdvdsi  19601  pgpfi1  19613  odcau  19622  subgslw  19634  fislw  19643  lsmless1x  19662  lsmless2x  19663  lsmsubm  19671  lsmmod  19693  lsmmod2  19694  efgsfo  19757  odadd1  19866  odadd2  19867  odadd  19868  lsmcomx  19874  prdscmnd  19879  gsumconst  19952  ablsimpgfindlem1  20127  srg1zr  20212  csrgbinom  20229  ring1eq0  20295  mulgass2  20306  rngisom1  20466  rhmdvdsr  20508  cntzsubrng  20567  cntzsubr  20606  isabvd  20813  rmodislmod  20928  0lmhm  21039  lmhmvsca  21044  reslmhm2b  21053  pwssplit1  21058  pwssplit2  21059  pwssplit3  21060  lbspss  21081  lspsnat  21147  lidldvgen  21344  xrsdsreclblem  21430  cssmre  21711  obs2ss  21749  uvcresum  21813  frlmsslsp  21816  frlmup4  21821  lindff1  21840  f1lindf  21842  lsslindf  21850  islindf4  21858  issubassa  21887  evlsval2  22111  coe1subfv  22269  coe1sclmul  22285  coe1sclmul2  22287  mpomatmul  22452  mamutpos  22464  scmatscmide  22513  mavmulsolcl  22557  mulmarep1gsum2  22580  mdetdiaglem  22604  mdetdiag  22605  mdetunilem1  22618  mdetunilem3  22620  mdetunilem9  22626  maducoeval2  22646  madurid  22650  slesolinvbi  22687  cramerimplem1  22689  cramerlem1  22693  cramer  22697  cpmatel2  22719  m2cpm  22747  m2pmfzmap  22753  m2cpminvid2lem  22760  m2cpminvid2  22761  decpmatmul  22778  pmatcollpw1lem2  22781  pmatcollpw1  22782  pmatcollpw2lem  22783  pmatcollpwfi  22788  pm2mpcl  22803  mply1topmatcl  22811  mp2pm2mplem2  22813  mp2pm2mplem4  22815  mp2pm2mplem5  22816  mp2pm2mp  22817  pm2mpghmlem2  22818  pm2mpghmlem1  22819  chfacfisfcpmat  22861  topssnei  23132  cnconst2  23291  cnpresti  23296  cnprest2  23298  cnpdis  23301  cnt0  23354  cnt1  23358  cnhaus  23362  sscmp  23413  hauscmp  23415  cnconn  23430  unconn  23437  finlocfin  23528  comppfsc  23540  kgen2ss  23563  ptpjopn  23620  prdstopn  23636  ptrescn  23647  qtopss  23723  kqfvima  23738  fbssint  23846  fbasrn  23892  filuni  23893  fmss  23954  rnelfm  23961  fmufil  23967  fmco  23969  flimss2  23980  flimss1  23981  flimrest  23991  cnpflf2  24008  flfcnp  24012  supnfcls  24028  fclsss1  24030  fclsss2  24031  isfcf  24042  subgntr  24115  opnsubg  24116  cldsubg  24119  ghmcnp  24123  ustuqtop1  24250  bldisj  24408  blgt0  24409  bl2in  24410  blss2ps  24413  blss2  24414  blssps  24434  blss  24435  xmetresbl  24447  lpbl  24516  blcld  24518  stdbdmopn  24531  metcnp3  24553  metcnp  24554  metcnp2  24555  txmetcnp  24560  blval2  24575  nmoix  24750  nmoi2  24751  nmotri  24760  metdsge  24871  metdseq0  24876  iocopnst  24970  xrhmeo  24977  nmhmcn  25153  cphsqrtcl2  25220  cphsqrtcl3  25221  cssbn  25409  pjth  25473  ovoliunlem2  25538  volun  25580  mbfimaopn2  25692  iblconst  25853  limcvallem  25906  dvfval  25932  dvcnp2  25955  dvcnp2OLD  25956  dvcn  25957  deg1mul3le  26156  deg1tmle  26157  dvdsq1p  26202  idomrootle  26212  ig1peu  26214  ig1pdvds  26219  ply1term  26243  coeid3  26279  dgrmulc  26311  dvply1  26325  aaliou2  26382  efcvx  26493  tanord  26580  eflogeq  26644  logdivlti  26662  logccv  26705  recxpcl  26717  cxplea  26738  cxpeq  26800  ang180  26857  isosctrlem2  26862  cxp2lim  27020  amgm  27034  muval1  27176  dvdssqf  27181  mumullem2  27223  mumul  27224  bcmono  27321  lgsneg  27365  lgsdilem  27368  lgsdirprm  27375  lgsdir  27376  lgsdi  27378  lgsne0  27379  nolesgn2o  27716  nogesgn1o  27718  nosep1o  27726  nosep2o  27727  nosepssdm  27731  nosupres  27752  nosupbnd1lem1  27753  nosupbnd1lem4  27756  nosupbnd1lem5  27757  nosupbnd1lem6  27758  noinfres  27767  noinfbnd1lem1  27768  noinfbnd1lem4  27771  noinfbnd1lem6  27773  noinfbnd2  27776  noetasuplem3  27780  noetainflem3  27784  slelss  27946  cofsslt  27952  coinitsslt  27953  cofcutrtime  27961  addsass  28038  addsdi  28181  mulsass  28192  sltmul2  28197  divsmulw  28218  brbtwn2  28920  colinearalglem1  28921  colinearalg  28925  axcgrtr  28930  axsegconlem8  28939  axsegconlem9  28940  axsegconlem10  28941  axcontlem2  28980  axcontlem10  28988  elntg2  29000  ewlkle  29623  crctcshwlkn0lem5  29834  wwlknp  29863  wwlksnext  29913  wwlksnextproplem1  29929  wspthsnwspthsnon  29936  clwlkclwwlklem3  30020  erclwwlksym  30040  erclwwlknsym  30089  upgriseupth  30226  eucrct2eupth  30264  3cyclfrgrrn  30305  numclwwlk2lem1lem  30361  numclwwlk1lem2foa  30373  frgrregord13  30415  nvmul0or  30669  ipval2lem2  30723  lnoadd  30777  lnosub  30778  lnomul  30779  shless  31378  shlej1  31379  kbmul  31974  homco2  31996  kbass2  32136  eliccelico  32779  elicoelioo  32780  iocinioc2  32781  iocinif  32783  difioo  32784  nexple  32833  swrdrn2  32939  swrdrn3  32940  xrge0adddir  33023  xrge0npcan  33025  isarchi2  33192  archiabl  33205  pidlnz  33404  lindssn  33406  ssmxidl  33502  pstmfval  33895  fmcncfil  33930  zrhnm  33968  qqhnm  33991  volfiniune  34231  dya2iocnrect  34283  probinc  34423  cndprob01  34437  signswmnd  34572  bnj517  34899  cvmsss2  35279  cvmlift2lem10  35317  br6  35757  funsseq  35768  cgrtriv  36003  5segofs  36007  btwnouttr2  36023  btwnxfr  36057  lineext  36077  btwnconn1lem13  36100  brsegle2  36110  nn0prpwlem  36323  weiunpo  36466  weiunso  36467  weiunfr  36468  weiunse  36469  lindsenlbs  37622  blbnd  37794  ismtyima  37810  rrndstprj2  37838  ghomdiv  37899  grpokerinj  37900  lsatfixedN  39010  lssat  39017  lshpkrlem4  39114  cvrcon3b  39278  atlen0  39311  atcvreq0  39315  atnle  39318  atlatmstc  39320  atlatle  39321  cvlcvr1  39340  hlsupr2  39389  hlrelat2  39405  cvrexchlem  39421  lnnat  39429  atcvrj2b  39434  3dimlem3  39463  3dim1  39469  1cvrjat  39477  llni  39510  llni2  39514  llnexatN  39523  2llnmat  39526  lplni  39534  2atnelpln  39546  llncvrlpln2  39559  2llnmj  39562  lplnexatN  39565  lplnexllnN  39566  2llnm3N  39571  lvoli  39577  lvoli3  39579  lvolnle3at  39584  islvol2aN  39594  4atlem4a  39601  4atlem4b  39602  4atlem11  39611  lplncvrlvol2  39617  2lplnmj  39624  islinei  39742  linepmap  39777  lnjatN  39782  lncvrat  39784  lncmp  39785  elpaddn0  39802  elpaddatriN  39805  elpaddat  39806  paddcom  39815  paddss2  39820  paddss12  39821  paddasslem4  39825  paddasslem9  39830  paddasslem10  39831  pmodl42N  39853  pmapjoin  39854  llnmod1i2  39862  polcon2bN  39922  pclfinclN  39952  poml4N  39955  poml6N  39957  osumcllem1N  39958  osumcllem2N  39959  osumcllem11N  39968  osumclN  39969  pmapojoinN  39970  pexmidlem2N  39973  pexmidlem3N  39974  pexmidlem4N  39975  pexmidlem6N  39977  pexmidlem7N  39978  pl42lem2N  39982  pl42lem3N  39983  pl42lem4N  39984  pl42N  39985  lhprelat3N  40042  4atex  40078  lauteq  40097  lautco  40099  ltrncoidN  40130  ltrneq2  40150  ltrnideq  40177  trlnle  40188  trlval3  40189  cdlemc  40199  cdlemd9  40208  cdlemd  40209  cdleme21j  40338  cdleme21  40339  cdleme29ex  40376  cdlemefr27cl  40405  cdlemefs27cl  40415  cdleme32d  40446  cdleme32f  40448  cdleme35h2  40459  cdleme40m  40469  cdleme17d3  40498  cdleme48fvg  40502  cdlemeg46fvcl  40508  cdlemeg46fgN  40536  cdleme48fgv  40540  cdleme50trn3  40555  cdlemb3  40608  cdlemg8  40633  cdlemg11a  40639  cdlemg15a  40657  cdlemg15  40658  cdlemg16  40659  cdlemg16z  40661  cdlemg17dN  40665  cdlemg24  40690  cdlemg37  40691  cdlemg29  40707  cdlemg33b  40709  cdlemg38  40717  cdlemg40  40719  trlco  40729  cdlemg44b  40734  ltrncom  40740  trljco  40742  tendococl  40774  tendoplcl  40783  tendoplcom  40784  cdlemj2  40824  tendoid0  40827  tendo1ne0  40830  cdlemk25-3  40906  cdlemk36  40915  cdlemkid4  40936  cdlemk19x  40945  cdlemk53  40959  cdlemk56  40973  cdleml5N  40982  tendospcanN  41025  cdlemm10N  41120  dihord6apre  41258  dihord  41266  dihmeetlem1N  41292  dihglblem2N  41296  dihmeetlem2N  41301  dihmeetbN  41305  dihmeetlem5  41310  dihmeetlem6  41311  dihmeetlem7N  41312  dihmeetlem10N  41318  dihmeetlem12N  41320  dihmeetlem16N  41324  dihmeetlem17N  41325  dihmeetlem18N  41326  dihmeetALTN  41329  dihlspsnssN  41334  dvh3dim2  41450  dvh3dim3N  41451  lcfrlem16  41560  mapdrvallem2  41647  mapdh8ad  41781  hgmapvvlem3  41927  sticksstones1  42147  sticksstones2  42148  aks6d1c6isolem1  42175  resubcan2  42418  diophrw  42770  eldioph2lem1  42771  diophrex  42786  rencldnfi  42832  pellexlem2  42841  pellqrexplicit  42888  infmrgelbi  42889  pellfundglb  42896  pellfund14gap  42898  rmxycomplete  42929  congadd  42978  acongeq  42995  jm2.19  43005  jm2.23  43008  jm2.20nn  43009  jm2.27  43020  jm3.1  43032  lnmepi  43097  lmhmlnmsplit  43099  hbtlem2  43136  dgraa0p  43161  proot1hash  43207  iocunico  43223  iocinico  43224  oasubex  43299  cantnf2  43338  onmcl  43344  omcl2  43346  nadd2rabex  43399  nadd1rabtr  43401  nadd1rabex  43403  fzunt  43468  relexpxpmin  43730  ntrclsk3  44083  grur1cld  44251  ismnu  44280  grumnudlem  44304  ismnushort  44320  rfcnnnub  45041  uzwo4  45058  wessf1ornlem  45190  supxrge  45349  infleinflem2  45382  iccintsng  45536  climsuse  45623  lptre2pt  45655  limcleqr  45659  0ellimcdiv  45664  fnlimfvre  45689  dvnprodlem1  45961  volioc  45987  stoweidlem17  46032  stoweidlem19  46034  stoweidlem20  46035  stoweidlem22  46037  stoweidlem28  46043  stoweidlem34  46049  stoweidlem44  46059  stoweidlem60  46075  wallispilem3  46082  fourierdlem42  46164  fourierdlem48  46169  fourierdlem51  46172  fourierdlem54  46175  fourierdlem74  46195  fourierdlem77  46198  fourierdlem87  46208  fourierdlem97  46218  ioorrnopnlem  46319  ovnsubaddlem2  46586  smfinflem  46832  fsupdm  46857  finfdm  46861  eluzge0nn0  47324  fzopredsuc  47335  imasetpreimafvbijlemfv  47389  lighneallem4  47597  oexpnegALTV  47664  oexpnegnz  47665  tgblthelfgott  47802  clnbgrgrim  47902  isubgr3stgrlem3  47935  rmsupp0  48284  rmsuppss  48286  lincresunit3lem3  48391  lincresunit3lem2  48397  lindssnlvec  48403  fdivmptf  48462  refdivmptf  48463  elbigolo1  48478  rrx2linest  48663  itsclc0lem1  48677  itsclc0lem2  48678  itsclc0yqsollem1  48683  itsclc0b  48693