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  3618  2nreu  4419  f1prex  7276  weniso  7346  ofmpteq  7692  tfisi  7852  mposn  8100  fprlem1  8297  smogt  8379  smocdmdom  8380  omeulem1  8592  nnmord  8642  nnmword  8643  naddasslem1  8704  naddasslem2  8705  difsnen  9065  enfixsn  9093  mapunen  9158  ac6sfi  9290  ordiso2  9527  wemaplem2  9559  wemapso2lem  9564  en2eqpr  10019  acndom  10063  infmap2  10229  cflim2  10275  cfsmolem  10282  coftr  10285  fin23lem26  10337  isf32lem9  10373  fin1a2lem9  10420  fin1a2lem10  10421  gchdomtri  10641  canth4  10659  gchpwdom  10682  gruima  10814  grudomon  10829  prn0  11001  distrlem4pr  11038  prlem934  11045  addcan  11417  addcan2  11418  divmulass  11917  divmulasscom  11918  ltmul1a  12088  supmul1  12209  uzsupss  12954  xaddass  13263  xleadd1a  13267  xlesubadd  13277  xmulass  13301  xlemul2a  13303  xadddilem  13308  xadddi  13309  ixxdisj  13375  ixxun  13376  ixxlb  13382  icoshftf1o  13489  icodisj  13491  ioounsn  13492  lincmb01cmp  13510  iccf1o  13511  elfz1b  13608  ssfzoulel  13774  fzoopth  13776  modmuladd  13929  modaddmulmod  13954  ltexp2a  14182  leexp2  14187  ltexp2r  14189  exple1  14193  expnlbnd2  14250  mulsubdivbinom2  14278  fun2dmnop0  14520  ccatass  14604  ccatopth  14732  pfxccatin12lem2a  14743  repswpfx  14801  repswccat  14802  cshwidxmodr  14820  2cshw  14829  repsco  14857  s2f1o  14933  limsupgle  15491  limsupgre  15495  addcn2  15608  mulcn2  15610  binomrisefac  16056  dvdsval2  16273  dvdsadd2b  16323  dvdsmod  16346  oexpneg  16362  sadass  16488  gcdass  16564  rplpwr  16575  lcmass  16631  coprmdvds2  16671  rpmulgcd2  16673  rpdvds  16677  coprmprod  16678  cncongr2  16685  rpexp  16739  prmdiveq  16803  hashgcdlem  16805  odzdvds  16813  coprimeprodsq2  16827  pythagtriplem3  16836  pythagtriplem4  16837  pcdvdsb  16887  vdwnnlem1  17013  0ram  17038  ramz2  17042  ramub1lem1  17044  mremre  17614  mrieqv2d  17649  lubss  18521  lubun  18523  clatleglb  18526  clatglbss  18527  mrelatglb  18568  isnsgrp  18699  issubmnd  18737  gsumccat  18817  frmdss2  18839  submefmnd  18871  nmzsubg  19146  ghmnsgima  19221  gsmsymgreqlem1  19409  psgnunilem4  19476  odmodnn0  19519  odnncl  19524  odmod  19525  oddvds  19526  odeq  19529  odmulgid  19533  odmulgeq  19536  odbezout  19537  odf1o1  19551  odf1o2  19552  odngen  19556  gexdvdsi  19562  pgpfi1  19574  odcau  19583  subgslw  19595  fislw  19604  lsmless1x  19623  lsmless2x  19624  lsmsubm  19632  lsmmod  19654  lsmmod2  19655  efgsfo  19718  odadd1  19827  odadd2  19828  odadd  19829  lsmcomx  19835  prdscmnd  19840  gsumconst  19913  ablsimpgfindlem1  20088  srg1zr  20173  csrgbinom  20190  ring1eq0  20256  mulgass2  20267  rngisom1  20424  rhmdvdsr  20466  cntzsubrng  20525  cntzsubr  20564  isabvd  20770  rmodislmod  20885  0lmhm  20996  lmhmvsca  21001  reslmhm2b  21010  pwssplit1  21015  pwssplit2  21016  pwssplit3  21017  lbspss  21038  lspsnat  21104  lidldvgen  21293  xrsdsreclblem  21378  cssmre  21651  obs2ss  21687  uvcresum  21751  frlmsslsp  21754  frlmup4  21759  lindff1  21778  f1lindf  21780  lsslindf  21788  islindf4  21796  issubassa  21825  evlsval2  22043  coe1subfv  22201  coe1sclmul  22217  coe1sclmul2  22219  mpomatmul  22382  mamutpos  22394  scmatscmide  22443  mavmulsolcl  22487  mulmarep1gsum2  22510  mdetdiaglem  22534  mdetdiag  22535  mdetunilem1  22548  mdetunilem3  22550  mdetunilem9  22556  maducoeval2  22576  madurid  22580  slesolinvbi  22617  cramerimplem1  22619  cramerlem1  22623  cramer  22627  cpmatel2  22649  m2cpm  22677  m2pmfzmap  22683  m2cpminvid2lem  22690  m2cpminvid2  22691  decpmatmul  22708  pmatcollpw1lem2  22711  pmatcollpw1  22712  pmatcollpw2lem  22713  pmatcollpwfi  22718  pm2mpcl  22733  mply1topmatcl  22741  mp2pm2mplem2  22743  mp2pm2mplem4  22745  mp2pm2mplem5  22746  mp2pm2mp  22747  pm2mpghmlem2  22748  pm2mpghmlem1  22749  chfacfisfcpmat  22791  topssnei  23060  cnconst2  23219  cnpresti  23224  cnprest2  23226  cnpdis  23229  cnt0  23282  cnt1  23286  cnhaus  23290  sscmp  23341  hauscmp  23343  cnconn  23358  unconn  23365  finlocfin  23456  comppfsc  23468  kgen2ss  23491  ptpjopn  23548  prdstopn  23564  ptrescn  23575  qtopss  23651  kqfvima  23666  fbssint  23774  fbasrn  23820  filuni  23821  fmss  23882  rnelfm  23889  fmufil  23895  fmco  23897  flimss2  23908  flimss1  23909  flimrest  23919  cnpflf2  23936  flfcnp  23940  supnfcls  23956  fclsss1  23958  fclsss2  23959  isfcf  23970  subgntr  24043  opnsubg  24044  cldsubg  24047  ghmcnp  24051  ustuqtop1  24178  bldisj  24335  blgt0  24336  bl2in  24337  blss2ps  24340  blss2  24341  blssps  24361  blss  24362  xmetresbl  24374  lpbl  24440  blcld  24442  stdbdmopn  24455  metcnp3  24477  metcnp  24478  metcnp2  24479  txmetcnp  24484  blval2  24499  nmoix  24666  nmoi2  24667  nmotri  24676  metdsge  24787  metdseq0  24792  iocopnst  24886  xrhmeo  24893  nmhmcn  25069  cphsqrtcl2  25136  cphsqrtcl3  25137  cssbn  25325  pjth  25389  ovoliunlem2  25454  volun  25496  mbfimaopn2  25608  iblconst  25769  limcvallem  25822  dvfval  25848  dvcnp2  25871  dvcnp2OLD  25872  dvcn  25873  deg1mul3le  26072  deg1tmle  26073  dvdsq1p  26118  idomrootle  26128  ig1peu  26130  ig1pdvds  26135  ply1term  26159  coeid3  26195  dgrmulc  26227  dvply1  26241  aaliou2  26298  efcvx  26409  tanord  26497  eflogeq  26561  logdivlti  26579  logccv  26622  recxpcl  26634  cxplea  26655  cxpeq  26717  ang180  26774  isosctrlem2  26779  cxp2lim  26937  amgm  26951  muval1  27093  dvdssqf  27098  mumullem2  27140  mumul  27141  bcmono  27238  lgsneg  27282  lgsdilem  27285  lgsdirprm  27292  lgsdir  27293  lgsdi  27295  lgsne0  27296  nolesgn2o  27633  nogesgn1o  27635  nosep1o  27643  nosep2o  27644  nosepssdm  27648  nosupres  27669  nosupbnd1lem1  27670  nosupbnd1lem4  27673  nosupbnd1lem5  27674  nosupbnd1lem6  27675  noinfres  27684  noinfbnd1lem1  27685  noinfbnd1lem4  27688  noinfbnd1lem6  27690  noinfbnd2  27693  noetasuplem3  27697  noetainflem3  27701  slelss  27863  cofsslt  27869  coinitsslt  27870  cofcutrtime  27878  addsass  27955  addsdi  28098  mulsass  28109  sltmul2  28114  divsmulw  28135  brbtwn2  28830  colinearalglem1  28831  colinearalg  28835  axcgrtr  28840  axsegconlem8  28849  axsegconlem9  28850  axsegconlem10  28851  axcontlem2  28890  axcontlem10  28898  elntg2  28910  ewlkle  29531  crctcshwlkn0lem5  29742  wwlknp  29771  wwlksnext  29821  wwlksnextproplem1  29837  wspthsnwspthsnon  29844  clwlkclwwlklem3  29928  erclwwlksym  29948  erclwwlknsym  29997  upgriseupth  30134  eucrct2eupth  30172  3cyclfrgrrn  30213  numclwwlk2lem1lem  30269  numclwwlk1lem2foa  30281  frgrregord13  30323  nvmul0or  30577  ipval2lem2  30631  lnoadd  30685  lnosub  30686  lnomul  30687  shless  31286  shlej1  31287  kbmul  31882  homco2  31904  kbass2  32044  eliccelico  32700  elicoelioo  32701  iocinioc2  32702  iocinif  32704  difioo  32705  nexple  32769  swrdrn2  32876  swrdrn3  32877  xrge0adddir  32959  xrge0npcan  32961  isarchi2  33129  archiabl  33142  pidlnz  33337  lindssn  33339  ssmxidl  33435  pstmfval  33873  fmcncfil  33908  zrhnm  33944  qqhnm  33967  volfiniune  34207  dya2iocnrect  34259  probinc  34399  cndprob01  34413  signswmnd  34535  bnj517  34862  cvmsss2  35242  cvmlift2lem10  35280  br6  35720  funsseq  35731  cgrtriv  35966  5segofs  35970  btwnouttr2  35986  btwnxfr  36020  lineext  36040  btwnconn1lem13  36063  brsegle2  36073  nn0prpwlem  36286  weiunpo  36429  weiunso  36430  weiunfr  36431  weiunse  36432  lindsenlbs  37585  blbnd  37757  ismtyima  37773  rrndstprj2  37801  ghomdiv  37862  grpokerinj  37863  lsatfixedN  38973  lssat  38980  lshpkrlem4  39077  cvrcon3b  39241  atlen0  39274  atcvreq0  39278  atnle  39281  atlatmstc  39283  atlatle  39284  cvlcvr1  39303  hlsupr2  39352  hlrelat2  39368  cvrexchlem  39384  lnnat  39392  atcvrj2b  39397  3dimlem3  39426  3dim1  39432  1cvrjat  39440  llni  39473  llni2  39477  llnexatN  39486  2llnmat  39489  lplni  39497  2atnelpln  39509  llncvrlpln2  39522  2llnmj  39525  lplnexatN  39528  lplnexllnN  39529  2llnm3N  39534  lvoli  39540  lvoli3  39542  lvolnle3at  39547  islvol2aN  39557  4atlem4a  39564  4atlem4b  39565  4atlem11  39574  lplncvrlvol2  39580  2lplnmj  39587  islinei  39705  linepmap  39740  lnjatN  39745  lncvrat  39747  lncmp  39748  elpaddn0  39765  elpaddatriN  39768  elpaddat  39769  paddcom  39778  paddss2  39783  paddss12  39784  paddasslem4  39788  paddasslem9  39793  paddasslem10  39794  pmodl42N  39816  pmapjoin  39817  llnmod1i2  39825  polcon2bN  39885  pclfinclN  39915  poml4N  39918  poml6N  39920  osumcllem1N  39921  osumcllem2N  39922  osumcllem11N  39931  osumclN  39932  pmapojoinN  39933  pexmidlem2N  39936  pexmidlem3N  39937  pexmidlem4N  39938  pexmidlem6N  39940  pexmidlem7N  39941  pl42lem2N  39945  pl42lem3N  39946  pl42lem4N  39947  pl42N  39948  lhprelat3N  40005  4atex  40041  lauteq  40060  lautco  40062  ltrncoidN  40093  ltrneq2  40113  ltrnideq  40140  trlnle  40151  trlval3  40152  cdlemc  40162  cdlemd9  40171  cdlemd  40172  cdleme21j  40301  cdleme21  40302  cdleme29ex  40339  cdlemefr27cl  40368  cdlemefs27cl  40378  cdleme32d  40409  cdleme32f  40411  cdleme35h2  40422  cdleme40m  40432  cdleme17d3  40461  cdleme48fvg  40465  cdlemeg46fvcl  40471  cdlemeg46fgN  40499  cdleme48fgv  40503  cdleme50trn3  40518  cdlemb3  40571  cdlemg8  40596  cdlemg11a  40602  cdlemg15a  40620  cdlemg15  40621  cdlemg16  40622  cdlemg16z  40624  cdlemg17dN  40628  cdlemg24  40653  cdlemg37  40654  cdlemg29  40670  cdlemg33b  40672  cdlemg38  40680  cdlemg40  40682  trlco  40692  cdlemg44b  40697  ltrncom  40703  trljco  40705  tendococl  40737  tendoplcl  40746  tendoplcom  40747  cdlemj2  40787  tendoid0  40790  tendo1ne0  40793  cdlemk25-3  40869  cdlemk36  40878  cdlemkid4  40899  cdlemk19x  40908  cdlemk53  40922  cdlemk56  40936  cdleml5N  40945  tendospcanN  40988  cdlemm10N  41083  dihord6apre  41221  dihord  41229  dihmeetlem1N  41255  dihglblem2N  41259  dihmeetlem2N  41264  dihmeetbN  41268  dihmeetlem5  41273  dihmeetlem6  41274  dihmeetlem7N  41275  dihmeetlem10N  41281  dihmeetlem12N  41283  dihmeetlem16N  41287  dihmeetlem17N  41288  dihmeetlem18N  41289  dihmeetALTN  41292  dihlspsnssN  41297  dvh3dim2  41413  dvh3dim3N  41414  lcfrlem16  41523  mapdrvallem2  41610  mapdh8ad  41744  hgmapvvlem3  41890  sticksstones1  42105  sticksstones2  42106  aks6d1c6isolem1  42133  resubcan2  42378  diophrw  42729  eldioph2lem1  42730  diophrex  42745  rencldnfi  42791  pellexlem2  42800  pellqrexplicit  42847  infmrgelbi  42848  pellfundglb  42855  pellfund14gap  42857  rmxycomplete  42888  congadd  42937  acongeq  42954  jm2.19  42964  jm2.23  42967  jm2.20nn  42968  jm2.27  42979  jm3.1  42991  lnmepi  43056  lmhmlnmsplit  43058  hbtlem2  43095  dgraa0p  43120  proot1hash  43166  iocunico  43182  iocinico  43183  oasubex  43257  cantnf2  43296  onmcl  43302  omcl2  43304  nadd2rabex  43357  nadd1rabtr  43359  nadd1rabex  43361  fzunt  43426  relexpxpmin  43688  ntrclsk3  44041  grur1cld  44204  ismnu  44233  grumnudlem  44257  ismnushort  44273  rfcnnnub  45008  uzwo4  45025  wessf1ornlem  45157  supxrge  45313  infleinflem2  45346  iccintsng  45500  climsuse  45585  lptre2pt  45617  limcleqr  45621  0ellimcdiv  45626  fnlimfvre  45651  dvnprodlem1  45923  volioc  45949  stoweidlem17  45994  stoweidlem19  45996  stoweidlem20  45997  stoweidlem22  45999  stoweidlem28  46005  stoweidlem34  46011  stoweidlem44  46021  stoweidlem60  46037  wallispilem3  46044  fourierdlem42  46126  fourierdlem48  46131  fourierdlem51  46134  fourierdlem54  46137  fourierdlem74  46157  fourierdlem77  46160  fourierdlem87  46170  fourierdlem97  46180  ioorrnopnlem  46281  ovnsubaddlem2  46548  smfinflem  46794  fsupdm  46819  finfdm  46823  eluzge0nn0  47289  fzopredsuc  47300  imasetpreimafvbijlemfv  47364  lighneallem4  47572  oexpnegALTV  47639  oexpnegnz  47640  tgblthelfgott  47777  clnbgrgrim  47895  isubgr3stgrlem3  47928  rmsupp0  48291  rmsuppss  48293  lincresunit3lem3  48398  lincresunit3lem2  48404  lindssnlvec  48410  fdivmptf  48469  refdivmptf  48470  elbigolo1  48485  rrx2linest  48670  itsclc0lem1  48684  itsclc0lem2  48685  itsclc0yqsollem1  48690  itsclc0b  48700  setc1onsubc  49427