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  3605  2nreu  4407  f1prex  7259  weniso  7329  ofmpteq  7676  tfisi  7835  mposn  8082  fprlem1  8279  smogt  8336  smocdmdom  8337  omeulem1  8546  nnmord  8596  nnmword  8597  naddasslem1  8658  naddasslem2  8659  difsnen  9023  enfixsn  9050  mapunen  9110  ac6sfi  9231  ordiso2  9468  wemaplem2  9500  wemapso2lem  9505  en2eqpr  9960  acndom  10004  infmap2  10170  cflim2  10216  cfsmolem  10223  coftr  10226  fin23lem26  10278  isf32lem9  10314  fin1a2lem9  10361  fin1a2lem10  10362  gchdomtri  10582  canth4  10600  gchpwdom  10623  gruima  10755  grudomon  10770  prn0  10942  distrlem4pr  10979  prlem934  10986  addcan  11358  addcan2  11359  divmulass  11860  divmulasscom  11861  ltmul1a  12031  supmul1  12152  uzsupss  12899  xaddass  13209  xleadd1a  13213  xlesubadd  13223  xmulass  13247  xlemul2a  13249  xadddilem  13254  xadddi  13255  ixxdisj  13321  ixxun  13322  ixxlb  13328  icoshftf1o  13435  icodisj  13437  ioounsn  13438  lincmb01cmp  13456  iccf1o  13457  elfz1b  13554  ssfzoulel  13721  fzoopth  13723  modmuladd  13878  modaddmulmod  13903  ltexp2a  14131  leexp2  14136  ltexp2r  14138  exple1  14142  expnlbnd2  14199  mulsubdivbinom2  14227  fun2dmnop0  14469  ccatass  14553  ccatopth  14681  pfxccatin12lem2a  14692  repswpfx  14750  repswccat  14751  cshwidxmodr  14769  2cshw  14778  repsco  14806  s2f1o  14882  limsupgle  15443  limsupgre  15447  addcn2  15560  mulcn2  15562  binomrisefac  16008  dvdsval2  16225  dvdsadd2b  16276  dvdsmod  16299  oexpneg  16315  sadass  16441  gcdass  16517  rplpwr  16528  lcmass  16584  coprmdvds2  16624  rpmulgcd2  16626  rpdvds  16630  coprmprod  16631  cncongr2  16638  rpexp  16692  prmdiveq  16756  hashgcdlem  16758  odzdvds  16766  coprimeprodsq2  16780  pythagtriplem3  16789  pythagtriplem4  16790  pcdvdsb  16840  vdwnnlem1  16966  0ram  16991  ramz2  16995  ramub1lem1  16997  mremre  17565  mrieqv2d  17600  lubss  18472  lubun  18474  clatleglb  18477  clatglbss  18478  mrelatglb  18519  isnsgrp  18650  issubmnd  18688  gsumccat  18768  frmdss2  18790  submefmnd  18822  nmzsubg  19097  ghmnsgima  19172  gsmsymgreqlem1  19360  psgnunilem4  19427  odmodnn0  19470  odnncl  19475  odmod  19476  oddvds  19477  odeq  19480  odmulgid  19484  odmulgeq  19487  odbezout  19488  odf1o1  19502  odf1o2  19503  odngen  19507  gexdvdsi  19513  pgpfi1  19525  odcau  19534  subgslw  19546  fislw  19555  lsmless1x  19574  lsmless2x  19575  lsmsubm  19583  lsmmod  19605  lsmmod2  19606  efgsfo  19669  odadd1  19778  odadd2  19779  odadd  19780  lsmcomx  19786  prdscmnd  19791  gsumconst  19864  ablsimpgfindlem1  20039  srg1zr  20124  csrgbinom  20141  ring1eq0  20207  mulgass2  20218  rngisom1  20375  rhmdvdsr  20417  cntzsubrng  20476  cntzsubr  20515  isabvd  20721  rmodislmod  20836  0lmhm  20947  lmhmvsca  20952  reslmhm2b  20961  pwssplit1  20966  pwssplit2  20967  pwssplit3  20968  lbspss  20989  lspsnat  21055  lidldvgen  21244  xrsdsreclblem  21329  cssmre  21602  obs2ss  21638  uvcresum  21702  frlmsslsp  21705  frlmup4  21710  lindff1  21729  f1lindf  21731  lsslindf  21739  islindf4  21747  issubassa  21776  evlsval2  21994  coe1subfv  22152  coe1sclmul  22168  coe1sclmul2  22170  mpomatmul  22333  mamutpos  22345  scmatscmide  22394  mavmulsolcl  22438  mulmarep1gsum2  22461  mdetdiaglem  22485  mdetdiag  22486  mdetunilem1  22499  mdetunilem3  22501  mdetunilem9  22507  maducoeval2  22527  madurid  22531  slesolinvbi  22568  cramerimplem1  22570  cramerlem1  22574  cramer  22578  cpmatel2  22600  m2cpm  22628  m2pmfzmap  22634  m2cpminvid2lem  22641  m2cpminvid2  22642  decpmatmul  22659  pmatcollpw1lem2  22662  pmatcollpw1  22663  pmatcollpw2lem  22664  pmatcollpwfi  22669  pm2mpcl  22684  mply1topmatcl  22692  mp2pm2mplem2  22694  mp2pm2mplem4  22696  mp2pm2mplem5  22697  mp2pm2mp  22698  pm2mpghmlem2  22699  pm2mpghmlem1  22700  chfacfisfcpmat  22742  topssnei  23011  cnconst2  23170  cnpresti  23175  cnprest2  23177  cnpdis  23180  cnt0  23233  cnt1  23237  cnhaus  23241  sscmp  23292  hauscmp  23294  cnconn  23309  unconn  23316  finlocfin  23407  comppfsc  23419  kgen2ss  23442  ptpjopn  23499  prdstopn  23515  ptrescn  23526  qtopss  23602  kqfvima  23617  fbssint  23725  fbasrn  23771  filuni  23772  fmss  23833  rnelfm  23840  fmufil  23846  fmco  23848  flimss2  23859  flimss1  23860  flimrest  23870  cnpflf2  23887  flfcnp  23891  supnfcls  23907  fclsss1  23909  fclsss2  23910  isfcf  23921  subgntr  23994  opnsubg  23995  cldsubg  23998  ghmcnp  24002  ustuqtop1  24129  bldisj  24286  blgt0  24287  bl2in  24288  blss2ps  24291  blss2  24292  blssps  24312  blss  24313  xmetresbl  24325  lpbl  24391  blcld  24393  stdbdmopn  24406  metcnp3  24428  metcnp  24429  metcnp2  24430  txmetcnp  24435  blval2  24450  nmoix  24617  nmoi2  24618  nmotri  24627  metdsge  24738  metdseq0  24743  iocopnst  24837  xrhmeo  24844  nmhmcn  25020  cphsqrtcl2  25086  cphsqrtcl3  25087  cssbn  25275  pjth  25339  ovoliunlem2  25404  volun  25446  mbfimaopn2  25558  iblconst  25719  limcvallem  25772  dvfval  25798  dvcnp2  25821  dvcnp2OLD  25822  dvcn  25823  deg1mul3le  26022  deg1tmle  26023  dvdsq1p  26068  idomrootle  26078  ig1peu  26080  ig1pdvds  26085  ply1term  26109  coeid3  26145  dgrmulc  26177  dvply1  26191  aaliou2  26248  efcvx  26359  tanord  26447  eflogeq  26511  logdivlti  26529  logccv  26572  recxpcl  26584  cxplea  26605  cxpeq  26667  ang180  26724  isosctrlem2  26729  cxp2lim  26887  amgm  26901  muval1  27043  dvdssqf  27048  mumullem2  27090  mumul  27091  bcmono  27188  lgsneg  27232  lgsdilem  27235  lgsdirprm  27242  lgsdir  27243  lgsdi  27245  lgsne0  27246  nolesgn2o  27583  nogesgn1o  27585  nosep1o  27593  nosep2o  27594  nosepssdm  27598  nosupres  27619  nosupbnd1lem1  27620  nosupbnd1lem4  27623  nosupbnd1lem5  27624  nosupbnd1lem6  27625  noinfres  27634  noinfbnd1lem1  27635  noinfbnd1lem4  27638  noinfbnd1lem6  27640  noinfbnd2  27643  noetasuplem3  27647  noetainflem3  27651  slelss  27820  cofsslt  27826  coinitsslt  27827  cofcutrtime  27835  addsass  27912  addsdi  28058  mulsass  28069  sltmul2  28074  divsmulw  28096  brbtwn2  28832  colinearalglem1  28833  colinearalg  28837  axcgrtr  28842  axsegconlem8  28851  axsegconlem9  28852  axsegconlem10  28853  axcontlem2  28892  axcontlem10  28900  elntg2  28912  ewlkle  29533  crctcshwlkn0lem5  29744  wwlknp  29773  wwlksnext  29823  wwlksnextproplem1  29839  wspthsnwspthsnon  29846  clwlkclwwlklem3  29930  erclwwlksym  29950  erclwwlknsym  29999  upgriseupth  30136  eucrct2eupth  30174  3cyclfrgrrn  30215  numclwwlk2lem1lem  30271  numclwwlk1lem2foa  30283  frgrregord13  30325  nvmul0or  30579  ipval2lem2  30633  lnoadd  30687  lnosub  30688  lnomul  30689  shless  31288  shlej1  31289  kbmul  31884  homco2  31906  kbass2  32046  eliccelico  32700  elicoelioo  32701  iocinioc2  32702  iocinif  32704  difioo  32705  nexple  32769  swrdrn2  32876  swrdrn3  32877  xrge0adddir  32959  xrge0npcan  32961  isarchi2  33139  archiabl  33152  pidlnz  33347  lindssn  33349  ssmxidl  33445  pstmfval  33886  fmcncfil  33921  zrhnm  33957  qqhnm  33980  volfiniune  34220  dya2iocnrect  34272  probinc  34412  cndprob01  34426  signswmnd  34548  bnj517  34875  cvmsss2  35261  cvmlift2lem10  35299  br6  35744  funsseq  35755  cgrtriv  35990  5segofs  35994  btwnouttr2  36010  btwnxfr  36044  lineext  36064  btwnconn1lem13  36087  brsegle2  36097  nn0prpwlem  36310  weiunpo  36453  weiunso  36454  weiunfr  36455  weiunse  36456  lindsenlbs  37609  blbnd  37781  ismtyima  37797  rrndstprj2  37825  ghomdiv  37886  grpokerinj  37887  lsatfixedN  39002  lssat  39009  lshpkrlem4  39106  cvrcon3b  39270  atlen0  39303  atcvreq0  39307  atnle  39310  atlatmstc  39312  atlatle  39313  cvlcvr1  39332  hlsupr2  39381  hlrelat2  39397  cvrexchlem  39413  lnnat  39421  atcvrj2b  39426  3dimlem3  39455  3dim1  39461  1cvrjat  39469  llni  39502  llni2  39506  llnexatN  39515  2llnmat  39518  lplni  39526  2atnelpln  39538  llncvrlpln2  39551  2llnmj  39554  lplnexatN  39557  lplnexllnN  39558  2llnm3N  39563  lvoli  39569  lvoli3  39571  lvolnle3at  39576  islvol2aN  39586  4atlem4a  39593  4atlem4b  39594  4atlem11  39603  lplncvrlvol2  39609  2lplnmj  39616  islinei  39734  linepmap  39769  lnjatN  39774  lncvrat  39776  lncmp  39777  elpaddn0  39794  elpaddatriN  39797  elpaddat  39798  paddcom  39807  paddss2  39812  paddss12  39813  paddasslem4  39817  paddasslem9  39822  paddasslem10  39823  pmodl42N  39845  pmapjoin  39846  llnmod1i2  39854  polcon2bN  39914  pclfinclN  39944  poml4N  39947  poml6N  39949  osumcllem1N  39950  osumcllem2N  39951  osumcllem11N  39960  osumclN  39961  pmapojoinN  39962  pexmidlem2N  39965  pexmidlem3N  39966  pexmidlem4N  39967  pexmidlem6N  39969  pexmidlem7N  39970  pl42lem2N  39974  pl42lem3N  39975  pl42lem4N  39976  pl42N  39977  lhprelat3N  40034  4atex  40070  lauteq  40089  lautco  40091  ltrncoidN  40122  ltrneq2  40142  ltrnideq  40169  trlnle  40180  trlval3  40181  cdlemc  40191  cdlemd9  40200  cdlemd  40201  cdleme21j  40330  cdleme21  40331  cdleme29ex  40368  cdlemefr27cl  40397  cdlemefs27cl  40407  cdleme32d  40438  cdleme32f  40440  cdleme35h2  40451  cdleme40m  40461  cdleme17d3  40490  cdleme48fvg  40494  cdlemeg46fvcl  40500  cdlemeg46fgN  40528  cdleme48fgv  40532  cdleme50trn3  40547  cdlemb3  40600  cdlemg8  40625  cdlemg11a  40631  cdlemg15a  40649  cdlemg15  40650  cdlemg16  40651  cdlemg16z  40653  cdlemg17dN  40657  cdlemg24  40682  cdlemg37  40683  cdlemg29  40699  cdlemg33b  40701  cdlemg38  40709  cdlemg40  40711  trlco  40721  cdlemg44b  40726  ltrncom  40732  trljco  40734  tendococl  40766  tendoplcl  40775  tendoplcom  40776  cdlemj2  40816  tendoid0  40819  tendo1ne0  40822  cdlemk25-3  40898  cdlemk36  40907  cdlemkid4  40928  cdlemk19x  40937  cdlemk53  40951  cdlemk56  40965  cdleml5N  40974  tendospcanN  41017  cdlemm10N  41112  dihord6apre  41250  dihord  41258  dihmeetlem1N  41284  dihglblem2N  41288  dihmeetlem2N  41293  dihmeetbN  41297  dihmeetlem5  41302  dihmeetlem6  41303  dihmeetlem7N  41304  dihmeetlem10N  41310  dihmeetlem12N  41312  dihmeetlem16N  41316  dihmeetlem17N  41317  dihmeetlem18N  41318  dihmeetALTN  41321  dihlspsnssN  41326  dvh3dim2  41442  dvh3dim3N  41443  lcfrlem16  41552  mapdrvallem2  41639  mapdh8ad  41773  hgmapvvlem3  41919  sticksstones1  42134  sticksstones2  42135  aks6d1c6isolem1  42162  resubcan2  42376  diophrw  42747  eldioph2lem1  42748  diophrex  42763  rencldnfi  42809  pellexlem2  42818  pellqrexplicit  42865  infmrgelbi  42866  pellfundglb  42873  pellfund14gap  42875  rmxycomplete  42906  congadd  42955  acongeq  42972  jm2.19  42982  jm2.23  42985  jm2.20nn  42986  jm2.27  42997  jm3.1  43009  lnmepi  43074  lmhmlnmsplit  43076  hbtlem2  43113  dgraa0p  43138  proot1hash  43184  iocunico  43200  iocinico  43201  oasubex  43275  cantnf2  43314  onmcl  43320  omcl2  43322  nadd2rabex  43375  nadd1rabtr  43377  nadd1rabex  43379  fzunt  43444  relexpxpmin  43706  ntrclsk3  44059  grur1cld  44221  ismnu  44250  grumnudlem  44274  ismnushort  44290  rfcnnnub  45030  uzwo4  45047  wessf1ornlem  45179  supxrge  45334  infleinflem2  45367  iccintsng  45521  climsuse  45606  lptre2pt  45638  limcleqr  45642  0ellimcdiv  45647  fnlimfvre  45672  dvnprodlem1  45944  volioc  45970  stoweidlem17  46015  stoweidlem19  46017  stoweidlem20  46018  stoweidlem22  46020  stoweidlem28  46026  stoweidlem34  46032  stoweidlem44  46042  stoweidlem60  46058  wallispilem3  46065  fourierdlem42  46147  fourierdlem48  46152  fourierdlem51  46155  fourierdlem54  46158  fourierdlem74  46178  fourierdlem77  46181  fourierdlem87  46191  fourierdlem97  46201  ioorrnopnlem  46302  ovnsubaddlem2  46569  smfinflem  46815  fsupdm  46840  finfdm  46844  eluzge0nn0  47313  fzopredsuc  47324  imasetpreimafvbijlemfv  47403  lighneallem4  47611  oexpnegALTV  47678  oexpnegnz  47679  tgblthelfgott  47816  clnbgrgrim  47934  isubgr3stgrlem3  47967  rmsupp0  48356  rmsuppss  48358  lincresunit3lem3  48463  lincresunit3lem2  48469  lindssnlvec  48475  fdivmptf  48530  refdivmptf  48531  elbigolo1  48546  rrx2linest  48731  itsclc0lem1  48745  itsclc0lem2  48746  itsclc0yqsollem1  48751  itsclc0b  48761  setc1onsubc  49591