Theorem simpl2 1209

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 487	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2	1	3ad2antl2 1203	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simpl12  1266  simpl22  1269  simpl32  1272  simp1l2  1284  simp2l2  1290  simp3l2  1296  3anandirs  1499  rspc3ev  3597  2nreu  4408  f1prex  7282  weniso  7352  ofmpteq  7697  tfisi  7854  mposn  8097  fprlem1  8296  smogt  8353  smocdmdom  8354  omeulem1  8566  nnmord  8617  nnmword  8618  naddasslem1  8680  naddasslem2  8681  difsnen  9046  enfixsn  9073  mapunen  9133  ac6sfi  9243  ordiso2  9476  wemaplem2  9508  wemapso2lem  9513  en2eqpr  9990  acndom  10034  infmap2  10199  cflim2  10246  cfsmolem  10253  coftr  10256  fin23lem26  10308  isf32lem9  10344  fin1a2lem9  10391  fin1a2lem10  10392  gchdomtri  10613  canth4  10631  gchpwdom  10654  gruima  10786  grudomon  10801  prn0  10973  distrlem4pr  11010  prlem934  11017  addcan  11393  addcan2  11394  divmulass  11894  divmulasscom  11895  ltmul1a  12063  supmul1  12183  uzsupss  12963  xaddass  13274  xleadd1a  13278  xlesubadd  13288  xmulass  13312  xlemul2a  13314  xadddilem  13319  xadddi  13320  ixxdisj  13386  ixxun  13387  ixxlb  13393  icoshftf1o  13500  icodisj  13502  ioounsn  13503  lincmb01cmp  13521  iccf1o  13522  elfz1b  13621  ssfzoulel  13789  fzoopth  13791  modmuladd  13949  modaddmulmod  13974  ltexp2a  14202  leexp2  14207  ltexp2r  14209  exple1  14213  expnlbnd2  14270  mulsubdivbinom2  14298  fun2dmnop0  14541  ccatass  14626  ccatopth  14753  pfxccatin12lem2a  14764  repswpfx  14822  repswccat  14823  cshwidxmodr  14841  2cshw  14850  repsco  14877  s2f1o  14953  limsupgle  15528  limsupgre  15532  addcn2  15645  mulcn2  15647  binomrisefac  16095  dvdsval2  16312  dvdsadd2b  16363  dvdsmod  16386  oexpneg  16402  sadass  16528  gcdass  16604  rplpwr  16615  lcmass  16671  coprmdvds2  16711  rpmulgcd2  16713  rpdvds  16717  coprmprod  16718  cncongr2  16725  rpexp  16780  prmdiveq  16844  hashgcdlem  16846  odzdvds  16854  coprimeprodsq2  16868  pythagtriplem3  16877  pythagtriplem4  16878  pcdvdsb  16928  vdwnnlem1  17054  0ram  17079  ramz2  17083  ramub1lem1  17085  mremre  17655  mrieqv2d  17694  lubss  18568  lubun  18570  clatleglb  18573  clatglbss  18574  mrelatglb  18615  isnsgrp  18780  issubmnd  18818  gsumccat  18899  frmdss2  18921  submefmnd  18953  nmzsubg  19230  ghmnsgima  19309  gsmsymgreqlem1  19499  psgnunilem4  19566  odmodnn0  19609  odnncl  19614  odmod  19615  oddvds  19616  odeq  19619  odmulgid  19623  odmulgeq  19626  odbezout  19627  odf1o1  19641  odf1o2  19642  odngen  19646  gexdvdsi  19652  pgpfi1  19664  odcau  19673  subgslw  19685  fislw  19694  lsmless1x  19713  lsmless2x  19714  lsmsubm  19722  lsmmod  19744  lsmmod2  19745  efgsfo  19808  odadd1  19917  odadd2  19918  odadd  19919  lsmcomx  19925  prdscmnd  19930  gsumconst  20003  ablsimpgfindlem1  20178  csrgbinom  20313  ring1eq0  20380  mulgass2  20391  rngisom1  20547  rhmdvdsr  20590  cntzsubrng  20651  cntzsubr  20690  isabvd  20894  rmodislmod  21030  0lmhm  21140  lmhmvsca  21145  reslmhm2b  21154  pwssplit1  21159  pwssplit2  21160  pwssplit3  21161  lbspss  21182  lspsnat  21248  pidlnz  21353  lidldvgen  21481  xrsdsreclblem  21542  cssmre  21822  obs2ss  21858  uvcresum  21922  frlmsslsp  21925  frlmup4  21930  lindff1  21949  f1lindf  21951  lsslindf  21959  islindf4  21967  issubassa  21996  evlsval2  22217  coe1subfv  22406  coe1sclmul  22422  coe1sclmul2  22424  mpomatmul  22582  mamutpos  22594  scmatscmide  22643  mavmulsolcl  22687  mulmarep1gsum2  22710  mdetdiaglem  22734  mdetdiag  22735  mdetunilem1  22748  mdetunilem3  22750  mdetunilem9  22756  maducoeval2  22776  madurid  22780  slesolinvbi  22817  cramerimplem1  22819  cramerlem1  22823  cramer  22827  cpmatel2  22849  m2cpm  22877  m2pmfzmap  22883  m2cpminvid2lem  22890  m2cpminvid2  22891  decpmatmul  22908  pmatcollpw1lem2  22911  pmatcollpw1  22912  pmatcollpw2lem  22913  pmatcollpwfi  22918  pm2mpcl  22933  mply1topmatcl  22941  mp2pm2mplem2  22943  mp2pm2mplem4  22945  mp2pm2mplem5  22946  mp2pm2mp  22947  pm2mpghmlem2  22948  pm2mpghmlem1  22949  chfacfisfcpmat  22991  topssnei  23260  cnconst2  23419  cnpresti  23424  cnprest2  23426  cnpdis  23429  cnt0  23482  cnt1  23486  cnhaus  23490  sscmp  23541  hauscmp  23543  cnconn  23558  unconn  23565  finlocfin  23656  comppfsc  23668  kgen2ss  23691  ptpjopn  23748  prdstopn  23764  ptrescn  23775  qtopss  23851  kqfvima  23866  fbssint  23974  fbasrn  24020  filuni  24021  fmss  24082  rnelfm  24089  fmufil  24095  fmco  24097  flimss2  24108  flimss1  24109  flimrest  24119  cnpflf2  24136  flfcnp  24140  supnfcls  24156  fclsss1  24158  fclsss2  24159  isfcf  24170  subgntr  24243  opnsubg  24244  cldsubg  24247  ghmcnp  24251  ustuqtop1  24377  bldisj  24534  blgt0  24535  bl2in  24536  blss2ps  24539  blss2  24540  blssps  24560  blss  24561  xmetresbl  24573  lpbl  24639  blcld  24641  stdbdmopn  24654  metcnp3  24676  metcnp  24677  metcnp2  24678  txmetcnp  24683  blval2  24698  nmoix  24865  nmoi2  24866  nmotri  24875  metdsge  24986  metdseq0  24991  iocopnst  25078  xrhmeo  25084  nmhmcn  25258  cphsqrtcl2  25324  cphsqrtcl3  25325  cssbn  25513  pjth  25577  ovoliunlem2  25641  volun  25683  mbfimaopn2  25795  iblconst  25956  limcvallem  26009  dvfval  26035  dvcnp2  26058  dvcn  26059  deg1mul3le  26253  deg1tmle  26254  dvdsq1p  26299  idomrootle  26309  ig1peu  26311  ig1pdvds  26316  ply1term  26340  coeid3  26376  dgrmulc  26407  dvply1  26424  aaliou2  26480  efcvx  26588  tanord  26679  eflogeq  26743  logdivlti  26761  logccv  26804  recxpcl  26816  cxplea  26837  cxpeq  26898  ang180  26955  isosctrlem2  26960  cxp2lim  27117  amgm  27131  muval1  27273  dvdssqf  27278  mumullem2  27320  mumul  27321  bcmono  27417  lgsneg  27461  lgsdilem  27464  lgsdirprm  27471  lgsdir  27472  lgsdi  27474  lgsne0  27475  nolesgn2o  27811  nogesgn1o  27813  nosep1o  27821  nosep2o  27822  nosepssdm  27826  nosupres  27847  nosupbnd1lem1  27848  nosupbnd1lem4  27851  nosupbnd1lem5  27852  nosupbnd1lem6  27853  noinfres  27862  noinfbnd1lem1  27863  noinfbnd1lem4  27866  noinfbnd1lem6  27868  noinfbnd2  27871  noetasuplem3  27875  noetainflem3  27879  leslss  28078  cofslts  28087  coinitslts  28088  cofcutrtime  28096  addsass  28174  addsdi  28324  mulsass  28335  ltmuls2  28340  divmulsw  28362  bdayfinbndlem1  28636  z12bdaylem  28653  brbtwn2  29221  colinearalglem1  29222  colinearalg  29226  axcgrtr  29231  axsegconlem8  29240  axsegconlem9  29241  axsegconlem10  29242  axcontlem2  29281  axcontlem10  29289  elntg2  29301  ewlkle  29921  crctcshwlkn0lem5  30129  wwlknp  30158  wwlksnext  30208  wwlksnextproplem1  30224  wspthsnwspthsnon  30231  clwlkclwwlklem3  30318  erclwwlksym  30338  erclwwlknsym  30387  upgriseupth  30524  eucrct2eupth  30562  3cyclfrgrrn  30603  numclwwlk2lem1lem  30659  numclwwlk1lem2foa  30671  frgrregord13  30713  nvmul0or  30968  ipval2lem2  31022  lnoadd  31076  lnosub  31077  lnomul  31078  shless  31677  shlej1  31678  kbmul  32273  homco2  32295  kbass2  32435  eliccelico  33088  elicoelioo  33089  iocinioc2  33090  iocinif  33092  difioo  33093  nexple  33143  swrdrn2  33240  swrdrn3  33241  xrge0adddir  33304  xrge0npcan  33306  isarchi2  33471  archiabl  33484  lindssn  33657  ssmxidl  33723  pstmfval  34252  fmcncfil  34287  zrhnm  34323  qqhnm  34346  volfiniune  34586  dya2iocnrect  34637  probinc  34777  cndprob01  34791  signswmnd  34910  bnj517  35239  cvmsss2  35732  cvmlift2lem10  35770  br6  36215  funsseq  36226  cgrtriv  36460  5segofs  36464  btwnouttr2  36480  btwnxfr  36514  lineext  36534  btwnconn1lem13  36557  brsegle2  36567  nmulss1  36657  ltnmul  36659  nmulle  36660  ltnadd  36661  naddle  36662  nn0prpwlem  36799  weiunpo  36942  weiunso  36943  weiunfr  36944  weiunse  36945  axtcond  36955  lindsenlbs  38232  blbnd  38404  ismtyima  38420  rrndstprj2  38448  ghomdiv  38509  grpokerinj  38510  lsatfixedN  39751  lssat  39758  lshpkrlem4  39855  cvrcon3b  40019  atlen0  40052  atcvreq0  40056  atnle  40059  atlatmstc  40061  atlatle  40062  cvlcvr1  40081  hlsupr2  40129  hlrelat2  40145  cvrexchlem  40161  lnnat  40169  atcvrj2b  40174  3dimlem3  40203  3dim1  40209  1cvrjat  40217  llni  40250  llni2  40254  llnexatN  40263  2llnmat  40266  lplni  40274  2atnelpln  40286  llncvrlpln2  40299  2llnmj  40302  lplnexatN  40305  lplnexllnN  40306  2llnm3N  40311  lvoli  40317  lvoli3  40319  lvolnle3at  40324  islvol2aN  40334  4atlem4a  40341  4atlem4b  40342  4atlem11  40351  lplncvrlvol2  40357  2lplnmj  40364  islinei  40482  linepmap  40517  lnjatN  40522  lncvrat  40524  lncmp  40525  elpaddn0  40542  elpaddatriN  40545  elpaddat  40546  paddcom  40555  paddss2  40560  paddss12  40561  paddasslem4  40565  paddasslem9  40570  paddasslem10  40571  pmodl42N  40593  pmapjoin  40594  llnmod1i2  40602  polcon2bN  40662  pclfinclN  40692  poml4N  40695  poml6N  40697  osumcllem1N  40698  osumcllem2N  40699  osumcllem11N  40708  osumclN  40709  pmapojoinN  40710  pexmidlem2N  40713  pexmidlem3N  40714  pexmidlem4N  40715  pexmidlem6N  40717  pexmidlem7N  40718  pl42lem2N  40722  pl42lem3N  40723  pl42lem4N  40724  pl42N  40725  lhprelat3N  40782  4atex  40818  lauteq  40837  lautco  40839  ltrncoidN  40870  ltrneq2  40890  ltrnideq  40917  trlnle  40928  trlval3  40929  cdlemc  40939  cdlemd9  40948  cdlemd  40949  cdleme21j  41078  cdleme21  41079  cdleme29ex  41116  cdlemefr27cl  41145  cdlemefs27cl  41155  cdleme32d  41186  cdleme32f  41188  cdleme35h2  41199  cdleme40m  41209  cdleme17d3  41238  cdleme48fvg  41242  cdlemeg46fvcl  41248  cdlemeg46fgN  41276  cdleme48fgv  41280  cdleme50trn3  41295  cdlemb3  41348  cdlemg8  41373  cdlemg11a  41379  cdlemg15a  41397  cdlemg15  41398  cdlemg16  41399  cdlemg16z  41401  cdlemg17dN  41405  cdlemg24  41430  cdlemg37  41431  cdlemg29  41447  cdlemg33b  41449  cdlemg38  41457  cdlemg40  41459  trlco  41469  cdlemg44b  41474  ltrncom  41480  trljco  41482  tendococl  41514  tendoplcl  41523  tendoplcom  41524  cdlemj2  41564  tendoid0  41567  tendo1ne0  41570  cdlemk25-3  41646  cdlemk36  41655  cdlemkid4  41676  cdlemk19x  41685  cdlemk53  41699  cdlemk56  41713  cdleml5N  41722  tendospcanN  41765  cdlemm10N  41860  dihord6apre  41998  dihord  42006  dihmeetlem1N  42032  dihglblem2N  42036  dihmeetlem2N  42041  dihmeetbN  42045  dihmeetlem5  42050  dihmeetlem6  42051  dihmeetlem7N  42052  dihmeetlem10N  42058  dihmeetlem12N  42060  dihmeetlem16N  42064  dihmeetlem17N  42065  dihmeetlem18N  42066  dihmeetALTN  42069  dihlspsnssN  42074  dvh3dim2  42190  dvh3dim3N  42191  lcfrlem16  42300  mapdrvallem2  42387  mapdh8ad  42521  hgmapvvlem3  42667  sticksstones1  42881  sticksstones2  42882  aks6d1c6isolem1  42909  resubcan2  43117  diophrw  43460  eldioph2lem1  43461  diophrex  43476  rencldnfi  43518  pellexlem2  43527  pellqrexplicit  43574  infmrgelbi  43575  pellfundglb  43582  pellfund14gap  43584  rmxycomplete  43614  congadd  43663  acongeq  43680  jm2.19  43690  jm2.23  43693  jm2.20nn  43694  jm2.27  43705  jm3.1  43717  lnmepi  43782  lmhmlnmsplit  43784  hbtlem2  43821  dgraa0p  43846  proot1hash  43892  iocunico  43908  iocinico  43909  oasubex  43983  cantnf2  44022  onmcl  44028  omcl2  44030  nadd2rabex  44083  nadd1rabtr  44085  nadd1rabex  44087  fzunt  44151  relexpxpmin  44413  ntrclsk3  44766  grur1cld  44926  ismnu  44941  grumnudlem  44965  ismnushort  44981  rfcnnnub  45726  uzwo4  45743  wessf1ornlem  45873  supxrge  46024  infleinflem2  46056  iccintsng  46209  climsuse  46294  lptre2pt  46324  limcleqr  46328  0ellimcdiv  46333  fnlimfvre  46358  dvnprodlem1  46630  volioc  46656  stoweidlem17  46701  stoweidlem19  46703  stoweidlem20  46704  stoweidlem22  46706  stoweidlem28  46712  stoweidlem34  46718  stoweidlem44  46728  stoweidlem60  46744  wallispilem3  46751  fourierdlem42  46833  fourierdlem48  46838  fourierdlem51  46841  fourierdlem54  46844  fourierdlem74  46864  fourierdlem77  46867  fourierdlem87  46877  fourierdlem97  46887  ioorrnopnlem  46988  ovnsubaddlem2  47255  smfinflem  47501  fsupdm  47526  finfdm  47530  eluzge0nn0  48016  fzopredsuc  48028  imasetpreimafvbijlemfv  48118  lighneallem4  48329  oexpnegALTV  48409  oexpnegnz  48410  tgblthelfgott  48547  clnbgrgrim  48666  isubgr3stgrlem3  48700  rmsupp0  49115  rmsuppss  49117  lincresunit3lem3  49221  lincresunit3lem2  49227  lindssnlvec  49233  fdivmptf  49288  refdivmptf  49289  elbigolo1  49304  rrx2linest  49489  itsclc0lem1  49503  itsclc0lem2  49504  itsclc0yqsollem1  49509  itsclc0b  49519  setc1onsubc  50347