Theorem simpl2 1211

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl12  1268  simpl22  1271  simpl32  1274  simp1l2  1286  simp2l2  1292  simp3l2  1298  3anandirs  1502  rspc3ev  3596  2nreu  4405  f1prex  7315  weniso  7387  ofmpteq  7740  tfisi  7894  mposn  8141  fprlem1  8346  smogt  8403  smocdmdom  8404  omeulem1  8618  nnmord  8669  nnmword  8670  naddasslem1  8732  naddasslem2  8733  difsnen  9106  enfixsn  9133  mapunen  9193  ac6sfi  9303  ordiso2  9536  wemaplem2  9568  wemapso2lem  9573  en2eqpr  10113  acndom  10157  infmap2  10322  cflim2  10368  cfsmolem  10375  coftr  10378  fin23lem26  10430  isf32lem9  10466  fin1a2lem9  10513  fin1a2lem10  10514  gchdomtri  10741  canth4  10759  gchpwdom  10782  gruima  10914  grudomon  10929  prn0  11101  distrlem4pr  11138  prlem934  11145  addcan  11521  addcan2  11522  divmulass  12024  divmulasscom  12025  ltmul1a  12193  supmul1  12313  uzsupss  13094  xaddass  13406  xleadd1a  13410  xlesubadd  13420  xmulass  13444  xlemul2a  13446  xadddilem  13451  xadddi  13452  ixxdisj  13518  ixxun  13519  ixxlb  13525  icoshftf1o  13632  icodisj  13634  ioounsn  13635  lincmb01cmp  13653  iccf1o  13654  elfz1b  13754  ssfzoulel  13922  fzoopth  13924  modmuladd  14083  modaddmulmod  14108  ltexp2a  14336  leexp2  14341  ltexp2r  14343  exple1  14347  expnlbnd2  14405  mulsubdivbinom2  14433  fun2dmnop0  14676  ccatass  14761  swrdrn3  14830  ccatopth  14893  pfxccatin12lem2a  14904  repswpfx  14964  repswccat  14965  cshwidxmodr  14983  2cshw  14992  repsco  15019  s2f1o  15096  limsupgle  15673  limsupgre  15677  addcn2  15790  mulcn2  15792  binomrisefac  16237  dvdsval2  16454  dvdsadd2b  16505  dvdsmod  16528  oexpneg  16544  sadass  16670  gcdass  16749  rplpwr  16761  lcmass  16818  coprmdvds2  16858  rpmulgcd2  16860  rpdvds  16864  coprmprod  16865  cncongr2  16872  rpexp  16927  prmdiveq  16992  hashgcdlem  16994  odzdvds  17002  coprimeprodsq2  17016  pythagtriplem3  17025  pythagtriplem4  17026  pcdvdsb  17076  vdwnnlem1  17202  0ram  17227  ramz2  17231  ramub1lem1  17233  mremre  17803  mrieqv2d  17842  lubss  18716  lubun  18718  clatleglb  18721  clatglbss  18722  mrelatglb  18763  isnsgrp  18941  issubmnd  18982  gsumccat  19066  frmdss2  19088  submefmnd  19120  nmzsubg  19404  ghmnsgima  19483  gsmsymgreqlem1  19674  psgnunilem4  19741  odmodnn0  19784  odnncl  19789  odmod  19790  oddvds  19791  odeq  19794  odmulgid  19798  odmulgeq  19801  odbezout  19802  odf1o1  19816  odf1o2  19817  odngen  19821  gexdvdsi  19827  pgpfi1  19839  odcau  19848  subgslw  19860  fislw  19869  lsmless1x  19888  lsmless2x  19889  lsmsubm  19897  lsmmod  19919  lsmmod2  19920  efgsfo  19983  odadd1  20092  odadd2  20093  odadd  20094  lsmcomx  20100  prdscmnd  20105  gsumconst  20178  ablsimpgfindlem1  20353  csrgbinom  20488  ring1eq0  20559  mulgass2  20570  rngisom1  20726  rhmdvdsr  20788  cntzsubrng  20849  cntzsubr  20888  isdrng3lem2  21036  isabvd  21099  rmodislmod  21235  0lmhm  21345  lmhmvsca  21350  reslmhm2b  21359  pwssplit1  21364  pwssplit2  21365  pwssplit3  21366  lbspss  21387  lspsnat  21453  pidlnz  21558  lidldvgen  21688  xrsdsreclblem  21749  cssmre  22029  obs2ss  22065  uvcresum  22129  frlmsslsp  22132  frlmup4  22137  lindff1  22156  f1lindf  22158  lsslindf  22166  islindf4  22174  lindsenlbs  22187  issubassa  22205  evlsval2  22426  coe1subfv  22615  coe1sclmul  22631  coe1sclmul2  22633  mpomatmul  22791  mamutpos  22803  scmatscmide  22852  mavmulsolcl  22896  mulmarep1gsum2  22919  mdetdiaglem  22943  mdetdiag  22944  mdetunilem1  22957  mdetunilem3  22959  mdetunilem9  22965  maducoeval2  22985  madurid  22989  slesolinvbi  23029  cramerimplem1  23031  cramerlem1  23035  cramer  23039  cpmatel2  23061  m2cpm  23089  m2pmfzmap  23095  m2cpminvid2lem  23102  m2cpminvid2  23103  decpmatmul  23120  pmatcollpw1lem2  23123  pmatcollpw1  23124  pmatcollpw2lem  23125  pmatcollpwfi  23130  pm2mpcl  23145  mply1topmatcl  23153  mp2pm2mplem2  23155  mp2pm2mplem4  23157  mp2pm2mplem5  23158  mp2pm2mp  23159  pm2mpghmlem2  23160  pm2mpghmlem1  23161  chfacfisfcpmat  23203  topssnei  23472  cnconst2  23631  cnpresti  23636  cnprest2  23638  cnpdis  23641  cnt0  23694  cnt1  23698  cnhaus  23702  sscmp  23753  hauscmp  23755  cnconn  23770  unconn  23777  finlocfin  23869  comppfsc  23881  kgen2ss  23904  ptpjopn  23961  prdstopn  23977  ptrescn  23988  qtopss  24064  kqfvima  24079  fbssint  24187  fbasrn  24233  filuni  24234  fmss  24295  rnelfm  24302  fmufil  24308  fmco  24310  flimss2  24321  flimss1  24322  flimrest  24332  cnpflf2  24349  flfcnp  24353  supnfcls  24369  fclsss1  24371  fclsss2  24372  isfcf  24383  subgntr  24456  opnsubg  24457  cldsubg  24460  ghmcnp  24464  ustuqtop1  24590  bldisj  24747  blgt0  24748  bl2in  24749  blss2ps  24752  blss2  24753  blssps  24773  blss  24774  xmetresbl  24786  lpbl  24852  blcld  24854  stdbdmopn  24867  metcnp3  24889  metcnp  24890  metcnp2  24891  txmetcnp  24896  blval2  24911  nmoix  25078  nmoi2  25079  nmotri  25088  metdsge  25199  metdseq0  25204  iocopnst  25291  xrhmeo  25297  nmhmcn  25471  cphsqrtcl2  25537  cphsqrtcl3  25538  cssbn  25726  pjth  25790  ovoliunlem2  25854  volun  25896  mbfimaopn2  26008  iblconst  26168  limcvallem  26221  dvfval  26247  dvcnp2  26270  dvcn  26271  deg1mul3le  26465  deg1tmle  26466  dvdsq1p  26511  idomrootle  26521  ig1peu  26523  ig1pdvds  26528  ply1term  26552  coeid3  26589  dgrmulc  26620  dvply1  26635  aaliou2  26697  efcvx  26806  tanord  26896  eflogeq  26960  logdivlti  26978  logccv  27021  recxpcl  27033  cxplea  27054  cxpeq  27115  ang180  27172  isosctrlem2  27177  cxp2lim  27334  amgm  27348  muval1  27490  dvdssqf  27495  mumullem2  27537  mumul  27538  bcmono  27634  lgsneg  27678  lgsdilem  27681  lgsdirprm  27688  lgsdir  27689  lgsdi  27691  lgsne0  27692  nolesgn2o  28058  nogesgn1o  28060  nosep1o  28068  nosep2o  28069  nosepssdm  28073  nosupres  28094  nosupbnd1lem1  28095  nosupbnd1lem4  28098  nosupbnd1lem5  28099  nosupbnd1lem6  28100  noinfres  28109  noinfbnd1lem1  28110  noinfbnd1lem4  28113  noinfbnd1lem6  28115  noinfbnd2  28118  noetasuplem3  28122  noetainflem3  28126  leslss  28325  cofslts  28334  coinitslts  28335  cofcutrtime  28343  addsass  28421  addsdi  28571  mulsass  28582  ltmuls2  28587  divmulsw  28609  bdayfinbndlem1  28883  z12bdaylem  28900  brbtwn2  29513  colinearalglem1  29514  colinearalg  29518  axcgrtr  29523  axsegconlem8  29532  axsegconlem9  29533  axsegconlem10  29534  axcontlem2  29573  axcontlem10  29581  elntg2  29593  ewlkle  30216  crctcshwlkn0lem5  30433  wwlknp  30462  wwlksnext  30512  wwlksnextproplem1  30528  wspthsnwspthsnon  30535  clwlkclwwlklem3  30622  erclwwlksym  30642  erclwwlknsym  30691  upgriseupth  30838  eucrct2eupth  30876  3cyclfrgrrn  30917  numclwwlk2lem1lem  30973  numclwwlk1lem2foa  30985  frgrregord13  31027  nvmul0or  31282  ipval2lem2  31336  lnoadd  31390  lnosub  31391  lnomul  31392  shless  31991  shlej1  31992  kbmul  32587  homco2  32609  kbass2  32749  eliccelico  33439  elicoelioo  33440  iocinioc2  33441  iocinif  33443  difioo  33444  nexple  33494  swrdrn2  33587  xrge0adddir  33649  xrge0npcan  33651  isarchi2  33816  archiabl  33829  lindssn  34003  ssmxidl  34069  pstmfval  34598  fmcncfil  34633  zrhnm  34669  qqhnm  34692  volfiniune  34933  dya2iocnrect  34983  probinc  35123  cndprob01  35137  signswmnd  35256  bnj517  35585  cvmsss2  36206  cvmlift2lem10  36244  br6  36700  funsseq  36711  cgrtriv  36945  5segofs  36949  btwnouttr2  36965  btwnxfr  36999  lineext  37019  btwnconn1lem13  37042  brsegle2  37052  nmulss1  37141  ltnmul  37143  nmulle  37144  ltnadd  37145  naddle  37146  nadddi  37151  nn0prpwlem  37288  weiunpo  37431  weiunso  37432  weiunfr  37433  weiunse  37434  axtcond  37444  blbnd  38913  ismtyima  38929  rrndstprj2  38957  ghomdiv  39018  grpokerinj  39019  lsatfixedN  40258  lssat  40265  lshpkrlem4  40362  cvrcon3b  40526  atlen0  40559  atcvreq0  40563  atnle  40566  atlatmstc  40568  atlatle  40569  cvlcvr1  40588  hlsupr2  40636  hlrelat2  40652  cvrexchlem  40668  lnnat  40676  atcvrj2b  40681  3dimlem3  40710  3dim1  40716  1cvrjat  40724  llni  40757  llni2  40761  llnexatN  40770  2llnmat  40773  lplni  40781  2atnelpln  40793  llncvrlpln2  40806  2llnmj  40809  lplnexatN  40812  lplnexllnN  40813  2llnm3N  40818  lvoli  40824  lvoli3  40826  lvolnle3at  40831  islvol2aN  40841  4atlem4a  40848  4atlem4b  40849  4atlem11  40858  lplncvrlvol2  40864  2lplnmj  40871  islinei  40989  linepmap  41024  lnjatN  41029  lncvrat  41031  lncmp  41032  elpaddn0  41049  elpaddatriN  41052  elpaddat  41053  paddcom  41062  paddss2  41067  paddss12  41068  paddasslem4  41072  paddasslem9  41077  paddasslem10  41078  pmodl42N  41100  pmapjoin  41101  llnmod1i2  41109  polcon2bN  41169  pclfinclN  41199  poml4N  41202  poml6N  41204  osumcllem1N  41205  osumcllem2N  41206  osumcllem11N  41215  osumclN  41216  pmapojoinN  41217  pexmidlem2N  41220  pexmidlem3N  41221  pexmidlem4N  41222  pexmidlem6N  41224  pexmidlem7N  41225  pl42lem2N  41229  pl42lem3N  41230  pl42lem4N  41231  pl42N  41232  lhprelat3N  41289  4atex  41325  lauteq  41344  lautco  41346  ltrncoidN  41377  ltrneq2  41397  ltrnideq  41424  trlnle  41435  trlval3  41436  cdlemc  41446  cdlemd9  41455  cdlemd  41456  cdleme21j  41585  cdleme21  41586  cdleme29ex  41623  cdlemefr27cl  41652  cdlemefs27cl  41662  cdleme32d  41693  cdleme32f  41695  cdleme35h2  41706  cdleme40m  41716  cdleme17d3  41745  cdleme48fvg  41749  cdlemeg46fvcl  41755  cdlemeg46fgN  41783  cdleme48fgv  41787  cdleme50trn3  41802  cdlemb3  41855  cdlemg8  41880  cdlemg11a  41886  cdlemg15a  41904  cdlemg15  41905  cdlemg16  41906  cdlemg16z  41908  cdlemg17dN  41912  cdlemg24  41937  cdlemg37  41938  cdlemg29  41954  cdlemg33b  41956  cdlemg38  41964  cdlemg40  41966  trlco  41976  cdlemg44b  41981  ltrncom  41987  trljco  41989  tendococl  42021  tendoplcl  42030  tendoplcom  42031  cdlemj2  42071  tendoid0  42074  tendo1ne0  42077  cdlemk25-3  42153  cdlemk36  42162  cdlemkid4  42183  cdlemk19x  42192  cdlemk53  42206  cdlemk56  42220  cdleml5N  42229  tendospcanN  42272  cdlemm10N  42367  dihord6apre  42505  dihord  42513  dihmeetlem1N  42539  dihglblem2N  42543  dihmeetlem2N  42548  dihmeetbN  42552  dihmeetlem5  42557  dihmeetlem6  42558  dihmeetlem7N  42559  dihmeetlem10N  42565  dihmeetlem12N  42567  dihmeetlem16N  42571  dihmeetlem17N  42572  dihmeetlem18N  42573  dihmeetALTN  42576  dihlspsnssN  42581  dvh3dim2  42697  dvh3dim3N  42698  lcfrlem16  42807  mapdrvallem2  42894  mapdh8ad  43028  hgmapvvlem3  43174  sticksstones1  43388  sticksstones2  43389  aks6d1c6isolem1  43416  resubcan2  43632  diophrw  43963  eldioph2lem1  43964  diophrex  43979  rencldnfi  44021  pellexlem2  44030  pellqrexplicit  44077  infmrgelbi  44078  pellfundglb  44085  pellfund14gap  44087  rmxycomplete  44117  congadd  44166  acongeq  44183  jm2.19  44193  jm2.23  44196  jm2.20nn  44197  jm2.27  44208  jm3.1  44220  lnmepi  44280  lmhmlnmsplit  44282  hbtlem2  44318  dgraa0p  44343  proot1hash  44389  iocunico  44405  iocinico  44406  oasubex  44480  cantnf2  44519  onmcl  44525  omcl2  44527  nadd2rabex  44580  nadd1rabtr  44582  nadd1rabex  44584  fzunt  44648  relexpxpmin  44909  ntrclsk3  45262  grur1cld  45422  ismnu  45437  grumnudlem  45461  ismnushort  45477  rfcnnnub  46258  uzwo4  46275  wessf1ornlem  46405  supxrge  46555  infleinflem2  46587  iccintsng  46740  climsuse  46825  lptre2pt  46855  limcleqr  46859  0ellimcdiv  46864  fnlimfvre  46889  dvnprodlem1  47161  volioc  47187  stoweidlem17  47232  stoweidlem19  47234  stoweidlem20  47235  stoweidlem22  47237  stoweidlem28  47243  stoweidlem34  47249  stoweidlem44  47259  stoweidlem60  47275  wallispilem3  47282  fourierdlem42  47364  fourierdlem48  47369  fourierdlem51  47372  fourierdlem54  47375  fourierdlem74  47395  fourierdlem77  47398  fourierdlem87  47408  fourierdlem97  47418  ioorrnopnlem  47519  ovnsubaddlem2  47786  smfinflem  48032  fsupdm  48057  finfdm  48061  eluzge0nn0  48587  fzopredsuc  48599  imasetpreimafvbijlemfv  48689  lighneallem4  48900  oexpnegALTV  48980  oexpnegnz  48981  tgblthelfgott  49118  clnbgrgrim  49237  isubgr3stgrlem3  49271  rmsupp0  49685  rmsuppss  49687  lincresunit3lem3  49791  lincresunit3lem2  49797  lindssnlvec  49803  fdivmptf  49858  refdivmptf  49859  elbigolo1  49874  rrx2linest  50059  itsclc0lem1  50073  itsclc0lem2  50074  itsclc0yqsollem1  50079  itsclc0b  50089  setc1onsubc  50945