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  3608  2nreu  4410  f1prex  7262  weniso  7332  ofmpteq  7679  tfisi  7838  mposn  8085  fprlem1  8282  smogt  8339  smocdmdom  8340  omeulem1  8549  nnmord  8599  nnmword  8600  naddasslem1  8661  naddasslem2  8662  difsnen  9027  enfixsn  9055  mapunen  9116  ac6sfi  9238  ordiso2  9475  wemaplem2  9507  wemapso2lem  9512  en2eqpr  9967  acndom  10011  infmap2  10177  cflim2  10223  cfsmolem  10230  coftr  10233  fin23lem26  10285  isf32lem9  10321  fin1a2lem9  10368  fin1a2lem10  10369  gchdomtri  10589  canth4  10607  gchpwdom  10630  gruima  10762  grudomon  10777  prn0  10949  distrlem4pr  10986  prlem934  10993  addcan  11365  addcan2  11366  divmulass  11867  divmulasscom  11868  ltmul1a  12038  supmul1  12159  uzsupss  12906  xaddass  13216  xleadd1a  13220  xlesubadd  13230  xmulass  13254  xlemul2a  13256  xadddilem  13261  xadddi  13262  ixxdisj  13328  ixxun  13329  ixxlb  13335  icoshftf1o  13442  icodisj  13444  ioounsn  13445  lincmb01cmp  13463  iccf1o  13464  elfz1b  13561  ssfzoulel  13728  fzoopth  13730  modmuladd  13885  modaddmulmod  13910  ltexp2a  14138  leexp2  14143  ltexp2r  14145  exple1  14149  expnlbnd2  14206  mulsubdivbinom2  14234  fun2dmnop0  14476  ccatass  14560  ccatopth  14688  pfxccatin12lem2a  14699  repswpfx  14757  repswccat  14758  cshwidxmodr  14776  2cshw  14785  repsco  14813  s2f1o  14889  limsupgle  15450  limsupgre  15454  addcn2  15567  mulcn2  15569  binomrisefac  16015  dvdsval2  16232  dvdsadd2b  16283  dvdsmod  16306  oexpneg  16322  sadass  16448  gcdass  16524  rplpwr  16535  lcmass  16591  coprmdvds2  16631  rpmulgcd2  16633  rpdvds  16637  coprmprod  16638  cncongr2  16645  rpexp  16699  prmdiveq  16763  hashgcdlem  16765  odzdvds  16773  coprimeprodsq2  16787  pythagtriplem3  16796  pythagtriplem4  16797  pcdvdsb  16847  vdwnnlem1  16973  0ram  16998  ramz2  17002  ramub1lem1  17004  mremre  17572  mrieqv2d  17607  lubss  18479  lubun  18481  clatleglb  18484  clatglbss  18485  mrelatglb  18526  isnsgrp  18657  issubmnd  18695  gsumccat  18775  frmdss2  18797  submefmnd  18829  nmzsubg  19104  ghmnsgima  19179  gsmsymgreqlem1  19367  psgnunilem4  19434  odmodnn0  19477  odnncl  19482  odmod  19483  oddvds  19484  odeq  19487  odmulgid  19491  odmulgeq  19494  odbezout  19495  odf1o1  19509  odf1o2  19510  odngen  19514  gexdvdsi  19520  pgpfi1  19532  odcau  19541  subgslw  19553  fislw  19562  lsmless1x  19581  lsmless2x  19582  lsmsubm  19590  lsmmod  19612  lsmmod2  19613  efgsfo  19676  odadd1  19785  odadd2  19786  odadd  19787  lsmcomx  19793  prdscmnd  19798  gsumconst  19871  ablsimpgfindlem1  20046  srg1zr  20131  csrgbinom  20148  ring1eq0  20214  mulgass2  20225  rngisom1  20382  rhmdvdsr  20424  cntzsubrng  20483  cntzsubr  20522  isabvd  20728  rmodislmod  20843  0lmhm  20954  lmhmvsca  20959  reslmhm2b  20968  pwssplit1  20973  pwssplit2  20974  pwssplit3  20975  lbspss  20996  lspsnat  21062  lidldvgen  21251  xrsdsreclblem  21336  cssmre  21609  obs2ss  21645  uvcresum  21709  frlmsslsp  21712  frlmup4  21717  lindff1  21736  f1lindf  21738  lsslindf  21746  islindf4  21754  issubassa  21783  evlsval2  22001  coe1subfv  22159  coe1sclmul  22175  coe1sclmul2  22177  mpomatmul  22340  mamutpos  22352  scmatscmide  22401  mavmulsolcl  22445  mulmarep1gsum2  22468  mdetdiaglem  22492  mdetdiag  22493  mdetunilem1  22506  mdetunilem3  22508  mdetunilem9  22514  maducoeval2  22534  madurid  22538  slesolinvbi  22575  cramerimplem1  22577  cramerlem1  22581  cramer  22585  cpmatel2  22607  m2cpm  22635  m2pmfzmap  22641  m2cpminvid2lem  22648  m2cpminvid2  22649  decpmatmul  22666  pmatcollpw1lem2  22669  pmatcollpw1  22670  pmatcollpw2lem  22671  pmatcollpwfi  22676  pm2mpcl  22691  mply1topmatcl  22699  mp2pm2mplem2  22701  mp2pm2mplem4  22703  mp2pm2mplem5  22704  mp2pm2mp  22705  pm2mpghmlem2  22706  pm2mpghmlem1  22707  chfacfisfcpmat  22749  topssnei  23018  cnconst2  23177  cnpresti  23182  cnprest2  23184  cnpdis  23187  cnt0  23240  cnt1  23244  cnhaus  23248  sscmp  23299  hauscmp  23301  cnconn  23316  unconn  23323  finlocfin  23414  comppfsc  23426  kgen2ss  23449  ptpjopn  23506  prdstopn  23522  ptrescn  23533  qtopss  23609  kqfvima  23624  fbssint  23732  fbasrn  23778  filuni  23779  fmss  23840  rnelfm  23847  fmufil  23853  fmco  23855  flimss2  23866  flimss1  23867  flimrest  23877  cnpflf2  23894  flfcnp  23898  supnfcls  23914  fclsss1  23916  fclsss2  23917  isfcf  23928  subgntr  24001  opnsubg  24002  cldsubg  24005  ghmcnp  24009  ustuqtop1  24136  bldisj  24293  blgt0  24294  bl2in  24295  blss2ps  24298  blss2  24299  blssps  24319  blss  24320  xmetresbl  24332  lpbl  24398  blcld  24400  stdbdmopn  24413  metcnp3  24435  metcnp  24436  metcnp2  24437  txmetcnp  24442  blval2  24457  nmoix  24624  nmoi2  24625  nmotri  24634  metdsge  24745  metdseq0  24750  iocopnst  24844  xrhmeo  24851  nmhmcn  25027  cphsqrtcl2  25093  cphsqrtcl3  25094  cssbn  25282  pjth  25346  ovoliunlem2  25411  volun  25453  mbfimaopn2  25565  iblconst  25726  limcvallem  25779  dvfval  25805  dvcnp2  25828  dvcnp2OLD  25829  dvcn  25830  deg1mul3le  26029  deg1tmle  26030  dvdsq1p  26075  idomrootle  26085  ig1peu  26087  ig1pdvds  26092  ply1term  26116  coeid3  26152  dgrmulc  26184  dvply1  26198  aaliou2  26255  efcvx  26366  tanord  26454  eflogeq  26518  logdivlti  26536  logccv  26579  recxpcl  26591  cxplea  26612  cxpeq  26674  ang180  26731  isosctrlem2  26736  cxp2lim  26894  amgm  26908  muval1  27050  dvdssqf  27055  mumullem2  27097  mumul  27098  bcmono  27195  lgsneg  27239  lgsdilem  27242  lgsdirprm  27249  lgsdir  27250  lgsdi  27252  lgsne0  27253  nolesgn2o  27590  nogesgn1o  27592  nosep1o  27600  nosep2o  27601  nosepssdm  27605  nosupres  27626  nosupbnd1lem1  27627  nosupbnd1lem4  27630  nosupbnd1lem5  27631  nosupbnd1lem6  27632  noinfres  27641  noinfbnd1lem1  27642  noinfbnd1lem4  27645  noinfbnd1lem6  27647  noinfbnd2  27650  noetasuplem3  27654  noetainflem3  27658  slelss  27827  cofsslt  27833  coinitsslt  27834  cofcutrtime  27842  addsass  27919  addsdi  28065  mulsass  28076  sltmul2  28081  divsmulw  28103  brbtwn2  28839  colinearalglem1  28840  colinearalg  28844  axcgrtr  28849  axsegconlem8  28858  axsegconlem9  28859  axsegconlem10  28860  axcontlem2  28899  axcontlem10  28907  elntg2  28919  ewlkle  29540  crctcshwlkn0lem5  29751  wwlknp  29780  wwlksnext  29830  wwlksnextproplem1  29846  wspthsnwspthsnon  29853  clwlkclwwlklem3  29937  erclwwlksym  29957  erclwwlknsym  30006  upgriseupth  30143  eucrct2eupth  30181  3cyclfrgrrn  30222  numclwwlk2lem1lem  30278  numclwwlk1lem2foa  30290  frgrregord13  30332  nvmul0or  30586  ipval2lem2  30640  lnoadd  30694  lnosub  30695  lnomul  30696  shless  31295  shlej1  31296  kbmul  31891  homco2  31913  kbass2  32053  eliccelico  32707  elicoelioo  32708  iocinioc2  32709  iocinif  32711  difioo  32712  nexple  32776  swrdrn2  32883  swrdrn3  32884  xrge0adddir  32966  xrge0npcan  32968  isarchi2  33146  archiabl  33159  pidlnz  33354  lindssn  33356  ssmxidl  33452  pstmfval  33893  fmcncfil  33928  zrhnm  33964  qqhnm  33987  volfiniune  34227  dya2iocnrect  34279  probinc  34419  cndprob01  34433  signswmnd  34555  bnj517  34882  cvmsss2  35268  cvmlift2lem10  35306  br6  35751  funsseq  35762  cgrtriv  35997  5segofs  36001  btwnouttr2  36017  btwnxfr  36051  lineext  36071  btwnconn1lem13  36094  brsegle2  36104  nn0prpwlem  36317  weiunpo  36460  weiunso  36461  weiunfr  36462  weiunse  36463  lindsenlbs  37616  blbnd  37788  ismtyima  37804  rrndstprj2  37832  ghomdiv  37893  grpokerinj  37894  lsatfixedN  39009  lssat  39016  lshpkrlem4  39113  cvrcon3b  39277  atlen0  39310  atcvreq0  39314  atnle  39317  atlatmstc  39319  atlatle  39320  cvlcvr1  39339  hlsupr2  39388  hlrelat2  39404  cvrexchlem  39420  lnnat  39428  atcvrj2b  39433  3dimlem3  39462  3dim1  39468  1cvrjat  39476  llni  39509  llni2  39513  llnexatN  39522  2llnmat  39525  lplni  39533  2atnelpln  39545  llncvrlpln2  39558  2llnmj  39561  lplnexatN  39564  lplnexllnN  39565  2llnm3N  39570  lvoli  39576  lvoli3  39578  lvolnle3at  39583  islvol2aN  39593  4atlem4a  39600  4atlem4b  39601  4atlem11  39610  lplncvrlvol2  39616  2lplnmj  39623  islinei  39741  linepmap  39776  lnjatN  39781  lncvrat  39783  lncmp  39784  elpaddn0  39801  elpaddatriN  39804  elpaddat  39805  paddcom  39814  paddss2  39819  paddss12  39820  paddasslem4  39824  paddasslem9  39829  paddasslem10  39830  pmodl42N  39852  pmapjoin  39853  llnmod1i2  39861  polcon2bN  39921  pclfinclN  39951  poml4N  39954  poml6N  39956  osumcllem1N  39957  osumcllem2N  39958  osumcllem11N  39967  osumclN  39968  pmapojoinN  39969  pexmidlem2N  39972  pexmidlem3N  39973  pexmidlem4N  39974  pexmidlem6N  39976  pexmidlem7N  39977  pl42lem2N  39981  pl42lem3N  39982  pl42lem4N  39983  pl42N  39984  lhprelat3N  40041  4atex  40077  lauteq  40096  lautco  40098  ltrncoidN  40129  ltrneq2  40149  ltrnideq  40176  trlnle  40187  trlval3  40188  cdlemc  40198  cdlemd9  40207  cdlemd  40208  cdleme21j  40337  cdleme21  40338  cdleme29ex  40375  cdlemefr27cl  40404  cdlemefs27cl  40414  cdleme32d  40445  cdleme32f  40447  cdleme35h2  40458  cdleme40m  40468  cdleme17d3  40497  cdleme48fvg  40501  cdlemeg46fvcl  40507  cdlemeg46fgN  40535  cdleme48fgv  40539  cdleme50trn3  40554  cdlemb3  40607  cdlemg8  40632  cdlemg11a  40638  cdlemg15a  40656  cdlemg15  40657  cdlemg16  40658  cdlemg16z  40660  cdlemg17dN  40664  cdlemg24  40689  cdlemg37  40690  cdlemg29  40706  cdlemg33b  40708  cdlemg38  40716  cdlemg40  40718  trlco  40728  cdlemg44b  40733  ltrncom  40739  trljco  40741  tendococl  40773  tendoplcl  40782  tendoplcom  40783  cdlemj2  40823  tendoid0  40826  tendo1ne0  40829  cdlemk25-3  40905  cdlemk36  40914  cdlemkid4  40935  cdlemk19x  40944  cdlemk53  40958  cdlemk56  40972  cdleml5N  40981  tendospcanN  41024  cdlemm10N  41119  dihord6apre  41257  dihord  41265  dihmeetlem1N  41291  dihglblem2N  41295  dihmeetlem2N  41300  dihmeetbN  41304  dihmeetlem5  41309  dihmeetlem6  41310  dihmeetlem7N  41311  dihmeetlem10N  41317  dihmeetlem12N  41319  dihmeetlem16N  41323  dihmeetlem17N  41324  dihmeetlem18N  41325  dihmeetALTN  41328  dihlspsnssN  41333  dvh3dim2  41449  dvh3dim3N  41450  lcfrlem16  41559  mapdrvallem2  41646  mapdh8ad  41780  hgmapvvlem3  41926  sticksstones1  42141  sticksstones2  42142  aks6d1c6isolem1  42169  resubcan2  42383  diophrw  42754  eldioph2lem1  42755  diophrex  42770  rencldnfi  42816  pellexlem2  42825  pellqrexplicit  42872  infmrgelbi  42873  pellfundglb  42880  pellfund14gap  42882  rmxycomplete  42913  congadd  42962  acongeq  42979  jm2.19  42989  jm2.23  42992  jm2.20nn  42993  jm2.27  43004  jm3.1  43016  lnmepi  43081  lmhmlnmsplit  43083  hbtlem2  43120  dgraa0p  43145  proot1hash  43191  iocunico  43207  iocinico  43208  oasubex  43282  cantnf2  43321  onmcl  43327  omcl2  43329  nadd2rabex  43382  nadd1rabtr  43384  nadd1rabex  43386  fzunt  43451  relexpxpmin  43713  ntrclsk3  44066  grur1cld  44228  ismnu  44257  grumnudlem  44281  ismnushort  44297  rfcnnnub  45037  uzwo4  45054  wessf1ornlem  45186  supxrge  45341  infleinflem2  45374  iccintsng  45528  climsuse  45613  lptre2pt  45645  limcleqr  45649  0ellimcdiv  45654  fnlimfvre  45679  dvnprodlem1  45951  volioc  45977  stoweidlem17  46022  stoweidlem19  46024  stoweidlem20  46025  stoweidlem22  46027  stoweidlem28  46033  stoweidlem34  46039  stoweidlem44  46049  stoweidlem60  46065  wallispilem3  46072  fourierdlem42  46154  fourierdlem48  46159  fourierdlem51  46162  fourierdlem54  46165  fourierdlem74  46185  fourierdlem77  46188  fourierdlem87  46198  fourierdlem97  46208  ioorrnopnlem  46309  ovnsubaddlem2  46576  smfinflem  46822  fsupdm  46847  finfdm  46851  eluzge0nn0  47317  fzopredsuc  47328  imasetpreimafvbijlemfv  47407  lighneallem4  47615  oexpnegALTV  47682  oexpnegnz  47683  tgblthelfgott  47820  clnbgrgrim  47938  isubgr3stgrlem3  47971  rmsupp0  48360  rmsuppss  48362  lincresunit3lem3  48467  lincresunit3lem2  48473  lindssnlvec  48479  fdivmptf  48534  refdivmptf  48535  elbigolo1  48550  rrx2linest  48735  itsclc0lem1  48749  itsclc0lem2  48750  itsclc0yqsollem1  48755  itsclc0b  48765  setc1onsubc  49595