Theorem simpl3 1194

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 482	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2antl3 1188	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:  simpl13  1251  simpl23  1254  simpl33  1257  simp1l3  1269  simp2l3  1275  simp3l3  1281  3anandirs  1474  2nreu  4397  predtrss  6274  frpomin  6292  f1prex  7225  fcofo  7229  soisores  7268  weniso  7295  knatar  7298  ofmpteq  7640  funelss  7989  frrlem10  8235  fprlem1  8240  smocdmdom  8298  nnmord  8557  nnmword  8558  naddasslem1  8619  naddasslem2  8620  difsnen  8983  mapunen  9070  ac6sfi  9189  fipreima  9267  wemaplem2  9458  wemapso2lem  9463  ttrclselem2  9641  en2eqpr  9920  indcardi  9954  acndom  9964  fodomfi2  9973  infmap2  10130  cflim2  10176  coftr  10186  infpssrlem4  10219  fin23lem11  10230  fincssdom  10236  isf32lem9  10274  fin1a2lem9  10321  gchpwdom  10583  gruima  10715  prpssnq  10903  distrlem4pr  10939  dedekind  11297  addcan  11318  addcan2  11319  divmulass  11820  supmul1  12112  uzsupss  12859  xaddass  13169  xleadd1a  13173  xlesubadd  13183  xmulasslem3  13206  xmulass  13207  xadddilem  13214  xadddi  13215  ixxun  13282  icoshftf1o  13395  snunioc  13401  difelfzle  13562  fzo1fzo0n0  13636  ssfzoulel  13681  modmuladd  13838  modifeq2int  13858  modaddmulmod  13863  modsubdir  13865  ltexp2a  14091  leexp2  14096  ltexp2r  14098  exple1  14102  expnlbnd2  14159  mulsubdivbinom2  14187  hashtpg  14410  ccatass  14513  ccatopth  14640  pfxccatin12lem2a  14651  pfxccat3  14658  cshinj  14735  2cshw  14737  s2f1o  14841  limsupgre  15406  addcn2  15519  mulcn2  15521  binomrisefac  15967  bpolydif  15980  dvdsmodexp  16189  modmulconst  16217  dvdsexp2im  16256  dvdsmod  16258  sadass  16400  gcdass  16476  rplpwr  16487  rpmulgcd2  16585  rpdvds  16589  rpexp  16651  prmdiveq  16715  hashgcdlem  16717  coprimeprodsq  16738  coprimeprodsq2  16739  pythagtriplem3  16748  pcdvdsb  16799  pcgcd1  16807  dvdsprmpweq  16814  pcbc  16830  0ram  16950  ramz2  16954  ramub1lem1  16956  mremre  17524  mrieqv2d  17563  lubun  18439  isnsgrp  18615  issubmnd  18653  frmdss2  18755  submefmnd  18787  sgrp2rid2ex  18819  mulgnn0p1  18982  mulgnnsubcl  18983  mulgneg  18989  mulgdirlem  19002  nmzsubg  19062  ghmmulg  19125  pmtrfv  19349  pmtrmvd  19353  pmtrfb  19362  odmodnn0  19437  oddvdsnn0  19441  odnncl  19442  odmod  19443  oddvds  19444  odeq  19447  odmulgid  19451  odmulg  19453  odmulgeq  19454  odbezout  19455  odf1o1  19469  odf1o2  19470  odngen  19474  odcau  19501  pgpssslw  19511  fislw  19522  lsmless1x  19541  lsmless2x  19542  lsmsubm  19550  lsmmod  19572  lsmmod2  19573  efgsfo  19636  cntzcmn  19737  odadd1  19745  odadd2  19746  odadd  19747  lsmcomx  19753  prdscmnd  19758  gsumconst  19831  ring1eq0  20201  cntzsubrng  20470  cntzsubr  20509  isabvd  20715  rmodislmod  20851  lspss  20905  0lmhm  20962  reslmhm2  20975  pwssplit0  20980  pwssplit1  20981  lbspss  21004  lspfixed  21053  lsmcv  21066  lspsnat  21070  2idlcpblrng  21196  cnfldfunALT  21294  cnfldfunALTOLD  21307  xrsdsreclblem  21337  obselocv  21653  frlmsplit2  21698  frlmsslss2  21700  frlmup4  21726  lindff1  21745  lsslindf  21755  lsslinds  21756  islindf4  21763  issubassa  21792  aspss  21802  coe1subfv  22168  coe1tm  22175  mpomatmul  22349  mamutpos  22361  submaval  22484  mdetdiag  22502  mdetunilem1  22515  mdetunilem3  22517  mdetunilem9  22523  mdetmul  22526  maducoeval2  22543  madurid  22547  minmar1val  22551  cramer  22594  cpmatel2  22616  m2cpm  22644  decpmatmul  22675  pmatcollpw1lem2  22678  pmatcollpw1  22679  pmatcollpw2lem  22680  pm2mpcl  22700  mply1topmatcl  22708  mp2pm2mplem2  22710  mp2pm2mplem4  22712  pm2mpghmlem2  22715  pm2mpghmlem1  22716  cayhamlem2  22787  neiint  23007  topssnei  23027  cnrest2  23189  cnprest2  23193  cnt0  23249  cnt1  23253  cnhaus  23257  cncmp  23295  fiuncmp  23307  sscmp  23308  hauscmp  23310  cnconn  23325  unconn  23332  comppfsc  23435  kgen2ss  23458  ptpjopn  23515  ptrescn  23542  qtopss  23618  kqfvima  23633  r0cld  23641  cmphaushmeo  23703  fbssint  23741  fbasrn  23787  filuni  23788  ufilmax  23810  fin1aufil  23835  fmf  23848  fmss  23849  rnelfmlem  23855  rnelfm  23856  fmufil  23862  fmco  23864  flimss2  23875  flimss1  23876  flimrest  23886  cnpflf2  23903  cnpflf  23904  flfcnp  23907  lmflf  23908  supnfcls  23923  fclsss1  23925  fclsss2  23926  cnpfcfi  23943  subgntr  24010  opnsubg  24011  cldsubg  24014  ustuqtop1  24145  ucncn  24188  bldisj  24302  blgt0  24303  bl2in  24304  blss2ps  24307  blss2  24308  xbln0  24318  blssps  24328  blss  24329  lpbl  24407  blcld  24409  blcls  24410  stdbdmopn  24422  metcnp2  24446  txmetcnp  24451  blval2  24466  restmetu  24474  nmoix  24633  nmoi2  24634  nmoeq0  24640  nmotri  24643  metdsge  24754  metds0  24755  metdseq0  24759  icoopnst  24852  iccpnfhmeo  24859  xrhmeo  24860  nmhmcn  25036  cphsqrtcl2  25102  cphsqrtcl3  25103  fmcfil  25188  bcthlem5  25244  cmetcusp1  25269  cssbn  25291  pjth  25355  ovolunnul  25417  volun  25462  voliunlem2  25468  itg2const  25657  iblconst  25735  itgconst  25736  limcvallem  25788  dvcnp2  25837  dvcnp2OLD  25838  dvcn  25839  deg1mul3le  26038  deg1tmle  26039  idomrootle  26094  ig1pdvds  26101  coe11  26174  dgrmulc  26193  dvply1  26207  aaliou2  26264  efcvx  26375  tanord  26463  logdivlti  26545  logccv  26588  recxpcl  26600  cxplea  26621  cxple2a  26624  ang180  26740  isosctrlem2  26745  cxp2lim  26903  amgm  26917  muval1  27059  dvdssqf  27064  mumullem2  27106  bcmono  27204  lgsneg  27248  lgsmod  27250  lgsdirprm  27258  lgsdir  27259  lgsdi  27261  sltres  27590  nolt02olem  27622  nolt02o  27623  nogt01o  27624  nosupbnd1lem1  27636  nosupbnd1lem4  27639  nosupbnd1lem5  27640  nosupbnd1lem6  27641  noinfbnd1lem1  27651  noinfbnd1lem4  27654  noinfbnd1lem6  27656  noinfbnd2  27659  noetainflem3  27667  sltlpss  27840  cofsslt  27849  coinitsslt  27850  cofcutrtime  27858  addsass  27935  addsdi  28081  mulsass  28092  sltmul2  28097  norecdiv  28116  brbtwn2  28868  colinearalglem1  28869  colinearalg  28873  axcgrtr  28878  axcontlem2  28928  upgrewlkle2  29570  wlksoneq1eq2  29626  crctcshwlkn0lem5  29777  wspthsnwspthsnon  29879  lppthon  30113  upgriseupth  30169  4cyclusnfrgr  30254  numclwwlk1lem2foa  30316  numclwwlk5  30350  nvmul0or  30612  shless  31321  shlej1  31322  pjspansn  31539  kbmul  31917  homco2  31939  kbass2  32079  fnpreimac  32628  padct  32676  eliccelico  32733  elicoelioo  32734  iocinioc2  32735  difioo  32738  nexple  32802  swrdrn2  32909  swrdrn3  32910  xrge0npcan  32987  isarchi2  33137  archiabl  33150  pidlnz  33323  lindssn  33325  ssmxidl  33421  mdetlap1  33792  zarclsiin  33837  pstmfval  33862  fmcncfil  33897  zrhnm  33933  qqhnm  33956  volfiniune  34196  omsmeas  34290  eulerpartlemb  34335  probinc  34388  cndprob01  34402  signswmnd  34524  cvmsss2  35246  funsseq  35740  cgrtriv  35975  5segofs  35979  btwntriv2  35985  btwnxfr  36029  segcon2  36078  brsegle2  36082  seglelin  36089  outsideofeu  36104  weiunpo  36438  weiunfr  36440  weiunse  36441  lindsenlbs  37594  mblfinlem2  37637  blbnd  37766  rrndstprj2  37810  zerdivemp1x  37926  lsmsat  38986  lsatfixedN  38987  lssat  38994  lkrlsp  39080  lshpkrlem4  39091  cvrcon3b  39255  leat3  39273  atlen0  39288  atnle  39295  atlatmstc  39297  atlatle  39298  cvlcvr1  39317  cvlsupr2  39321  hlsupr2  39366  hlrelat2  39382  cvrexchlem  39398  cvratlem  39400  lnnat  39406  atexchcvrN  39419  1cvratlt  39453  1cvrjat  39454  3atlem3  39464  3atlem7  39468  llni2  39491  atcvrlln2  39498  llnexatN  39500  llncmp  39501  2llnmat  39503  2at0mat0  39504  2atnelpln  39523  llncvrlpln2  39536  2lplnmN  39538  2llnmj  39539  lplncmp  39541  lplnexatN  39542  2llnjaN  39545  lvoli3  39556  islvol2aN  39571  4atlem3a  39576  4atlem4a  39578  4atlem4b  39579  4atlem11  39588  4atlem12  39591  lplncvrlvol2  39594  lvolcmp  39596  2lplnmj  39601  islinei  39719  linepmap  39754  lneq2at  39757  2llnma3r  39767  elpaddn0  39779  elpaddatriN  39782  elpaddat  39783  paddcom  39792  paddss1  39796  paddss2  39797  paddasslem6  39804  paddasslem7  39805  paddasslem10  39808  paddasslem15  39813  pmodlem2  39826  pmodl42N  39830  pmapjoin  39831  atmod1i1m  39837  llnmod1i2  39839  llnexchb2lem  39847  polcon2bN  39899  pclfinclN  39929  poml4N  39932  poml6N  39934  osumcllem11N  39945  osumclN  39946  pmapojoinN  39947  pexmidlem2N  39950  pexmidlem3N  39951  pexmidlem4N  39952  pexmidlem6N  39954  pexmidlem7N  39955  pl42lem2N  39959  pl42lem3N  39960  pl42lem4N  39961  pl42N  39962  lhpexle3lem  39990  lhpmcvr3  40004  lhp2at0nle  40014  lhprelat3N  40019  lauteq  40074  lautco  40076  ltrncoidN  40107  ltrneq2  40127  ltrnnidn  40153  ltrnideq  40154  trlnle  40165  cdlemc  40176  cdlemd4  40180  cdlemd5  40181  cdlemd9  40185  cdlemd  40186  ltrneq3  40187  cdlemefrs29pre00  40374  cdlemefrs29cpre1  40377  cdlemefrs29clN  40378  cdlemefrs32fva  40379  cdlemefr29exN  40381  cdlemefr27cl  40382  cdlemefs27cl  40392  cdlemefs32sn1aw  40393  cdleme32fva  40416  cdleme32d  40423  cdleme32f  40425  cdleme32le  40426  cdleme40n  40447  cdleme41snaw  40455  cdleme17d3  40475  cdleme48fvg  40479  cdlemeg46fvcl  40485  cdlemeg46fgN  40513  cdleme48fgv  40517  ltrniotavalbN  40563  cdlemb3  40585  cdlemg15  40635  cdlemg17dN  40642  trlco  40706  cdlemg44b  40711  ltrncom  40717  trljco  40719  tendococl  40751  tendoplcl  40760  tendoplcom  40761  tendotr  40809  cdlemk36  40892  cdlemk35s-id  40917  cdlemk39s-id  40919  cdlemk19x  40922  cdlemk53b  40935  cdlemk55  40940  cdlemk35u  40943  cdlemk55u  40945  cdlemk39u  40947  cdlemk19u  40949  cdlemk56  40950  tendoex  40954  cdleml5N  40959  dihord2pre  41204  dihord6apre  41235  dihord5b  41238  dihord5apre  41241  dihord  41243  dihmeetlem1N  41269  dihmeetlem2N  41278  dihglbcpreN  41279  dihmeetbN  41282  dihmeetlem4preN  41285  dihmeetlem5  41287  dihmeetlem6  41288  dihmeetlem7N  41289  dihmeetlem10N  41295  dihmeetlem11N  41296  dihmeetlem12N  41297  dihmeetlem13N  41298  dihmeetlem15N  41300  dihmeetlem17N  41302  dihmeetlem18N  41303  dihmeetlem19N  41304  dihmeetALTN  41306  dih1dimatlem0  41307  dihlspsnssN  41311  dvh3dim2  41427  sticksstones1  42119  sticksstones2  42120  sticksstones12  42131  aks6d1c6isolem1  42147  dvdsexpnn  42306  resubcan2  42361  mzpsubst  42721  diophrw  42732  eldioph2lem1  42733  rencldnfi  42794  pellexlem2  42803  pellqrexplicit  42850  infmrgelbi  42851  rmxycomplete  42890  congadd  42939  acongeq  42956  jm2.19  42966  jm2.22  42968  jm2.20nn  42970  jm2.25lem1  42971  jm2.27  42981  jm3.1  42993  lmhmlnmsplit  43060  pwssplit4  43062  hbtlem2  43097  dgraa0p  43122  proot1hash  43168  iocunico  43184  cantnf2  43298  dflim5  43302  omcl2  43306  tfsconcatrn  43315  nadd2rabex  43359  relexpxpmin  43690  brtrclfv2  43700  ntrclsk3  44043  grur1cld  44205  ismnu  44234  suprnmpt  45152  wessf1ornlem  45163  choicefi  45178  supxrgere  45313  supxrgelem  45317  supxrge  45318  infleinflem2  45351  snunioo1  45494  iccintsng  45505  fmul01  45562  lptre2pt  45622  0ellimcdiv  45631  fnlimfvre  45656  limsupmnfuzlem  45708  climisp  45728  limsupgtlem  45759  ibliccsinexp  45933  iblioosinexp  45935  volioc  45954  iblspltprt  45955  stoweidlem20  46002  stoweidlem22  46004  stoweidlem34  46016  stoweidlem44  46026  stoweidlem60  46042  wallispilem3  46049  fourierdlem42  46131  fourierdlem51  46139  fourierdlem54  46142  fourierdlem87  46175  fourierdlem97  46185  ioorrnopnlem  46286  sge0seq  46428  hoicvr  46530  fsupdm  46824  finfdm  46828  3f1oss1  47060  funfocofob  47063  imasetpreimafvbijlemfv  47387  uhgrimisgrgric  47916  uhgrimgrlim  47972  fprmappr  48330  lincresunit3lem3  48460  lindssnlvec  48472  rrx2linesl  48729  line2  48738  itsclc0lem3  48744  itsclc0yqsollem1  48748  itscnhlc0xyqsol  48751  itschlc0xyqsol1  48752  itsclc0  48757  itscnhlinecirc02plem2  48769  itscnhlinecirc02plem3  48770  uptrlem1  49196  uptr2  49207  setc1onsubc  49588