Theorem simpl3 1189

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 485	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2antl3 1183	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpl13  1246  simpl23  1249  simpl33  1252  simp1l3  1264  simp2l3  1270  simp3l3  1276  3anandirs  1468  2nreu  4393  f1prex  7040  fcofo  7044  soisores  7080  weniso  7107  knatar  7110  ofmpteq  7428  funelss  7746  smorndom  8005  nnmord  8258  nnmword  8259  difsnen  8599  mapunen  8686  ac6sfi  8762  fipreima  8830  wemaplem2  9011  wemapso2lem  9016  en2eqpr  9433  indcardi  9467  acndom  9477  fodomfi2  9486  infmap2  9640  cflim2  9685  coftr  9695  infpssrlem4  9728  fin23lem11  9739  fincssdom  9745  isf32lem9  9783  fin1a2lem9  9830  gchpwdom  10092  gruima  10224  prpssnq  10412  distrlem4pr  10448  dedekind  10803  addcan  10824  addcan2  10825  divmulass  11321  supmul1  11610  uzsupss  12341  xaddass  12643  xleadd1a  12647  xlesubadd  12657  xmulasslem3  12680  xmulass  12681  xadddilem  12688  xadddi  12689  ixxun  12755  icoshftf1o  12861  snunioc  12867  difelfzle  13021  fzo1fzo0n0  13089  ssfzoulel  13132  modmuladd  13282  modifeq2int  13302  modaddmulmod  13307  modsubdir  13309  ltexp2a  13531  leexp2  13536  ltexp2r  13538  exple1  13541  expnlbnd2  13596  mulsubdivbinom2  13623  hashtpg  13844  ccatass  13942  ccatopth  14078  pfxccatin12lem2a  14089  pfxccat3  14096  cshinj  14173  2cshw  14175  s2f1o  14278  limsupgre  14838  addcn2  14950  mulcn2  14952  binomrisefac  15396  bpolydif  15409  dvdsmodexp  15615  modmulconst  15641  dvdsmod  15678  sadass  15820  gcdass  15895  rplpwr  15907  rppwr  15908  rpmulgcd2  16000  rpdvds  16004  rpexp  16064  prmdiveq  16123  hashgcdlem  16125  coprimeprodsq  16145  coprimeprodsq2  16146  pythagtriplem3  16155  pcdvdsb  16205  pcgcd1  16213  dvdsprmpweq  16220  pcbc  16236  0ram  16356  ramz2  16360  ramub1lem1  16362  mremre  16875  mrieqv2d  16910  lubun  17733  isnsgrp  17905  issubmnd  17938  gsumccatOLD  18005  frmdss2  18028  submefmnd  18060  sgrp2rid2ex  18092  mulgnn0p1  18239  mulgnnsubcl  18240  mulgneg  18246  mulgdirlem  18258  nmzsubg  18317  ghmmulg  18370  pmtrfv  18580  pmtrmvd  18584  pmtrfb  18593  odmodnn0  18668  oddvdsnn0  18672  odnncl  18673  odmod  18674  oddvds  18675  odeq  18678  odmulgid  18681  odmulg  18683  odmulgeq  18684  odbezout  18685  odf1o1  18697  odf1o2  18698  odngen  18702  odcau  18729  pgpssslw  18739  fislw  18750  lsmless1x  18769  lsmless2x  18770  lsmsubm  18778  lsmmod  18801  lsmmod2  18802  efgsfo  18865  cntzcmn  18960  odadd1  18968  odadd2  18969  odadd  18970  lsmcomx  18976  prdscmnd  18981  gsumconst  19054  ring1eq0  19340  cntzsubr  19568  isabvd  19591  rmodislmod  19702  lspss  19756  0lmhm  19812  reslmhm2  19825  pwssplit0  19830  pwssplit1  19831  lbspss  19854  lspfixed  19900  lsmcv  19913  lspsnat  19917  issubassa  20098  aspss  20106  coe1subfv  20434  coe1tm  20441  xrsdsreclblem  20591  obselocv  20872  frlmsplit2  20917  frlmsslss2  20919  frlmup4  20945  lindff1  20964  lsslindf  20974  lsslinds  20975  islindf4  20982  mpomatmul  21055  mamutpos  21067  submaval  21190  mdetdiag  21208  mdetunilem1  21221  mdetunilem3  21223  mdetunilem9  21229  mdetmul  21232  maducoeval2  21249  madurid  21253  minmar1val  21257  cramer  21300  cpmatel2  21321  m2cpm  21349  decpmatmul  21380  pmatcollpw1lem2  21383  pmatcollpw1  21384  pmatcollpw2lem  21385  pm2mpcl  21405  mply1topmatcl  21413  mp2pm2mplem2  21415  mp2pm2mplem4  21417  pm2mpghmlem2  21420  pm2mpghmlem1  21421  cayhamlem2  21492  neiint  21712  topssnei  21732  cnrest2  21894  cnprest2  21898  cnt0  21954  cnt1  21958  cnhaus  21962  cncmp  22000  fiuncmp  22012  sscmp  22013  hauscmp  22015  cnconn  22030  unconn  22037  comppfsc  22140  kgen2ss  22163  ptpjopn  22220  ptrescn  22247  qtopss  22323  kqfvima  22338  r0cld  22346  cmphaushmeo  22408  fbssint  22446  fbasrn  22492  filuni  22493  ufilmax  22515  fin1aufil  22540  fmf  22553  fmss  22554  rnelfmlem  22560  rnelfm  22561  fmufil  22567  fmco  22569  flimss2  22580  flimss1  22581  flimrest  22591  cnpflf2  22608  cnpflf  22609  flfcnp  22612  lmflf  22613  supnfcls  22628  fclsss1  22630  fclsss2  22631  cnpfcfi  22648  subgntr  22715  opnsubg  22716  cldsubg  22719  ustuqtop1  22850  ucncn  22894  bldisj  23008  blgt0  23009  bl2in  23010  blss2ps  23013  blss2  23014  xbln0  23024  blssps  23034  blss  23035  lpbl  23113  blcld  23115  blcls  23116  stdbdmopn  23128  metcnp2  23152  txmetcnp  23157  blval2  23172  restmetu  23180  nmoix  23338  nmoi2  23339  nmoeq0  23345  nmotri  23348  metdsge  23457  metds0  23458  metdseq0  23462  icoopnst  23543  iccpnfhmeo  23549  xrhmeo  23550  nmhmcn  23724  cphsqrtcl2  23790  cphsqrtcl3  23791  fmcfil  23875  bcthlem5  23931  cmetcusp1  23956  cssbn  23978  pjth  24042  ovolunnul  24101  volun  24146  voliunlem2  24152  itg2const  24341  iblconst  24418  itgconst  24419  limcvallem  24469  dvcnp2  24517  dvcn  24518  deg1mul3le  24710  deg1tmle  24711  ig1pdvds  24770  coe11  24843  dgrmulc  24861  dvply1  24873  aaliou2  24929  efcvx  25037  tanord  25122  logdivlti  25203  logccv  25246  recxpcl  25258  cxplea  25279  cxple2a  25282  ang180  25392  isosctrlem2  25397  cxp2lim  25554  amgm  25568  muval1  25710  dvdssqf  25715  mumullem2  25757  bcmono  25853  lgsneg  25897  lgsmod  25899  lgsdirprm  25907  lgsdir  25908  lgsdi  25910  brbtwn2  26691  colinearalglem1  26692  colinearalg  26696  axcgrtr  26701  axcontlem2  26751  upgrewlkle2  27388  wlksoneq1eq2  27446  crctcshwlkn0lem5  27592  wspthsnwspthsnon  27695  lppthon  27930  upgriseupth  27986  4cyclusnfrgr  28071  numclwwlk1lem2foa  28133  numclwwlk5  28167  nvmul0or  28427  shless  29136  shlej1  29137  pjspansn  29354  kbmul  29732  homco2  29754  kbass2  29894  fnpreimac  30416  padct  30455  eliccelico  30500  elicoelioo  30501  iocinioc2  30502  difioo  30505  swrdrn2  30628  swrdrn3  30629  xrge0npcan  30681  isarchi2  30814  archiabl  30827  lindssn  30939  ssmxidl  30979  mdetlap1  31091  pstmfval  31136  fmcncfil  31174  zrhnm  31210  qqhnm  31231  nexple  31268  volfiniune  31489  omsmeas  31581  eulerpartlemb  31626  probinc  31679  cndprob01  31693  signswmnd  31827  cvmsss2  32521  dvdspw  32982  funsseq  33011  frpomin  33078  frrlem10  33132  fprlem1  33137  sltres  33169  nolt02olem  33198  nolt02o  33199  nosupbnd1lem1  33208  nosupbnd1lem4  33211  nosupbnd1lem5  33212  nosupbnd1lem6  33213  cgrtriv  33463  5segofs  33467  btwntriv2  33473  btwnxfr  33517  segcon2  33566  brsegle2  33570  seglelin  33577  outsideofeu  33592  lindsenlbs  34902  mblfinlem2  34945  blbnd  35080  rrndstprj2  35124  zerdivemp1x  35240  lsmsat  36159  lsatfixedN  36160  lssat  36167  lkrlsp  36253  lshpkrlem4  36264  cvrcon3b  36428  leat3  36446  atlen0  36461  atnle  36468  atlatmstc  36470  atlatle  36471  cvlcvr1  36490  cvlsupr2  36494  hlsupr2  36538  hlrelat2  36554  cvrexchlem  36570  cvratlem  36572  lnnat  36578  atexchcvrN  36591  1cvratlt  36625  1cvrjat  36626  3atlem3  36636  3atlem7  36640  llni2  36663  atcvrlln2  36670  llnexatN  36672  llncmp  36673  2llnmat  36675  2at0mat0  36676  2atnelpln  36695  llncvrlpln2  36708  2lplnmN  36710  2llnmj  36711  lplncmp  36713  lplnexatN  36714  2llnjaN  36717  lvoli3  36728  islvol2aN  36743  4atlem3a  36748  4atlem4a  36750  4atlem4b  36751  4atlem11  36760  4atlem12  36763  lplncvrlvol2  36766  lvolcmp  36768  2lplnmj  36773  islinei  36891  linepmap  36926  lneq2at  36929  2llnma3r  36939  elpaddn0  36951  elpaddatriN  36954  elpaddat  36955  paddcom  36964  paddss1  36968  paddss2  36969  paddasslem6  36976  paddasslem7  36977  paddasslem10  36980  paddasslem15  36985  pmodlem2  36998  pmodl42N  37002  pmapjoin  37003  atmod1i1m  37009  llnmod1i2  37011  llnexchb2lem  37019  polcon2bN  37071  pclfinclN  37101  poml4N  37104  poml6N  37106  osumcllem11N  37117  osumclN  37118  pmapojoinN  37119  pexmidlem2N  37122  pexmidlem3N  37123  pexmidlem4N  37124  pexmidlem6N  37126  pexmidlem7N  37127  pl42lem2N  37131  pl42lem3N  37132  pl42lem4N  37133  pl42N  37134  lhpexle3lem  37162  lhpmcvr3  37176  lhp2at0nle  37186  lhprelat3N  37191  lauteq  37246  lautco  37248  ltrncoidN  37279  ltrneq2  37299  ltrnnidn  37325  ltrnideq  37326  trlnle  37337  cdlemc  37348  cdlemd4  37352  cdlemd5  37353  cdlemd9  37357  cdlemd  37358  ltrneq3  37359  cdlemefrs29pre00  37546  cdlemefrs29cpre1  37549  cdlemefrs29clN  37550  cdlemefrs32fva  37551  cdlemefr29exN  37553  cdlemefr27cl  37554  cdlemefs27cl  37564  cdlemefs32sn1aw  37565  cdleme32fva  37588  cdleme32d  37595  cdleme32f  37597  cdleme32le  37598  cdleme40n  37619  cdleme41snaw  37627  cdleme17d3  37647  cdleme48fvg  37651  cdlemeg46fvcl  37657  cdlemeg46fgN  37685  cdleme48fgv  37689  ltrniotavalbN  37735  cdlemb3  37757  cdlemg15  37807  cdlemg17dN  37814  trlco  37878  cdlemg44b  37883  ltrncom  37889  trljco  37891  tendococl  37923  tendoplcl  37932  tendoplcom  37933  tendotr  37981  cdlemk36  38064  cdlemk35s-id  38089  cdlemk39s-id  38091  cdlemk19x  38094  cdlemk53b  38107  cdlemk55  38112  cdlemk35u  38115  cdlemk55u  38117  cdlemk39u  38119  cdlemk19u  38121  cdlemk56  38122  tendoex  38126  cdleml5N  38131  dihord2pre  38376  dihord6apre  38407  dihord5b  38410  dihord5apre  38413  dihord  38415  dihmeetlem1N  38441  dihmeetlem2N  38450  dihglbcpreN  38451  dihmeetbN  38454  dihmeetlem4preN  38457  dihmeetlem5  38459  dihmeetlem6  38460  dihmeetlem7N  38461  dihmeetlem10N  38467  dihmeetlem11N  38468  dihmeetlem12N  38469  dihmeetlem13N  38470  dihmeetlem15N  38472  dihmeetlem17N  38474  dihmeetlem18N  38475  dihmeetlem19N  38476  dihmeetALTN  38478  dih1dimatlem0  38479  dihlspsnssN  38483  dvh3dim2  38599  resubcan2  39267  mzpsubst  39394  diophrw  39405  eldioph2lem1  39406  rencldnfi  39467  pellexlem2  39476  pellqrexplicit  39523  infmrgelbi  39524  rmxycomplete  39563  congadd  39612  acongeq  39629  jm2.19  39639  jm2.22  39641  jm2.20nn  39643  jm2.25lem1  39644  jm2.27  39654  jm3.1  39666  lmhmlnmsplit  39736  pwssplit4  39738  hbtlem2  39773  dgraa0p  39798  idomrootle  39844  proot1hash  39849  iocunico  39866  relexpxpmin  40111  brtrclfv2  40121  ntrclsk3  40469  grur1cld  40617  ismnu  40646  suprnmpt  41479  wessf1ornlem  41494  choicefi  41512  supxrgere  41650  supxrgelem  41654  supxrge  41655  infleinflem2  41688  snunioo1  41837  iccintsng  41848  fmul01  41910  lptre2pt  41970  0ellimcdiv  41979  fnlimfvre  42004  limsupmnfuzlem  42056  climisp  42076  limsupgtlem  42107  ibliccsinexp  42285  iblioosinexp  42287  volioc  42306  iblspltprt  42307  stoweidlem20  42354  stoweidlem22  42356  stoweidlem34  42368  stoweidlem44  42378  stoweidlem60  42394  wallispilem3  42401  fourierdlem42  42483  fourierdlem51  42491  fourierdlem54  42494  fourierdlem87  42527  fourierdlem97  42537  ioorrnopnlem  42638  sge0seq  42777  hoicvr  42879  imasetpreimafvbijlemfv  43611  lincresunit3lem3  44578  lindssnlvec  44590  rrx2linesl  44779  line2  44788  itsclc0lem3  44794  itsclc0yqsollem1  44798  itscnhlc0xyqsol  44801  itschlc0xyqsol1  44802  itsclc0  44807  itscnhlinecirc02plem2  44819  itscnhlinecirc02plem3  44820