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  4394  predtrss  6269  frpomin  6287  f1prex  7218  fcofo  7222  soisores  7261  weniso  7288  knatar  7291  ofmpteq  7633  funelss  7979  frrlem10  8225  fprlem1  8230  smocdmdom  8288  nnmord  8547  nnmword  8548  naddasslem1  8609  naddasslem2  8610  difsnen  8972  mapunen  9059  ac6sfi  9168  fipreima  9242  wemaplem2  9433  wemapso2lem  9438  ttrclselem2  9616  en2eqpr  9895  indcardi  9929  acndom  9939  fodomfi2  9948  infmap2  10105  cflim2  10151  coftr  10161  infpssrlem4  10194  fin23lem11  10205  fincssdom  10211  isf32lem9  10249  fin1a2lem9  10296  gchpwdom  10558  gruima  10690  prpssnq  10878  distrlem4pr  10914  dedekind  11273  addcan  11294  addcan2  11295  divmulass  11796  supmul1  12088  uzsupss  12835  xaddass  13145  xleadd1a  13149  xlesubadd  13159  xmulasslem3  13182  xmulass  13183  xadddilem  13190  xadddi  13191  ixxun  13258  icoshftf1o  13371  snunioc  13377  difelfzle  13538  fzo1fzo0n0  13612  ssfzoulel  13657  modmuladd  13817  modifeq2int  13837  modaddmulmod  13842  modsubdir  13844  ltexp2a  14070  leexp2  14075  ltexp2r  14077  exple1  14081  expnlbnd2  14138  mulsubdivbinom2  14166  hashtpg  14389  ccatass  14493  ccatopth  14620  pfxccatin12lem2a  14631  pfxccat3  14638  cshinj  14715  2cshw  14717  s2f1o  14820  limsupgre  15385  addcn2  15498  mulcn2  15500  binomrisefac  15946  bpolydif  15959  dvdsmodexp  16168  modmulconst  16196  dvdsexp2im  16235  dvdsmod  16237  sadass  16379  gcdass  16455  rplpwr  16466  rpmulgcd2  16564  rpdvds  16568  rpexp  16630  prmdiveq  16694  hashgcdlem  16696  coprimeprodsq  16717  coprimeprodsq2  16718  pythagtriplem3  16727  pcdvdsb  16778  pcgcd1  16786  dvdsprmpweq  16793  pcbc  16809  0ram  16929  ramz2  16933  ramub1lem1  16935  mremre  17503  mrieqv2d  17542  lubun  18418  isnsgrp  18628  issubmnd  18666  frmdss2  18768  submefmnd  18800  sgrp2rid2ex  18832  mulgnn0p1  18995  mulgnnsubcl  18996  mulgneg  19002  mulgdirlem  19015  nmzsubg  19075  ghmmulg  19138  pmtrfv  19362  pmtrmvd  19366  pmtrfb  19375  odmodnn0  19450  oddvdsnn0  19454  odnncl  19455  odmod  19456  oddvds  19457  odeq  19460  odmulgid  19464  odmulg  19466  odmulgeq  19467  odbezout  19468  odf1o1  19482  odf1o2  19483  odngen  19487  odcau  19514  pgpssslw  19524  fislw  19535  lsmless1x  19554  lsmless2x  19555  lsmsubm  19563  lsmmod  19585  lsmmod2  19586  efgsfo  19649  cntzcmn  19750  odadd1  19758  odadd2  19759  odadd  19760  lsmcomx  19766  prdscmnd  19771  gsumconst  19844  ring1eq0  20214  cntzsubrng  20480  cntzsubr  20519  isabvd  20725  rmodislmod  20861  lspss  20915  0lmhm  20972  reslmhm2  20985  pwssplit0  20990  pwssplit1  20991  lbspss  21014  lspfixed  21063  lsmcv  21076  lspsnat  21080  2idlcpblrng  21206  cnfldfunALT  21304  cnfldfunALTOLD  21317  xrsdsreclblem  21347  obselocv  21663  frlmsplit2  21708  frlmsslss2  21710  frlmup4  21736  lindff1  21755  lsslindf  21765  lsslinds  21766  islindf4  21773  issubassa  21802  aspss  21812  coe1subfv  22178  coe1tm  22185  mpomatmul  22359  mamutpos  22371  submaval  22494  mdetdiag  22512  mdetunilem1  22525  mdetunilem3  22527  mdetunilem9  22533  mdetmul  22536  maducoeval2  22553  madurid  22557  minmar1val  22561  cramer  22604  cpmatel2  22626  m2cpm  22654  decpmatmul  22685  pmatcollpw1lem2  22688  pmatcollpw1  22689  pmatcollpw2lem  22690  pm2mpcl  22710  mply1topmatcl  22718  mp2pm2mplem2  22720  mp2pm2mplem4  22722  pm2mpghmlem2  22725  pm2mpghmlem1  22726  cayhamlem2  22797  neiint  23017  topssnei  23037  cnrest2  23199  cnprest2  23203  cnt0  23259  cnt1  23263  cnhaus  23267  cncmp  23305  fiuncmp  23317  sscmp  23318  hauscmp  23320  cnconn  23335  unconn  23342  comppfsc  23445  kgen2ss  23468  ptpjopn  23525  ptrescn  23552  qtopss  23628  kqfvima  23643  r0cld  23651  cmphaushmeo  23713  fbssint  23751  fbasrn  23797  filuni  23798  ufilmax  23820  fin1aufil  23845  fmf  23858  fmss  23859  rnelfmlem  23865  rnelfm  23866  fmufil  23872  fmco  23874  flimss2  23885  flimss1  23886  flimrest  23896  cnpflf2  23913  cnpflf  23914  flfcnp  23917  lmflf  23918  supnfcls  23933  fclsss1  23935  fclsss2  23936  cnpfcfi  23953  subgntr  24020  opnsubg  24021  cldsubg  24024  ustuqtop1  24154  ucncn  24197  bldisj  24311  blgt0  24312  bl2in  24313  blss2ps  24316  blss2  24317  xbln0  24327  blssps  24337  blss  24338  lpbl  24416  blcld  24418  blcls  24419  stdbdmopn  24431  metcnp2  24455  txmetcnp  24460  blval2  24475  restmetu  24483  nmoix  24642  nmoi2  24643  nmoeq0  24649  nmotri  24652  metdsge  24763  metds0  24764  metdseq0  24768  icoopnst  24861  iccpnfhmeo  24868  xrhmeo  24869  nmhmcn  25045  cphsqrtcl2  25111  cphsqrtcl3  25112  fmcfil  25197  bcthlem5  25253  cmetcusp1  25278  cssbn  25300  pjth  25364  ovolunnul  25426  volun  25471  voliunlem2  25477  itg2const  25666  iblconst  25744  itgconst  25745  limcvallem  25797  dvcnp2  25846  dvcnp2OLD  25847  dvcn  25848  deg1mul3le  26047  deg1tmle  26048  idomrootle  26103  ig1pdvds  26110  coe11  26183  dgrmulc  26202  dvply1  26216  aaliou2  26273  efcvx  26384  tanord  26472  logdivlti  26554  logccv  26597  recxpcl  26609  cxplea  26630  cxple2a  26633  ang180  26749  isosctrlem2  26754  cxp2lim  26912  amgm  26926  muval1  27068  dvdssqf  27073  mumullem2  27115  bcmono  27213  lgsneg  27257  lgsmod  27259  lgsdirprm  27267  lgsdir  27268  lgsdi  27270  sltres  27599  nolt02olem  27631  nolt02o  27632  nogt01o  27633  nosupbnd1lem1  27645  nosupbnd1lem4  27648  nosupbnd1lem5  27649  nosupbnd1lem6  27650  noinfbnd1lem1  27660  noinfbnd1lem4  27663  noinfbnd1lem6  27665  noinfbnd2  27668  noetainflem3  27676  sltlpss  27851  cofsslt  27860  coinitsslt  27861  cofcutrtime  27869  addsass  27946  addsdi  28092  mulsass  28103  sltmul2  28108  norecdiv  28127  brbtwn2  28881  colinearalglem1  28882  colinearalg  28886  axcgrtr  28891  axcontlem2  28941  upgrewlkle2  29583  wlksoneq1eq2  29639  crctcshwlkn0lem5  29790  wspthsnwspthsnon  29892  lppthon  30126  upgriseupth  30182  4cyclusnfrgr  30267  numclwwlk1lem2foa  30329  numclwwlk5  30363  nvmul0or  30625  shless  31334  shlej1  31335  pjspansn  31552  kbmul  31930  homco2  31952  kbass2  32092  fnpreimac  32648  padct  32696  eliccelico  32755  elicoelioo  32756  iocinioc2  32757  difioo  32760  nexple  32822  swrdrn2  32930  swrdrn3  32931  xrge0npcan  32996  isarchi2  33149  archiabl  33162  pidlnz  33336  lindssn  33338  ssmxidl  33434  mdetlap1  33834  zarclsiin  33879  pstmfval  33904  fmcncfil  33939  zrhnm  33975  qqhnm  33998  volfiniune  34238  omsmeas  34331  eulerpartlemb  34376  probinc  34429  cndprob01  34443  signswmnd  34565  cvmsss2  35306  funsseq  35800  cgrtriv  36035  5segofs  36039  btwntriv2  36045  btwnxfr  36089  segcon2  36138  brsegle2  36142  seglelin  36149  outsideofeu  36164  weiunpo  36498  weiunfr  36500  weiunse  36501  lindsenlbs  37654  mblfinlem2  37697  blbnd  37826  rrndstprj2  37870  zerdivemp1x  37986  lsmsat  39046  lsatfixedN  39047  lssat  39054  lkrlsp  39140  lshpkrlem4  39151  cvrcon3b  39315  leat3  39333  atlen0  39348  atnle  39355  atlatmstc  39357  atlatle  39358  cvlcvr1  39377  cvlsupr2  39381  hlsupr2  39425  hlrelat2  39441  cvrexchlem  39457  cvratlem  39459  lnnat  39465  atexchcvrN  39478  1cvratlt  39512  1cvrjat  39513  3atlem3  39523  3atlem7  39527  llni2  39550  atcvrlln2  39557  llnexatN  39559  llncmp  39560  2llnmat  39562  2at0mat0  39563  2atnelpln  39582  llncvrlpln2  39595  2lplnmN  39597  2llnmj  39598  lplncmp  39600  lplnexatN  39601  2llnjaN  39604  lvoli3  39615  islvol2aN  39630  4atlem3a  39635  4atlem4a  39637  4atlem4b  39638  4atlem11  39647  4atlem12  39650  lplncvrlvol2  39653  lvolcmp  39655  2lplnmj  39660  islinei  39778  linepmap  39813  lneq2at  39816  2llnma3r  39826  elpaddn0  39838  elpaddatriN  39841  elpaddat  39842  paddcom  39851  paddss1  39855  paddss2  39856  paddasslem6  39863  paddasslem7  39864  paddasslem10  39867  paddasslem15  39872  pmodlem2  39885  pmodl42N  39889  pmapjoin  39890  atmod1i1m  39896  llnmod1i2  39898  llnexchb2lem  39906  polcon2bN  39958  pclfinclN  39988  poml4N  39991  poml6N  39993  osumcllem11N  40004  osumclN  40005  pmapojoinN  40006  pexmidlem2N  40009  pexmidlem3N  40010  pexmidlem4N  40011  pexmidlem6N  40013  pexmidlem7N  40014  pl42lem2N  40018  pl42lem3N  40019  pl42lem4N  40020  pl42N  40021  lhpexle3lem  40049  lhpmcvr3  40063  lhp2at0nle  40073  lhprelat3N  40078  lauteq  40133  lautco  40135  ltrncoidN  40166  ltrneq2  40186  ltrnnidn  40212  ltrnideq  40213  trlnle  40224  cdlemc  40235  cdlemd4  40239  cdlemd5  40240  cdlemd9  40244  cdlemd  40245  ltrneq3  40246  cdlemefrs29pre00  40433  cdlemefrs29cpre1  40436  cdlemefrs29clN  40437  cdlemefrs32fva  40438  cdlemefr29exN  40440  cdlemefr27cl  40441  cdlemefs27cl  40451  cdlemefs32sn1aw  40452  cdleme32fva  40475  cdleme32d  40482  cdleme32f  40484  cdleme32le  40485  cdleme40n  40506  cdleme41snaw  40514  cdleme17d3  40534  cdleme48fvg  40538  cdlemeg46fvcl  40544  cdlemeg46fgN  40572  cdleme48fgv  40576  ltrniotavalbN  40622  cdlemb3  40644  cdlemg15  40694  cdlemg17dN  40701  trlco  40765  cdlemg44b  40770  ltrncom  40776  trljco  40778  tendococl  40810  tendoplcl  40819  tendoplcom  40820  tendotr  40868  cdlemk36  40951  cdlemk35s-id  40976  cdlemk39s-id  40978  cdlemk19x  40981  cdlemk53b  40994  cdlemk55  40999  cdlemk35u  41002  cdlemk55u  41004  cdlemk39u  41006  cdlemk19u  41008  cdlemk56  41009  tendoex  41013  cdleml5N  41018  dihord2pre  41263  dihord6apre  41294  dihord5b  41297  dihord5apre  41300  dihord  41302  dihmeetlem1N  41328  dihmeetlem2N  41337  dihglbcpreN  41338  dihmeetbN  41341  dihmeetlem4preN  41344  dihmeetlem5  41346  dihmeetlem6  41347  dihmeetlem7N  41348  dihmeetlem10N  41354  dihmeetlem11N  41355  dihmeetlem12N  41356  dihmeetlem13N  41357  dihmeetlem15N  41359  dihmeetlem17N  41361  dihmeetlem18N  41362  dihmeetlem19N  41363  dihmeetALTN  41365  dih1dimatlem0  41366  dihlspsnssN  41370  dvh3dim2  41486  sticksstones1  42178  sticksstones2  42179  sticksstones12  42190  aks6d1c6isolem1  42206  dvdsexpnn  42365  resubcan2  42420  mzpsubst  42780  diophrw  42791  eldioph2lem1  42792  rencldnfi  42853  pellexlem2  42862  pellqrexplicit  42909  infmrgelbi  42910  rmxycomplete  42949  congadd  42998  acongeq  43015  jm2.19  43025  jm2.22  43027  jm2.20nn  43029  jm2.25lem1  43030  jm2.27  43040  jm3.1  43052  lmhmlnmsplit  43119  pwssplit4  43121  hbtlem2  43156  dgraa0p  43181  proot1hash  43227  iocunico  43243  cantnf2  43357  dflim5  43361  omcl2  43365  tfsconcatrn  43374  nadd2rabex  43418  relexpxpmin  43749  brtrclfv2  43759  ntrclsk3  44102  grur1cld  44264  ismnu  44293  suprnmpt  45210  wessf1ornlem  45221  choicefi  45236  supxrgere  45371  supxrgelem  45375  supxrge  45376  infleinflem2  45408  snunioo1  45551  iccintsng  45562  fmul01  45619  lptre2pt  45677  0ellimcdiv  45686  fnlimfvre  45711  limsupmnfuzlem  45763  climisp  45783  limsupgtlem  45814  ibliccsinexp  45988  iblioosinexp  45990  volioc  46009  iblspltprt  46010  stoweidlem20  46057  stoweidlem22  46059  stoweidlem34  46071  stoweidlem44  46081  stoweidlem60  46097  wallispilem3  46104  fourierdlem42  46186  fourierdlem51  46194  fourierdlem54  46197  fourierdlem87  46230  fourierdlem97  46240  ioorrnopnlem  46341  sge0seq  46483  hoicvr  46585  fsupdm  46879  finfdm  46883  3f1oss1  47105  funfocofob  47108  imasetpreimafvbijlemfv  47432  uhgrimisgrgric  47961  uhgrimgrlim  48017  fprmappr  48375  lincresunit3lem3  48505  lindssnlvec  48517  rrx2linesl  48774  line2  48783  itsclc0lem3  48789  itsclc0yqsollem1  48793  itscnhlc0xyqsol  48796  itschlc0xyqsol1  48797  itsclc0  48802  itscnhlinecirc02plem2  48814  itscnhlinecirc02plem3  48815  uptrlem1  49241  uptr2  49252  setc1onsubc  49633