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 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:  simpl12  1250  simpl22  1253  simpl32  1256  simp1l2  1268  simp2l2  1274  simp3l2  1280  3anandirs  1474  rspc3ev  3596  2nreu  4397  f1prex  7225  weniso  7295  ofmpteq  7640  tfisi  7799  mposn  8043  fprlem1  8240  smogt  8297  smocdmdom  8298  omeulem1  8507  nnmord  8557  nnmword  8558  naddasslem1  8619  naddasslem2  8620  difsnen  8983  enfixsn  9010  mapunen  9070  ac6sfi  9189  ordiso2  9426  wemaplem2  9458  wemapso2lem  9463  en2eqpr  9920  acndom  9964  infmap2  10130  cflim2  10176  cfsmolem  10183  coftr  10186  fin23lem26  10238  isf32lem9  10274  fin1a2lem9  10321  fin1a2lem10  10322  gchdomtri  10542  canth4  10560  gchpwdom  10583  gruima  10715  grudomon  10730  prn0  10902  distrlem4pr  10939  prlem934  10946  addcan  11318  addcan2  11319  divmulass  11820  divmulasscom  11821  ltmul1a  11991  supmul1  12112  uzsupss  12859  xaddass  13169  xleadd1a  13173  xlesubadd  13183  xmulass  13207  xlemul2a  13209  xadddilem  13214  xadddi  13215  ixxdisj  13281  ixxun  13282  ixxlb  13288  icoshftf1o  13395  icodisj  13397  ioounsn  13398  lincmb01cmp  13416  iccf1o  13417  elfz1b  13514  ssfzoulel  13681  fzoopth  13683  modmuladd  13838  modaddmulmod  13863  ltexp2a  14091  leexp2  14096  ltexp2r  14098  exple1  14102  expnlbnd2  14159  mulsubdivbinom2  14187  fun2dmnop0  14429  ccatass  14513  ccatopth  14640  pfxccatin12lem2a  14651  repswpfx  14709  repswccat  14710  cshwidxmodr  14728  2cshw  14737  repsco  14765  s2f1o  14841  limsupgle  15402  limsupgre  15406  addcn2  15519  mulcn2  15521  binomrisefac  15967  dvdsval2  16184  dvdsadd2b  16235  dvdsmod  16258  oexpneg  16274  sadass  16400  gcdass  16476  rplpwr  16487  lcmass  16543  coprmdvds2  16583  rpmulgcd2  16585  rpdvds  16589  coprmprod  16590  cncongr2  16597  rpexp  16651  prmdiveq  16715  hashgcdlem  16717  odzdvds  16725  coprimeprodsq2  16739  pythagtriplem3  16748  pythagtriplem4  16749  pcdvdsb  16799  vdwnnlem1  16925  0ram  16950  ramz2  16954  ramub1lem1  16956  mremre  17524  mrieqv2d  17563  lubss  18437  lubun  18439  clatleglb  18442  clatglbss  18443  mrelatglb  18484  isnsgrp  18615  issubmnd  18653  gsumccat  18733  frmdss2  18755  submefmnd  18787  nmzsubg  19062  ghmnsgima  19137  gsmsymgreqlem1  19327  psgnunilem4  19394  odmodnn0  19437  odnncl  19442  odmod  19443  oddvds  19444  odeq  19447  odmulgid  19451  odmulgeq  19454  odbezout  19455  odf1o1  19469  odf1o2  19470  odngen  19474  gexdvdsi  19480  pgpfi1  19492  odcau  19501  subgslw  19513  fislw  19522  lsmless1x  19541  lsmless2x  19542  lsmsubm  19550  lsmmod  19572  lsmmod2  19573  efgsfo  19636  odadd1  19745  odadd2  19746  odadd  19747  lsmcomx  19753  prdscmnd  19758  gsumconst  19831  ablsimpgfindlem1  20006  srg1zr  20118  csrgbinom  20135  ring1eq0  20201  mulgass2  20212  rngisom1  20369  rhmdvdsr  20411  cntzsubrng  20470  cntzsubr  20509  isabvd  20715  rmodislmod  20851  0lmhm  20962  lmhmvsca  20967  reslmhm2b  20976  pwssplit1  20981  pwssplit2  20982  pwssplit3  20983  lbspss  21004  lspsnat  21070  lidldvgen  21259  xrsdsreclblem  21337  cssmre  21618  obs2ss  21654  uvcresum  21718  frlmsslsp  21721  frlmup4  21726  lindff1  21745  f1lindf  21747  lsslindf  21755  islindf4  21763  issubassa  21792  evlsval2  22010  coe1subfv  22168  coe1sclmul  22184  coe1sclmul2  22186  mpomatmul  22349  mamutpos  22361  scmatscmide  22410  mavmulsolcl  22454  mulmarep1gsum2  22477  mdetdiaglem  22501  mdetdiag  22502  mdetunilem1  22515  mdetunilem3  22517  mdetunilem9  22523  maducoeval2  22543  madurid  22547  slesolinvbi  22584  cramerimplem1  22586  cramerlem1  22590  cramer  22594  cpmatel2  22616  m2cpm  22644  m2pmfzmap  22650  m2cpminvid2lem  22657  m2cpminvid2  22658  decpmatmul  22675  pmatcollpw1lem2  22678  pmatcollpw1  22679  pmatcollpw2lem  22680  pmatcollpwfi  22685  pm2mpcl  22700  mply1topmatcl  22708  mp2pm2mplem2  22710  mp2pm2mplem4  22712  mp2pm2mplem5  22713  mp2pm2mp  22714  pm2mpghmlem2  22715  pm2mpghmlem1  22716  chfacfisfcpmat  22758  topssnei  23027  cnconst2  23186  cnpresti  23191  cnprest2  23193  cnpdis  23196  cnt0  23249  cnt1  23253  cnhaus  23257  sscmp  23308  hauscmp  23310  cnconn  23325  unconn  23332  finlocfin  23423  comppfsc  23435  kgen2ss  23458  ptpjopn  23515  prdstopn  23531  ptrescn  23542  qtopss  23618  kqfvima  23633  fbssint  23741  fbasrn  23787  filuni  23788  fmss  23849  rnelfm  23856  fmufil  23862  fmco  23864  flimss2  23875  flimss1  23876  flimrest  23886  cnpflf2  23903  flfcnp  23907  supnfcls  23923  fclsss1  23925  fclsss2  23926  isfcf  23937  subgntr  24010  opnsubg  24011  cldsubg  24014  ghmcnp  24018  ustuqtop1  24145  bldisj  24302  blgt0  24303  bl2in  24304  blss2ps  24307  blss2  24308  blssps  24328  blss  24329  xmetresbl  24341  lpbl  24407  blcld  24409  stdbdmopn  24422  metcnp3  24444  metcnp  24445  metcnp2  24446  txmetcnp  24451  blval2  24466  nmoix  24633  nmoi2  24634  nmotri  24643  metdsge  24754  metdseq0  24759  iocopnst  24853  xrhmeo  24860  nmhmcn  25036  cphsqrtcl2  25102  cphsqrtcl3  25103  cssbn  25291  pjth  25355  ovoliunlem2  25420  volun  25462  mbfimaopn2  25574  iblconst  25735  limcvallem  25788  dvfval  25814  dvcnp2  25837  dvcnp2OLD  25838  dvcn  25839  deg1mul3le  26038  deg1tmle  26039  dvdsq1p  26084  idomrootle  26094  ig1peu  26096  ig1pdvds  26101  ply1term  26125  coeid3  26161  dgrmulc  26193  dvply1  26207  aaliou2  26264  efcvx  26375  tanord  26463  eflogeq  26527  logdivlti  26545  logccv  26588  recxpcl  26600  cxplea  26621  cxpeq  26683  ang180  26740  isosctrlem2  26745  cxp2lim  26903  amgm  26917  muval1  27059  dvdssqf  27064  mumullem2  27106  mumul  27107  bcmono  27204  lgsneg  27248  lgsdilem  27251  lgsdirprm  27258  lgsdir  27259  lgsdi  27261  lgsne0  27262  nolesgn2o  27599  nogesgn1o  27601  nosep1o  27609  nosep2o  27610  nosepssdm  27614  nosupres  27635  nosupbnd1lem1  27636  nosupbnd1lem4  27639  nosupbnd1lem5  27640  nosupbnd1lem6  27641  noinfres  27650  noinfbnd1lem1  27651  noinfbnd1lem4  27654  noinfbnd1lem6  27656  noinfbnd2  27659  noetasuplem3  27663  noetainflem3  27667  slelss  27841  cofsslt  27849  coinitsslt  27850  cofcutrtime  27858  addsass  27935  addsdi  28081  mulsass  28092  sltmul2  28097  divsmulw  28119  brbtwn2  28868  colinearalglem1  28869  colinearalg  28873  axcgrtr  28878  axsegconlem8  28887  axsegconlem9  28888  axsegconlem10  28889  axcontlem2  28928  axcontlem10  28936  elntg2  28948  ewlkle  29569  crctcshwlkn0lem5  29777  wwlknp  29806  wwlksnext  29856  wwlksnextproplem1  29872  wspthsnwspthsnon  29879  clwlkclwwlklem3  29963  erclwwlksym  29983  erclwwlknsym  30032  upgriseupth  30169  eucrct2eupth  30207  3cyclfrgrrn  30248  numclwwlk2lem1lem  30304  numclwwlk1lem2foa  30316  frgrregord13  30358  nvmul0or  30612  ipval2lem2  30666  lnoadd  30720  lnosub  30721  lnomul  30722  shless  31321  shlej1  31322  kbmul  31917  homco2  31939  kbass2  32079  eliccelico  32733  elicoelioo  32734  iocinioc2  32735  iocinif  32737  difioo  32738  nexple  32802  swrdrn2  32909  swrdrn3  32910  xrge0adddir  32985  xrge0npcan  32987  isarchi2  33137  archiabl  33150  pidlnz  33323  lindssn  33325  ssmxidl  33421  pstmfval  33862  fmcncfil  33897  zrhnm  33933  qqhnm  33956  volfiniune  34196  dya2iocnrect  34248  probinc  34388  cndprob01  34402  signswmnd  34524  bnj517  34851  cvmsss2  35246  cvmlift2lem10  35284  br6  35729  funsseq  35740  cgrtriv  35975  5segofs  35979  btwnouttr2  35995  btwnxfr  36029  lineext  36049  btwnconn1lem13  36072  brsegle2  36082  nn0prpwlem  36295  weiunpo  36438  weiunso  36439  weiunfr  36440  weiunse  36441  lindsenlbs  37594  blbnd  37766  ismtyima  37782  rrndstprj2  37810  ghomdiv  37871  grpokerinj  37872  lsatfixedN  38987  lssat  38994  lshpkrlem4  39091  cvrcon3b  39255  atlen0  39288  atcvreq0  39292  atnle  39295  atlatmstc  39297  atlatle  39298  cvlcvr1  39317  hlsupr2  39366  hlrelat2  39382  cvrexchlem  39398  lnnat  39406  atcvrj2b  39411  3dimlem3  39440  3dim1  39446  1cvrjat  39454  llni  39487  llni2  39491  llnexatN  39500  2llnmat  39503  lplni  39511  2atnelpln  39523  llncvrlpln2  39536  2llnmj  39539  lplnexatN  39542  lplnexllnN  39543  2llnm3N  39548  lvoli  39554  lvoli3  39556  lvolnle3at  39561  islvol2aN  39571  4atlem4a  39578  4atlem4b  39579  4atlem11  39588  lplncvrlvol2  39594  2lplnmj  39601  islinei  39719  linepmap  39754  lnjatN  39759  lncvrat  39761  lncmp  39762  elpaddn0  39779  elpaddatriN  39782  elpaddat  39783  paddcom  39792  paddss2  39797  paddss12  39798  paddasslem4  39802  paddasslem9  39807  paddasslem10  39808  pmodl42N  39830  pmapjoin  39831  llnmod1i2  39839  polcon2bN  39899  pclfinclN  39929  poml4N  39932  poml6N  39934  osumcllem1N  39935  osumcllem2N  39936  osumcllem11N  39945  osumclN  39946  pmapojoinN  39947  pexmidlem2N  39950  pexmidlem3N  39951  pexmidlem4N  39952  pexmidlem6N  39954  pexmidlem7N  39955  pl42lem2N  39959  pl42lem3N  39960  pl42lem4N  39961  pl42N  39962  lhprelat3N  40019  4atex  40055  lauteq  40074  lautco  40076  ltrncoidN  40107  ltrneq2  40127  ltrnideq  40154  trlnle  40165  trlval3  40166  cdlemc  40176  cdlemd9  40185  cdlemd  40186  cdleme21j  40315  cdleme21  40316  cdleme29ex  40353  cdlemefr27cl  40382  cdlemefs27cl  40392  cdleme32d  40423  cdleme32f  40425  cdleme35h2  40436  cdleme40m  40446  cdleme17d3  40475  cdleme48fvg  40479  cdlemeg46fvcl  40485  cdlemeg46fgN  40513  cdleme48fgv  40517  cdleme50trn3  40532  cdlemb3  40585  cdlemg8  40610  cdlemg11a  40616  cdlemg15a  40634  cdlemg15  40635  cdlemg16  40636  cdlemg16z  40638  cdlemg17dN  40642  cdlemg24  40667  cdlemg37  40668  cdlemg29  40684  cdlemg33b  40686  cdlemg38  40694  cdlemg40  40696  trlco  40706  cdlemg44b  40711  ltrncom  40717  trljco  40719  tendococl  40751  tendoplcl  40760  tendoplcom  40761  cdlemj2  40801  tendoid0  40804  tendo1ne0  40807  cdlemk25-3  40883  cdlemk36  40892  cdlemkid4  40913  cdlemk19x  40922  cdlemk53  40936  cdlemk56  40950  cdleml5N  40959  tendospcanN  41002  cdlemm10N  41097  dihord6apre  41235  dihord  41243  dihmeetlem1N  41269  dihglblem2N  41273  dihmeetlem2N  41278  dihmeetbN  41282  dihmeetlem5  41287  dihmeetlem6  41288  dihmeetlem7N  41289  dihmeetlem10N  41295  dihmeetlem12N  41297  dihmeetlem16N  41301  dihmeetlem17N  41302  dihmeetlem18N  41303  dihmeetALTN  41306  dihlspsnssN  41311  dvh3dim2  41427  dvh3dim3N  41428  lcfrlem16  41537  mapdrvallem2  41624  mapdh8ad  41758  hgmapvvlem3  41904  sticksstones1  42119  sticksstones2  42120  aks6d1c6isolem1  42147  resubcan2  42361  diophrw  42732  eldioph2lem1  42733  diophrex  42748  rencldnfi  42794  pellexlem2  42803  pellqrexplicit  42850  infmrgelbi  42851  pellfundglb  42858  pellfund14gap  42860  rmxycomplete  42890  congadd  42939  acongeq  42956  jm2.19  42966  jm2.23  42969  jm2.20nn  42970  jm2.27  42981  jm3.1  42993  lnmepi  43058  lmhmlnmsplit  43060  hbtlem2  43097  dgraa0p  43122  proot1hash  43168  iocunico  43184  iocinico  43185  oasubex  43259  cantnf2  43298  onmcl  43304  omcl2  43306  nadd2rabex  43359  nadd1rabtr  43361  nadd1rabex  43363  fzunt  43428  relexpxpmin  43690  ntrclsk3  44043  grur1cld  44205  ismnu  44234  grumnudlem  44258  ismnushort  44274  rfcnnnub  45014  uzwo4  45031  wessf1ornlem  45163  supxrge  45318  infleinflem2  45351  iccintsng  45505  climsuse  45590  lptre2pt  45622  limcleqr  45626  0ellimcdiv  45631  fnlimfvre  45656  dvnprodlem1  45928  volioc  45954  stoweidlem17  45999  stoweidlem19  46001  stoweidlem20  46002  stoweidlem22  46004  stoweidlem28  46010  stoweidlem34  46016  stoweidlem44  46026  stoweidlem60  46042  wallispilem3  46049  fourierdlem42  46131  fourierdlem48  46136  fourierdlem51  46139  fourierdlem54  46142  fourierdlem74  46162  fourierdlem77  46165  fourierdlem87  46175  fourierdlem97  46185  ioorrnopnlem  46286  ovnsubaddlem2  46553  smfinflem  46799  fsupdm  46824  finfdm  46828  eluzge0nn0  47297  fzopredsuc  47308  imasetpreimafvbijlemfv  47387  lighneallem4  47595  oexpnegALTV  47662  oexpnegnz  47663  tgblthelfgott  47800  clnbgrgrim  47918  isubgr3stgrlem3  47951  rmsupp0  48340  rmsuppss  48342  lincresunit3lem3  48447  lincresunit3lem2  48453  lindssnlvec  48459  fdivmptf  48514  refdivmptf  48515  elbigolo1  48530  rrx2linest  48715  itsclc0lem1  48729  itsclc0lem2  48730  itsclc0yqsollem1  48735  itsclc0b  48745  setc1onsubc  49575