Theorem simpl2 1188

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpl12  1245  simpl22  1248  simpl32  1251  simp1l2  1263  simp2l2  1269  simp3l2  1275  3anandirs  1468  rspc3ev  3637  2nreu  4393  f1prex  7040  weniso  7107  ofmpteq  7428  tfisi  7573  mposn  7798  smogt  8004  smorndom  8005  omeulem1  8208  nnmord  8258  nnmword  8259  difsnen  8599  enfixsn  8626  mapunen  8686  ac6sfi  8762  ordiso2  8979  wemaplem2  9011  wemapso  9015  wemapso2lem  9016  en2eqpr  9433  acndom  9477  infmap2  9640  cflim2  9685  cfsmolem  9692  coftr  9695  fin23lem26  9747  isf32lem9  9783  fin1a2lem9  9830  fin1a2lem10  9831  gchdomtri  10051  canth4  10069  gchpwdom  10092  gruima  10224  grudomon  10239  prn0  10411  distrlem4pr  10448  prlem934  10455  addcan  10824  addcan2  10825  divmulass  11321  divmulasscom  11322  ltmul1a  11489  supmul1  11610  uzsupss  12341  xaddass  12643  xleadd1a  12647  xlesubadd  12657  xmulass  12681  xlemul2a  12683  xadddilem  12688  xadddi  12689  ixxdisj  12754  ixxun  12755  ixxlb  12761  icoshftf1o  12861  icodisj  12863  ioounsn  12864  lincmb01cmp  12882  iccf1o  12883  elfz1b  12977  ssfzoulel  13132  modmuladd  13282  modaddmulmod  13307  ltexp2a  13531  leexp2  13536  ltexp2r  13538  exple1  13541  expnlbnd2  13596  mulsubdivbinom2  13623  fun2dmnop0  13853  ccatass  13942  ccatopth  14078  pfxccatin12lem2a  14089  repswpfx  14147  repswccat  14148  cshwidxmodr  14166  2cshw  14175  repsco  14202  s2f1o  14278  limsupgle  14834  limsupgre  14838  addcn2  14950  mulcn2  14952  binomrisefac  15396  dvdsval2  15610  dvdsadd2b  15656  dvdsmod  15678  oexpneg  15694  sadass  15820  gcdass  15895  rplpwr  15907  rppwr  15908  lcmass  15958  coprmdvds2  15998  rpmulgcd2  16000  rpdvds  16004  coprmprod  16005  cncongr2  16012  rpexp  16064  prmdiveq  16123  hashgcdlem  16125  odzdvds  16132  coprimeprodsq2  16146  pythagtriplem3  16155  pythagtriplem4  16156  pcdvdsb  16205  vdwnnlem1  16331  0ram  16356  ramz2  16360  ramub1lem1  16362  mremre  16875  mrieqv2d  16910  lubss  17731  lubun  17733  clatleglb  17736  clatglbss  17737  mrelatglb  17794  isnsgrp  17905  issubmnd  17938  gsumccatOLD  18005  gsumccat  18006  frmdss2  18028  submefmnd  18060  nmzsubg  18317  ghmnsgima  18382  gsmsymgreqlem1  18558  psgnunilem4  18625  odmodnn0  18668  odnncl  18673  odmod  18674  oddvds  18675  odeq  18678  odmulgid  18681  odmulgeq  18684  odbezout  18685  odf1o1  18697  odf1o2  18698  odngen  18702  gexdvdsi  18708  pgpfi1  18720  odcau  18729  subgslw  18741  fislw  18750  lsmless1x  18769  lsmless2x  18770  lsmsubm  18778  lsmmod  18801  lsmmod2  18802  efgsfo  18865  odadd1  18968  odadd2  18969  odadd  18970  lsmcomx  18976  prdscmnd  18981  gsumconst  19054  ablsimpgfindlem1  19229  srg1zr  19279  csrgbinom  19296  ring1eq0  19340  mulgass2  19351  cntzsubr  19568  isabvd  19591  rmodislmod  19702  0lmhm  19812  lmhmvsca  19817  reslmhm2b  19826  pwssplit1  19831  pwssplit2  19832  pwssplit3  19833  lbspss  19854  lspsnat  19917  lidldvgen  20028  issubassa  20098  evlsval2  20300  coe1subfv  20434  coe1sclmul  20450  coe1sclmul2  20452  xrsdsreclblem  20591  cssmre  20837  obs2ss  20873  uvcresum  20937  frlmsslsp  20940  frlmup4  20945  lindff1  20964  f1lindf  20966  lsslindf  20974  islindf4  20982  mpomatmul  21055  mamutpos  21067  scmatscmide  21116  mavmulsolcl  21160  mulmarep1gsum2  21183  mdetdiaglem  21207  mdetdiag  21208  mdetunilem1  21221  mdetunilem3  21223  mdetunilem9  21229  maducoeval2  21249  madurid  21253  slesolinvbi  21290  cramerimplem1  21292  cramerlem1  21296  cramer  21300  cpmatel2  21321  m2cpm  21349  m2pmfzmap  21355  m2cpminvid2lem  21362  m2cpminvid2  21363  decpmatmul  21380  pmatcollpw1lem2  21383  pmatcollpw1  21384  pmatcollpw2lem  21385  pmatcollpwfi  21390  pm2mpcl  21405  mply1topmatcl  21413  mp2pm2mplem2  21415  mp2pm2mplem4  21417  mp2pm2mplem5  21418  mp2pm2mp  21419  pm2mpghmlem2  21420  pm2mpghmlem1  21421  chfacfisfcpmat  21463  topssnei  21732  cnconst2  21891  cnpresti  21896  cnprest2  21898  cnpdis  21901  cnt0  21954  cnt1  21958  cnhaus  21962  sscmp  22013  hauscmp  22015  cnconn  22030  unconn  22037  finlocfin  22128  comppfsc  22140  kgen2ss  22163  ptpjopn  22220  prdstopn  22236  ptrescn  22247  qtopss  22323  kqfvima  22338  fbssint  22446  fbasrn  22492  filuni  22493  fmss  22554  rnelfm  22561  fmufil  22567  fmco  22569  flimss2  22580  flimss1  22581  flimrest  22591  cnpflf2  22608  flfcnp  22612  supnfcls  22628  fclsss1  22630  fclsss2  22631  isfcf  22642  subgntr  22715  opnsubg  22716  cldsubg  22719  ghmcnp  22723  ustuqtop1  22850  bldisj  23008  blgt0  23009  bl2in  23010  blss2ps  23013  blss2  23014  blssps  23034  blss  23035  xmetresbl  23047  lpbl  23113  blcld  23115  stdbdmopn  23128  metcnp3  23150  metcnp  23151  metcnp2  23152  txmetcnp  23157  blval2  23172  nmoix  23338  nmoi2  23339  nmotri  23348  metdsge  23457  metdseq0  23462  iocopnst  23544  xrhmeo  23550  nmhmcn  23724  cphsqrtcl2  23790  cphsqrtcl3  23791  cssbn  23978  pjth  24042  ovoliunlem2  24104  volun  24146  mbfimaopn2  24258  iblconst  24418  limcvallem  24469  dvfval  24495  dvcnp2  24517  dvcn  24518  deg1mul3le  24710  deg1tmle  24711  dvdsq1p  24754  ig1peu  24765  ig1pdvds  24770  ply1term  24794  coeid3  24830  dgrmulc  24861  dvply1  24873  aaliou2  24929  efcvx  25037  tanord  25122  eflogeq  25185  logdivlti  25203  logccv  25246  recxpcl  25258  cxplea  25279  cxpeq  25338  ang180  25392  isosctrlem2  25397  cxp2lim  25554  amgm  25568  muval1  25710  dvdssqf  25715  mumullem2  25757  mumul  25758  bcmono  25853  lgsneg  25897  lgsdilem  25900  lgsdirprm  25907  lgsdir  25908  lgsdi  25910  lgsne0  25911  brbtwn2  26691  colinearalglem1  26692  colinearalg  26696  axcgrtr  26701  axsegconlem8  26710  axsegconlem9  26711  axsegconlem10  26712  axcontlem2  26751  axcontlem10  26759  elntg2  26771  ewlkle  27387  crctcshwlkn0lem5  27592  wwlknp  27621  wwlksnext  27671  wwlksnextproplem1  27688  wspthsnwspthsnon  27695  clwlkclwwlklem3  27779  erclwwlksym  27799  erclwwlknsym  27849  upgriseupth  27986  eucrct2eupth  28024  3cyclfrgrrn  28065  numclwwlk2lem1lem  28121  numclwwlk1lem2foa  28133  frgrregord13  28175  nvmul0or  28427  ipval2lem2  28481  lnoadd  28535  lnosub  28536  lnomul  28537  shless  29136  shlej1  29137  kbmul  29732  homco2  29754  kbass2  29894  eliccelico  30500  elicoelioo  30501  iocinioc2  30502  iocinif  30504  difioo  30505  swrdrn2  30628  swrdrn3  30629  xrge0adddir  30679  xrge0npcan  30681  isarchi2  30814  archiabl  30827  rhmdvdsr  30891  lindssn  30939  ssmxidl  30979  pstmfval  31136  fmcncfil  31174  zrhnm  31210  qqhnm  31231  nexple  31268  volfiniune  31489  dya2iocnrect  31539  probinc  31679  cndprob01  31693  signswmnd  31827  bnj517  32157  cvmsss2  32521  cvmlift2lem10  32559  br6  32993  funsseq  33011  fprlem1  33137  nolesgn2o  33178  nosep1o  33186  nosepssdm  33190  nosupres  33207  nosupbnd1lem1  33208  nosupbnd1lem4  33211  nosupbnd1lem5  33212  nosupbnd1lem6  33213  noetalem2  33218  cgrtriv  33463  5segofs  33467  btwnouttr2  33483  btwnxfr  33517  lineext  33537  btwnconn1lem13  33560  brsegle2  33570  nn0prpwlem  33670  lindsenlbs  34902  blbnd  35080  ismtyima  35096  rrndstprj2  35124  ghomdiv  35185  grpokerinj  35186  lsatfixedN  36160  lssat  36167  lshpkrlem4  36264  cvrcon3b  36428  atlen0  36461  atcvreq0  36465  atnle  36468  atlatmstc  36470  atlatle  36471  cvlcvr1  36490  hlsupr2  36538  hlrelat2  36554  cvrexchlem  36570  lnnat  36578  atcvrj2b  36583  3dimlem3  36612  3dim1  36618  1cvrjat  36626  llni  36659  llni2  36663  llnexatN  36672  2llnmat  36675  lplni  36683  2atnelpln  36695  llncvrlpln2  36708  2llnmj  36711  lplnexatN  36714  lplnexllnN  36715  2llnm3N  36720  lvoli  36726  lvoli3  36728  lvolnle3at  36733  islvol2aN  36743  4atlem4a  36750  4atlem4b  36751  4atlem11  36760  lplncvrlvol2  36766  2lplnmj  36773  islinei  36891  linepmap  36926  lnjatN  36931  lncvrat  36933  lncmp  36934  elpaddn0  36951  elpaddatriN  36954  elpaddat  36955  paddcom  36964  paddss2  36969  paddss12  36970  paddasslem4  36974  paddasslem9  36979  paddasslem10  36980  pmodl42N  37002  pmapjoin  37003  llnmod1i2  37011  polcon2bN  37071  pclfinclN  37101  poml4N  37104  poml6N  37106  osumcllem1N  37107  osumcllem2N  37108  osumcllem11N  37117  osumclN  37118  pmapojoinN  37119  pexmidlem2N  37122  pexmidlem3N  37123  pexmidlem4N  37124  pexmidlem6N  37126  pexmidlem7N  37127  pl42lem2N  37131  pl42lem3N  37132  pl42lem4N  37133  pl42N  37134  lhprelat3N  37191  4atex  37227  lauteq  37246  lautco  37248  ltrncoidN  37279  ltrneq2  37299  ltrnideq  37326  trlnle  37337  trlval3  37338  cdlemc  37348  cdlemd9  37357  cdlemd  37358  cdleme21j  37487  cdleme21  37488  cdleme29ex  37525  cdlemefr27cl  37554  cdlemefs27cl  37564  cdleme32d  37595  cdleme32f  37597  cdleme35h2  37608  cdleme40m  37618  cdleme17d3  37647  cdleme48fvg  37651  cdlemeg46fvcl  37657  cdlemeg46fgN  37685  cdleme48fgv  37689  cdleme50trn3  37704  cdlemb3  37757  cdlemg8  37782  cdlemg11a  37788  cdlemg15a  37806  cdlemg15  37807  cdlemg16  37808  cdlemg16z  37810  cdlemg17dN  37814  cdlemg24  37839  cdlemg37  37840  cdlemg29  37856  cdlemg33b  37858  cdlemg38  37866  cdlemg40  37868  trlco  37878  cdlemg44b  37883  ltrncom  37889  trljco  37891  tendococl  37923  tendoplcl  37932  tendoplcom  37933  cdlemj2  37973  tendoid0  37976  tendo1ne0  37979  cdlemk25-3  38055  cdlemk36  38064  cdlemkid4  38085  cdlemk19x  38094  cdlemk53  38108  cdlemk56  38122  cdleml5N  38131  tendospcanN  38174  cdlemm10N  38269  dihord6apre  38407  dihord  38415  dihmeetlem1N  38441  dihglblem2N  38445  dihmeetlem2N  38450  dihmeetbN  38454  dihmeetlem5  38459  dihmeetlem6  38460  dihmeetlem7N  38461  dihmeetlem10N  38467  dihmeetlem12N  38469  dihmeetlem16N  38473  dihmeetlem17N  38474  dihmeetlem18N  38475  dihmeetALTN  38478  dihlspsnssN  38483  dvh3dim2  38599  dvh3dim3N  38600  lcfrlem16  38709  mapdrvallem2  38796  mapdh8ad  38930  hgmapvvlem3  39076  resubcan2  39267  diophrw  39405  eldioph2lem1  39406  diophrex  39421  rencldnfi  39467  pellexlem2  39476  pellqrexplicit  39523  infmrgelbi  39524  pellfundglb  39531  pellfund14gap  39533  rmxycomplete  39563  congadd  39612  acongeq  39629  jm2.19  39639  jm2.23  39642  jm2.20nn  39643  jm2.27  39654  jm3.1  39666  lnmepi  39734  lmhmlnmsplit  39736  hbtlem2  39773  dgraa0p  39798  idomrootle  39844  proot1hash  39849  iocunico  39866  iocinico  39867  relexpxpmin  40111  ntrclsk3  40469  grur1cld  40617  ismnu  40646  grumnudlem  40670  rfcnnnub  41342  uzwo4  41364  wessf1ornlem  41494  supxrge  41655  infleinflem2  41688  iccintsng  41848  climsuse  41938  lptre2pt  41970  limcleqr  41974  0ellimcdiv  41979  fnlimfvre  42004  dvnprodlem1  42280  volioc  42306  stoweidlem17  42351  stoweidlem19  42353  stoweidlem20  42354  stoweidlem22  42356  stoweidlem28  42362  stoweidlem34  42368  stoweidlem44  42378  stoweidlem60  42394  wallispilem3  42401  fourierdlem42  42483  fourierdlem48  42488  fourierdlem51  42491  fourierdlem54  42494  fourierdlem74  42514  fourierdlem77  42517  fourierdlem87  42527  fourierdlem97  42537  ioorrnopnlem  42638  ovnsubaddlem2  42902  smfinflem  43140  eluzge0nn0  43561  fzopredsuc  43572  fzoopth  43576  imasetpreimafvbijlemfv  43611  lighneallem4  43824  oexpnegALTV  43891  oexpnegnz  43892  tgblthelfgott  44029  rmsupp0  44465  rmsuppss  44467  lincresunit3lem3  44578  lincresunit3lem2  44584  lindssnlvec  44590  fdivmptf  44650  refdivmptf  44651  elbigolo1  44666  rrx2linest  44778  itsclc0lem1  44792  itsclc0lem2  44793  itsclc0yqsollem1  44798  itsclc0b  44808