Theorem simpl2 1191

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simpl12  1248  simpl22  1251  simpl32  1254  simp1l2  1266  simp2l2  1272  simp3l2  1278  3anandirs  1471  rspc3ev  3575  2nreu  4376  f1prex  7165  weniso  7234  ofmpteq  7564  tfisi  7714  mposn  7952  fprlem1  8125  smogt  8207  smorndom  8208  omeulem1  8422  nnmord  8472  nnmword  8473  difsnen  8849  enfixsn  8877  mapunen  8942  ac6sfi  9067  ordiso2  9283  wemaplem2  9315  wemapso2lem  9320  en2eqpr  9772  acndom  9816  infmap2  9983  cflim2  10028  cfsmolem  10035  coftr  10038  fin23lem26  10090  isf32lem9  10126  fin1a2lem9  10173  fin1a2lem10  10174  gchdomtri  10394  canth4  10412  gchpwdom  10435  gruima  10567  grudomon  10582  prn0  10754  distrlem4pr  10791  prlem934  10798  addcan  11168  addcan2  11169  divmulass  11665  divmulasscom  11666  ltmul1a  11833  supmul1  11953  uzsupss  12689  xaddass  12992  xleadd1a  12996  xlesubadd  13006  xmulass  13030  xlemul2a  13032  xadddilem  13037  xadddi  13038  ixxdisj  13103  ixxun  13104  ixxlb  13110  icoshftf1o  13215  icodisj  13217  ioounsn  13218  lincmb01cmp  13236  iccf1o  13237  elfz1b  13334  ssfzoulel  13490  modmuladd  13642  modaddmulmod  13667  ltexp2a  13893  leexp2  13898  ltexp2r  13900  exple1  13903  expnlbnd2  13958  mulsubdivbinom2  13985  fun2dmnop0  14217  ccatass  14302  ccatopth  14438  pfxccatin12lem2a  14449  repswpfx  14507  repswccat  14508  cshwidxmodr  14526  2cshw  14535  repsco  14562  s2f1o  14638  limsupgle  15195  limsupgre  15199  addcn2  15312  mulcn2  15314  binomrisefac  15761  dvdsval2  15975  dvdsadd2b  16024  dvdsmod  16047  oexpneg  16063  sadass  16187  gcdass  16264  rplpwr  16276  lcmass  16328  coprmdvds2  16368  rpmulgcd2  16370  rpdvds  16374  coprmprod  16375  cncongr2  16382  rpexp  16436  prmdiveq  16496  hashgcdlem  16498  odzdvds  16505  coprimeprodsq2  16519  pythagtriplem3  16528  pythagtriplem4  16529  pcdvdsb  16579  vdwnnlem1  16705  0ram  16730  ramz2  16734  ramub1lem1  16736  mremre  17322  mrieqv2d  17357  lubss  18240  lubun  18242  clatleglb  18245  clatglbss  18246  mrelatglb  18287  isnsgrp  18388  issubmnd  18421  gsumccatOLD  18488  gsumccat  18489  frmdss2  18511  submefmnd  18543  nmzsubg  18802  ghmnsgima  18867  gsmsymgreqlem1  19047  psgnunilem4  19114  odmodnn0  19157  odnncl  19162  odmod  19163  oddvds  19164  odeq  19167  odmulgid  19170  odmulgeq  19173  odbezout  19174  odf1o1  19186  odf1o2  19187  odngen  19191  gexdvdsi  19197  pgpfi1  19209  odcau  19218  subgslw  19230  fislw  19239  lsmless1x  19258  lsmless2x  19259  lsmsubm  19267  lsmmod  19290  lsmmod2  19291  efgsfo  19354  odadd1  19458  odadd2  19459  odadd  19460  lsmcomx  19466  prdscmnd  19471  gsumconst  19544  ablsimpgfindlem1  19719  srg1zr  19774  csrgbinom  19791  ring1eq0  19838  mulgass2  19849  cntzsubr  20066  isabvd  20089  rmodislmod  20200  rmodislmodOLD  20201  0lmhm  20311  lmhmvsca  20316  reslmhm2b  20325  pwssplit1  20330  pwssplit2  20331  pwssplit3  20332  lbspss  20353  lspsnat  20416  lidldvgen  20535  xrsdsreclblem  20653  cssmre  20907  obs2ss  20945  uvcresum  21009  frlmsslsp  21012  frlmup4  21017  lindff1  21036  f1lindf  21038  lsslindf  21046  islindf4  21054  issubassa  21082  evlsval2  21306  coe1subfv  21446  coe1sclmul  21462  coe1sclmul2  21464  mpomatmul  21604  mamutpos  21616  scmatscmide  21665  mavmulsolcl  21709  mulmarep1gsum2  21732  mdetdiaglem  21756  mdetdiag  21757  mdetunilem1  21770  mdetunilem3  21772  mdetunilem9  21778  maducoeval2  21798  madurid  21802  slesolinvbi  21839  cramerimplem1  21841  cramerlem1  21845  cramer  21849  cpmatel2  21871  m2cpm  21899  m2pmfzmap  21905  m2cpminvid2lem  21912  m2cpminvid2  21913  decpmatmul  21930  pmatcollpw1lem2  21933  pmatcollpw1  21934  pmatcollpw2lem  21935  pmatcollpwfi  21940  pm2mpcl  21955  mply1topmatcl  21963  mp2pm2mplem2  21965  mp2pm2mplem4  21967  mp2pm2mplem5  21968  mp2pm2mp  21969  pm2mpghmlem2  21970  pm2mpghmlem1  21971  chfacfisfcpmat  22013  topssnei  22284  cnconst2  22443  cnpresti  22448  cnprest2  22450  cnpdis  22453  cnt0  22506  cnt1  22510  cnhaus  22514  sscmp  22565  hauscmp  22567  cnconn  22582  unconn  22589  finlocfin  22680  comppfsc  22692  kgen2ss  22715  ptpjopn  22772  prdstopn  22788  ptrescn  22799  qtopss  22875  kqfvima  22890  fbssint  22998  fbasrn  23044  filuni  23045  fmss  23106  rnelfm  23113  fmufil  23119  fmco  23121  flimss2  23132  flimss1  23133  flimrest  23143  cnpflf2  23160  flfcnp  23164  supnfcls  23180  fclsss1  23182  fclsss2  23183  isfcf  23194  subgntr  23267  opnsubg  23268  cldsubg  23271  ghmcnp  23275  ustuqtop1  23402  bldisj  23560  blgt0  23561  bl2in  23562  blss2ps  23565  blss2  23566  blssps  23586  blss  23587  xmetresbl  23599  lpbl  23668  blcld  23670  stdbdmopn  23683  metcnp3  23705  metcnp  23706  metcnp2  23707  txmetcnp  23712  blval2  23727  nmoix  23902  nmoi2  23903  nmotri  23912  metdsge  24021  metdseq0  24026  iocopnst  24112  xrhmeo  24118  nmhmcn  24292  cphsqrtcl2  24359  cphsqrtcl3  24360  cssbn  24548  pjth  24612  ovoliunlem2  24676  volun  24718  mbfimaopn2  24830  iblconst  24991  limcvallem  25044  dvfval  25070  dvcnp2  25093  dvcn  25094  deg1mul3le  25290  deg1tmle  25291  dvdsq1p  25334  ig1peu  25345  ig1pdvds  25350  ply1term  25374  coeid3  25410  dgrmulc  25441  dvply1  25453  aaliou2  25509  efcvx  25617  tanord  25703  eflogeq  25766  logdivlti  25784  logccv  25827  recxpcl  25839  cxplea  25860  cxpeq  25919  ang180  25973  isosctrlem2  25978  cxp2lim  26135  amgm  26149  muval1  26291  dvdssqf  26296  mumullem2  26338  mumul  26339  bcmono  26434  lgsneg  26478  lgsdilem  26481  lgsdirprm  26488  lgsdir  26489  lgsdi  26491  lgsne0  26492  brbtwn2  27282  colinearalglem1  27283  colinearalg  27287  axcgrtr  27292  axsegconlem8  27301  axsegconlem9  27302  axsegconlem10  27303  axcontlem2  27342  axcontlem10  27350  elntg2  27362  ewlkle  27981  crctcshwlkn0lem5  28188  wwlknp  28217  wwlksnext  28267  wwlksnextproplem1  28283  wspthsnwspthsnon  28290  clwlkclwwlklem3  28374  erclwwlksym  28394  erclwwlknsym  28443  upgriseupth  28580  eucrct2eupth  28618  3cyclfrgrrn  28659  numclwwlk2lem1lem  28715  numclwwlk1lem2foa  28727  frgrregord13  28769  nvmul0or  29021  ipval2lem2  29075  lnoadd  29129  lnosub  29130  lnomul  29131  shless  29730  shlej1  29731  kbmul  30326  homco2  30348  kbass2  30488  eliccelico  31107  elicoelioo  31108  iocinioc2  31109  iocinif  31111  difioo  31112  swrdrn2  31235  swrdrn3  31236  xrge0adddir  31310  xrge0npcan  31312  isarchi2  31448  archiabl  31461  rhmdvdsr  31526  pidlnz  31580  lindssn  31582  ssmxidl  31651  pstmfval  31855  fmcncfil  31890  zrhnm  31928  qqhnm  31949  nexple  31986  volfiniune  32207  dya2iocnrect  32257  probinc  32397  cndprob01  32411  signswmnd  32545  bnj517  32874  cvmsss2  33245  cvmlift2lem10  33283  br6  33733  funsseq  33751  nolesgn2o  33883  nogesgn1o  33885  nosep1o  33893  nosep2o  33894  nosepssdm  33898  nosupres  33919  nosupbnd1lem1  33920  nosupbnd1lem4  33923  nosupbnd1lem5  33924  nosupbnd1lem6  33925  noinfres  33934  noinfbnd1lem1  33935  noinfbnd1lem4  33938  noinfbnd1lem6  33940  noinfbnd2  33943  noetasuplem3  33947  noetainflem3  33951  cofsslt  34097  coinitsslt  34098  cofcutrtime  34102  cgrtriv  34313  5segofs  34317  btwnouttr2  34333  btwnxfr  34367  lineext  34387  btwnconn1lem13  34410  brsegle2  34420  nn0prpwlem  34520  lindsenlbs  35781  blbnd  35954  ismtyima  35970  rrndstprj2  35998  ghomdiv  36059  grpokerinj  36060  lsatfixedN  37030  lssat  37037  lshpkrlem4  37134  cvrcon3b  37298  atlen0  37331  atcvreq0  37335  atnle  37338  atlatmstc  37340  atlatle  37341  cvlcvr1  37360  hlsupr2  37408  hlrelat2  37424  cvrexchlem  37440  lnnat  37448  atcvrj2b  37453  3dimlem3  37482  3dim1  37488  1cvrjat  37496  llni  37529  llni2  37533  llnexatN  37542  2llnmat  37545  lplni  37553  2atnelpln  37565  llncvrlpln2  37578  2llnmj  37581  lplnexatN  37584  lplnexllnN  37585  2llnm3N  37590  lvoli  37596  lvoli3  37598  lvolnle3at  37603  islvol2aN  37613  4atlem4a  37620  4atlem4b  37621  4atlem11  37630  lplncvrlvol2  37636  2lplnmj  37643  islinei  37761  linepmap  37796  lnjatN  37801  lncvrat  37803  lncmp  37804  elpaddn0  37821  elpaddatriN  37824  elpaddat  37825  paddcom  37834  paddss2  37839  paddss12  37840  paddasslem4  37844  paddasslem9  37849  paddasslem10  37850  pmodl42N  37872  pmapjoin  37873  llnmod1i2  37881  polcon2bN  37941  pclfinclN  37971  poml4N  37974  poml6N  37976  osumcllem1N  37977  osumcllem2N  37978  osumcllem11N  37987  osumclN  37988  pmapojoinN  37989  pexmidlem2N  37992  pexmidlem3N  37993  pexmidlem4N  37994  pexmidlem6N  37996  pexmidlem7N  37997  pl42lem2N  38001  pl42lem3N  38002  pl42lem4N  38003  pl42N  38004  lhprelat3N  38061  4atex  38097  lauteq  38116  lautco  38118  ltrncoidN  38149  ltrneq2  38169  ltrnideq  38196  trlnle  38207  trlval3  38208  cdlemc  38218  cdlemd9  38227  cdlemd  38228  cdleme21j  38357  cdleme21  38358  cdleme29ex  38395  cdlemefr27cl  38424  cdlemefs27cl  38434  cdleme32d  38465  cdleme32f  38467  cdleme35h2  38478  cdleme40m  38488  cdleme17d3  38517  cdleme48fvg  38521  cdlemeg46fvcl  38527  cdlemeg46fgN  38555  cdleme48fgv  38559  cdleme50trn3  38574  cdlemb3  38627  cdlemg8  38652  cdlemg11a  38658  cdlemg15a  38676  cdlemg15  38677  cdlemg16  38678  cdlemg16z  38680  cdlemg17dN  38684  cdlemg24  38709  cdlemg37  38710  cdlemg29  38726  cdlemg33b  38728  cdlemg38  38736  cdlemg40  38738  trlco  38748  cdlemg44b  38753  ltrncom  38759  trljco  38761  tendococl  38793  tendoplcl  38802  tendoplcom  38803  cdlemj2  38843  tendoid0  38846  tendo1ne0  38849  cdlemk25-3  38925  cdlemk36  38934  cdlemkid4  38955  cdlemk19x  38964  cdlemk53  38978  cdlemk56  38992  cdleml5N  39001  tendospcanN  39044  cdlemm10N  39139  dihord6apre  39277  dihord  39285  dihmeetlem1N  39311  dihglblem2N  39315  dihmeetlem2N  39320  dihmeetbN  39324  dihmeetlem5  39329  dihmeetlem6  39330  dihmeetlem7N  39331  dihmeetlem10N  39337  dihmeetlem12N  39339  dihmeetlem16N  39343  dihmeetlem17N  39344  dihmeetlem18N  39345  dihmeetALTN  39348  dihlspsnssN  39353  dvh3dim2  39469  dvh3dim3N  39470  lcfrlem16  39579  mapdrvallem2  39666  mapdh8ad  39800  hgmapvvlem3  39946  sticksstones1  40109  sticksstones2  40110  resubcan2  40378  diophrw  40588  eldioph2lem1  40589  diophrex  40604  rencldnfi  40650  pellexlem2  40659  pellqrexplicit  40706  infmrgelbi  40707  pellfundglb  40714  pellfund14gap  40716  rmxycomplete  40746  congadd  40795  acongeq  40812  jm2.19  40822  jm2.23  40825  jm2.20nn  40826  jm2.27  40837  jm3.1  40849  lnmepi  40917  lmhmlnmsplit  40919  hbtlem2  40956  dgraa0p  40981  idomrootle  41027  proot1hash  41032  iocunico  41049  iocinico  41050  fzunt  41069  relexpxpmin  41332  ntrclsk3  41687  grur1cld  41857  ismnu  41886  grumnudlem  41910  ismnushort  41926  rfcnnnub  42586  uzwo4  42608  wessf1ornlem  42729  supxrge  42884  infleinflem2  42917  iccintsng  43068  climsuse  43156  lptre2pt  43188  limcleqr  43192  0ellimcdiv  43197  fnlimfvre  43222  dvnprodlem1  43494  volioc  43520  stoweidlem17  43565  stoweidlem19  43567  stoweidlem20  43568  stoweidlem22  43570  stoweidlem28  43576  stoweidlem34  43582  stoweidlem44  43592  stoweidlem60  43608  wallispilem3  43615  fourierdlem42  43697  fourierdlem48  43702  fourierdlem51  43705  fourierdlem54  43708  fourierdlem74  43728  fourierdlem77  43731  fourierdlem87  43741  fourierdlem97  43751  ioorrnopnlem  43852  ovnsubaddlem2  44116  smfinflem  44361  eluzge0nn0  44815  fzopredsuc  44826  fzoopth  44830  imasetpreimafvbijlemfv  44865  lighneallem4  45073  oexpnegALTV  45140  oexpnegnz  45141  tgblthelfgott  45278  rmsupp0  45715  rmsuppss  45717  lincresunit3lem3  45826  lincresunit3lem2  45832  lindssnlvec  45838  fdivmptf  45898  refdivmptf  45899  elbigolo1  45914  rrx2linest  46099  itsclc0lem1  46113  itsclc0lem2  46114  itsclc0yqsollem1  46119  itsclc0b  46129