Theorem simpl3 1210

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl3	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simpl3

Step	Hyp	Ref	Expression
1		simpl 487	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2antl3 1204	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simpl13  1267  simpl23  1270  simpl33  1273  simp1l3  1285  simp2l3  1291  simp3l3  1297  3anandirs  1496  2nreu  4401  predtrss  6312  frpomin  6330  f1prex  7272  fcofo  7276  soisores  7315  weniso  7342  knatar  7345  ofmpteq  7687  funelss  8032  frrlem10  8280  fprlem1  8285  smocdmdom  8343  nnmord  8606  nnmword  8607  naddasslem1  8669  naddasslem2  8670  difsnen  9035  mapunen  9122  ac6sfi  9232  fipreima  9303  wemaplem2  9497  wemapso2lem  9502  ttrclselem2  9683  en2eqpr  9979  indcardi  10013  acndom  10023  fodomfi2  10032  infmap2  10188  cflim2  10235  coftr  10245  infpssrlem4  10278  fin23lem11  10289  fincssdom  10295  isf32lem9  10333  fin1a2lem9  10380  gchpwdom  10643  gruima  10775  prpssnq  10963  distrlem4pr  10999  dedekind  11361  addcan  11382  addcan2  11383  divmulass  11883  supmul1  12172  uzsupss  12952  xaddass  13263  xleadd1a  13267  xlesubadd  13277  xmulasslem3  13300  xmulass  13301  xadddilem  13308  xadddi  13309  ixxun  13376  icoshftf1o  13489  snunioc  13495  difelfzle  13657  fzo1fzo0n0  13732  ssfzoulel  13777  modmuladd  13937  modifeq2int  13957  modaddmulmod  13962  modsubdir  13964  ltexp2a  14190  leexp2  14195  ltexp2r  14197  exple1  14201  expnlbnd2  14258  mulsubdivbinom2  14286  hashtpg  14510  ccatass  14614  ccatopth  14741  pfxccatin12lem2a  14752  pfxccat3  14759  cshinj  14836  2cshw  14838  s2f1o  14941  limsupgre  15520  addcn2  15633  mulcn2  15635  binomrisefac  16084  bpolydif  16097  dvdsmodexp  16306  modmulconst  16334  dvdsexp2im  16373  dvdsmod  16375  sadass  16517  gcdass  16593  rplpwr  16604  rpmulgcd2  16702  rpdvds  16706  rpexp  16769  prmdiveq  16833  hashgcdlem  16835  coprimeprodsq  16856  coprimeprodsq2  16857  pythagtriplem3  16866  pcdvdsb  16917  pcgcd1  16925  dvdsprmpweq  16932  pcbc  16948  0ram  17068  ramz2  17072  ramub1lem1  17074  mremre  17644  mrieqv2d  17683  lubun  18559  isnsgrp  18769  issubmnd  18807  frmdss2  18910  submefmnd  18942  sgrp2rid2ex  18977  mulgnn0p1  19139  mulgnnsubcl  19140  mulgneg  19146  mulgdirlem  19159  nmzsubg  19219  ghmmulg  19286  pmtrfv  19510  pmtrmvd  19514  pmtrfb  19523  odmodnn0  19598  oddvdsnn0  19602  odnncl  19603  odmod  19604  oddvds  19605  odeq  19608  odmulgid  19612  odmulg  19614  odmulgeq  19615  odbezout  19616  odf1o1  19630  odf1o2  19631  odngen  19635  odcau  19662  pgpssslw  19672  fislw  19683  lsmless1x  19702  lsmless2x  19703  lsmsubm  19711  lsmmod  19733  lsmmod2  19734  efgsfo  19797  cntzcmn  19898  odadd1  19906  odadd2  19907  odadd  19908  lsmcomx  19914  prdscmnd  19919  gsumconst  19992  ring1eq0  20369  cntzsubrng  20640  cntzsubr  20679  isabvd  20881  rmodislmod  21017  lspss  21071  0lmhm  21127  reslmhm2  21140  pwssplit0  21145  pwssplit1  21146  lbspss  21169  lspfixed  21218  lsmcv  21231  lspsnat  21235  2idlcpblrng  21369  cnfldfunALT  21494  xrsdsreclblem  21520  obselocv  21835  frlmsplit2  21880  frlmsslss2  21882  frlmup4  21908  lindff1  21927  lsslindf  21937  lsslinds  21938  islindf4  21945  issubassa  21974  aspss  21983  coe1subfv  22384  coe1tm  22391  mpomatmul  22560  mamutpos  22572  submaval  22695  mdetdiag  22713  mdetunilem1  22726  mdetunilem3  22728  mdetunilem9  22734  mdetmul  22737  maducoeval2  22754  madurid  22758  minmar1val  22762  cramer  22805  cpmatel2  22827  m2cpm  22855  decpmatmul  22886  pmatcollpw1lem2  22889  pmatcollpw1  22890  pmatcollpw2lem  22891  pm2mpcl  22911  mply1topmatcl  22919  mp2pm2mplem2  22921  mp2pm2mplem4  22923  pm2mpghmlem2  22926  pm2mpghmlem1  22927  cayhamlem2  22998  neiint  23218  topssnei  23238  cnrest2  23400  cnprest2  23404  cnt0  23460  cnt1  23464  cnhaus  23468  cncmp  23506  fiuncmp  23518  sscmp  23519  hauscmp  23521  cnconn  23536  unconn  23543  comppfsc  23646  kgen2ss  23669  ptpjopn  23726  ptrescn  23753  qtopss  23829  kqfvima  23844  r0cld  23852  cmphaushmeo  23914  fbssint  23952  fbasrn  23998  filuni  23999  ufilmax  24021  fin1aufil  24046  fmf  24059  fmss  24060  rnelfmlem  24066  rnelfm  24067  fmufil  24073  fmco  24075  flimss2  24086  flimss1  24087  flimrest  24097  cnpflf2  24114  cnpflf  24115  flfcnp  24118  lmflf  24119  supnfcls  24134  fclsss1  24136  fclsss2  24137  cnpfcfi  24154  subgntr  24221  opnsubg  24222  cldsubg  24225  ustuqtop1  24355  ucncn  24398  bldisj  24512  blgt0  24513  bl2in  24514  blss2ps  24517  blss2  24518  xbln0  24528  blssps  24538  blss  24539  lpbl  24617  blcld  24619  blcls  24620  stdbdmopn  24632  metcnp2  24656  txmetcnp  24661  blval2  24676  restmetu  24684  nmoix  24843  nmoi2  24844  nmoeq0  24850  nmotri  24853  metdsge  24964  metds0  24965  metdseq0  24969  icoopnst  25055  iccpnfhmeo  25061  xrhmeo  25062  nmhmcn  25236  cphsqrtcl2  25302  cphsqrtcl3  25303  fmcfil  25388  bcthlem5  25444  cmetcusp1  25469  cssbn  25491  pjth  25555  ovolunnul  25616  volun  25661  voliunlem2  25667  itg2const  25856  iblconst  25934  itgconst  25935  limcvallem  25987  dvcnp2  26036  dvcn  26037  deg1mul3le  26231  deg1tmle  26232  idomrootle  26287  ig1pdvds  26294  coe11  26367  dgrmulc  26385  dvply1  26402  aaliou2  26458  efcvx  26566  tanord  26657  logdivlti  26739  logccv  26782  recxpcl  26794  cxplea  26815  cxple2a  26818  ang180  26933  isosctrlem2  26938  cxp2lim  27095  amgm  27109  muval1  27251  dvdssqf  27256  mumullem2  27298  bcmono  27395  lgsneg  27439  lgsmod  27441  lgsdirprm  27449  lgsdir  27450  lgsdi  27452  ltsres  27780  nolt02olem  27812  nolt02o  27813  nogt01o  27814  nosupbnd1lem1  27826  nosupbnd1lem4  27829  nosupbnd1lem5  27830  nosupbnd1lem6  27831  noinfbnd1lem1  27841  noinfbnd1lem4  27844  noinfbnd1lem6  27846  noinfbnd2  27849  noetainflem3  27857  ltslpss  28055  cofslts  28065  coinitslts  28066  cofcutrtime  28074  addsass  28152  addsdi  28302  mulsass  28313  ltmuls2  28318  norecdiv  28337  z12bdaylem  28631  brbtwn2  29160  colinearalglem1  29161  colinearalg  29165  axcgrtr  29170  axcontlem2  29220  upgrewlkle2  29861  wlksoneq1eq2  29917  crctcshwlkn0lem5  30068  wspthsnwspthsnon  30170  lppthon  30407  upgriseupth  30463  4cyclusnfrgr  30548  numclwwlk1lem2foa  30610  numclwwlk5  30644  nvmul0or  30907  shless  31616  shlej1  31617  pjspansn  31834  kbmul  32212  homco2  32234  kbass2  32374  fnpreimac  32923  padct  32971  eliccelico  33030  elicoelioo  33031  iocinioc2  33032  difioo  33035  nexple  33085  swrdrn2  33182  swrdrn3  33183  xrge0npcan  33248  isarchi2  33413  archiabl  33426  pidlnz  33600  lindssn  33602  ssmxidl  33669  mdetlap1  34128  zarclsiin  34173  pstmfval  34198  fmcncfil  34233  zrhnm  34269  qqhnm  34292  volfiniune  34532  omsmeas  34625  eulerpartlemb  34670  probinc  34723  cndprob01  34737  signswmnd  34856  cvmsss2  35632  funsseq  36126  cgrtriv  36360  5segofs  36364  btwntriv2  36370  btwnxfr  36414  segcon2  36463  brsegle2  36467  seglelin  36474  outsideofeu  36489  weiunpo  36833  weiunfr  36835  weiunse  36836  lindsenlbs  38121  mblfinlem2  38164  blbnd  38293  rrndstprj2  38337  zerdivemp1x  38453  lsmsat  39639  lsatfixedN  39640  lssat  39647  lkrlsp  39733  lshpkrlem4  39744  cvrcon3b  39908  leat3  39926  atlen0  39941  atnle  39948  atlatmstc  39950  atlatle  39951  cvlcvr1  39970  cvlsupr2  39974  hlsupr2  40018  hlrelat2  40034  cvrexchlem  40050  cvratlem  40052  lnnat  40058  atexchcvrN  40071  1cvratlt  40105  1cvrjat  40106  3atlem3  40116  3atlem7  40120  llni2  40143  atcvrlln2  40150  llnexatN  40152  llncmp  40153  2llnmat  40155  2at0mat0  40156  2atnelpln  40175  llncvrlpln2  40188  2lplnmN  40190  2llnmj  40191  lplncmp  40193  lplnexatN  40194  2llnjaN  40197  lvoli3  40208  islvol2aN  40223  4atlem3a  40228  4atlem4a  40230  4atlem4b  40231  4atlem11  40240  4atlem12  40243  lplncvrlvol2  40246  lvolcmp  40248  2lplnmj  40253  islinei  40371  linepmap  40406  lneq2at  40409  2llnma3r  40419  elpaddn0  40431  elpaddatriN  40434  elpaddat  40435  paddcom  40444  paddss1  40448  paddss2  40449  paddasslem6  40456  paddasslem7  40457  paddasslem10  40460  paddasslem15  40465  pmodlem2  40478  pmodl42N  40482  pmapjoin  40483  atmod1i1m  40489  llnmod1i2  40491  llnexchb2lem  40499  polcon2bN  40551  pclfinclN  40581  poml4N  40584  poml6N  40586  osumcllem11N  40597  osumclN  40598  pmapojoinN  40599  pexmidlem2N  40602  pexmidlem3N  40603  pexmidlem4N  40604  pexmidlem6N  40606  pexmidlem7N  40607  pl42lem2N  40611  pl42lem3N  40612  pl42lem4N  40613  pl42N  40614  lhpexle3lem  40642  lhpmcvr3  40656  lhp2at0nle  40666  lhprelat3N  40671  lauteq  40726  lautco  40728  ltrncoidN  40759  ltrneq2  40779  ltrnnidn  40805  ltrnideq  40806  trlnle  40817  cdlemc  40828  cdlemd4  40832  cdlemd5  40833  cdlemd9  40837  cdlemd  40838  ltrneq3  40839  cdlemefrs29pre00  41026  cdlemefrs29cpre1  41029  cdlemefrs29clN  41030  cdlemefrs32fva  41031  cdlemefr29exN  41033  cdlemefr27cl  41034  cdlemefs27cl  41044  cdlemefs32sn1aw  41045  cdleme32fva  41068  cdleme32d  41075  cdleme32f  41077  cdleme32le  41078  cdleme40n  41099  cdleme41snaw  41107  cdleme17d3  41127  cdleme48fvg  41131  cdlemeg46fvcl  41137  cdlemeg46fgN  41165  cdleme48fgv  41169  ltrniotavalbN  41215  cdlemb3  41237  cdlemg15  41287  cdlemg17dN  41294  trlco  41358  cdlemg44b  41363  ltrncom  41369  trljco  41371  tendococl  41403  tendoplcl  41412  tendoplcom  41413  tendotr  41461  cdlemk36  41544  cdlemk35s-id  41569  cdlemk39s-id  41571  cdlemk19x  41574  cdlemk53b  41587  cdlemk55  41592  cdlemk35u  41595  cdlemk55u  41597  cdlemk39u  41599  cdlemk19u  41601  cdlemk56  41602  tendoex  41606  cdleml5N  41611  dihord2pre  41856  dihord6apre  41887  dihord5b  41890  dihord5apre  41893  dihord  41895  dihmeetlem1N  41921  dihmeetlem2N  41930  dihglbcpreN  41931  dihmeetbN  41934  dihmeetlem4preN  41937  dihmeetlem5  41939  dihmeetlem6  41940  dihmeetlem7N  41941  dihmeetlem10N  41947  dihmeetlem11N  41948  dihmeetlem12N  41949  dihmeetlem13N  41950  dihmeetlem15N  41952  dihmeetlem17N  41954  dihmeetlem18N  41955  dihmeetlem19N  41956  dihmeetALTN  41958  dih1dimatlem0  41959  dihlspsnssN  41963  dvh3dim2  42079  sticksstones1  42770  sticksstones2  42771  sticksstones12  42782  aks6d1c6isolem1  42798  dvdsexpnn  42949  resubcan2  43004  mzpsubst  43336  diophrw  43347  eldioph2lem1  43348  rencldnfi  43405  pellexlem2  43414  pellqrexplicit  43461  infmrgelbi  43462  rmxycomplete  43501  congadd  43550  acongeq  43567  jm2.19  43577  jm2.22  43579  jm2.20nn  43581  jm2.25lem1  43582  jm2.27  43592  jm3.1  43604  lmhmlnmsplit  43671  pwssplit4  43673  hbtlem2  43708  dgraa0p  43733  proot1hash  43779  iocunico  43795  cantnf2  43909  dflim5  43913  omcl2  43917  tfsconcatrn  43926  nadd2rabex  43970  relexpxpmin  44300  brtrclfv2  44310  ntrclsk3  44653  grur1cld  44815  ismnu  44830  suprnmpt  45751  wessf1ornlem  45762  choicefi  45776  supxrgere  45908  supxrgelem  45912  supxrge  45913  infleinflem2  45945  snunioo1  46087  iccintsng  46098  fmul01  46155  lptre2pt  46213  0ellimcdiv  46222  fnlimfvre  46247  limsupmnfuzlem  46299  climisp  46319  limsupgtlem  46350  ibliccsinexp  46524  iblioosinexp  46526  volioc  46545  iblspltprt  46546  stoweidlem20  46593  stoweidlem22  46595  stoweidlem34  46607  stoweidlem44  46617  stoweidlem60  46633  wallispilem3  46640  fourierdlem42  46722  fourierdlem51  46730  fourierdlem54  46733  fourierdlem87  46766  fourierdlem97  46776  ioorrnopnlem  46877  sge0seq  47019  hoicvr  47121  fsupdm  47415  finfdm  47419  3f1oss1  47668  funfocofob  47671  imasetpreimafvbijlemfv  48007  uhgrimisgrgric  48552  uhgrimgrlim  48608  fprmappr  48977  lincresunit3lem3  49106  lindssnlvec  49118  rrx2linesl  49375  line2  49384  itsclc0lem3  49390  itsclc0yqsollem1  49394  itscnhlc0xyqsol  49397  itschlc0xyqsol1  49398  itsclc0  49403  itscnhlinecirc02plem2  49415  itscnhlinecirc02plem3  49416  uptrlem1  49840  uptr2  49851  setc1onsubc  50232