Theorem simpl3 1203

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  simpll3OLD  1231  simprl3OLD  1243  simpl13  1290  simpl23  1296  simpl33  1302  simp1l3  1324  simp2l3  1330  simp3l3  1336  3anandirs  1545  f1prex  6811  fcofo  6815  soisores  6849  weniso  6876  knatar  6879  ofmpteq  7193  smorndom  7748  nnmord  7996  nnmword  7997  difsnen  8330  mapunen  8417  ac6sfi  8492  fipreima  8560  wemaplem2  8741  wemapso2lem  8746  en2eqpr  9163  indcardi  9197  acndom  9207  fodomfi2  9216  infmap2  9375  cflim2  9420  coftr  9430  infpssrlem4  9463  fin23lem11  9474  fincssdom  9480  isf32lem9  9518  fin1a2lem9  9565  gchpwdom  9827  gruima  9959  prpssnq  10147  distrlem4pr  10183  dedekind  10539  addcan  10560  addcan2  10561  divmulass  11056  supmul1  11346  uzsupss  12087  xaddass  12391  xleadd1a  12395  xlesubadd  12405  xmulasslem3  12428  xmulass  12429  xadddilem  12436  xadddi  12437  ixxun  12503  icoshftf1o  12610  snunioc  12617  difelfzle  12771  fzo1fzo0n0  12838  ssfzoulel  12881  modmuladd  13031  modifeq2int  13051  modaddmulmod  13056  modsubdir  13058  ltexp2a  13230  leexp2  13233  ltexp2r  13235  exple1  13238  expnlbnd2  13314  mulsubdivbinom2  13367  hashtpg  13581  ccatass  13678  ccatpfx  13810  ccatopth  13834  ccatopthOLD  13835  swrdccatin12lem2a  13853  pfxccat3  13863  swrdccat3OLD  13864  cshinj  13962  s2f1o  14067  limsupgre  14620  addcn2  14732  mulcn2  14734  binomrisefac  15175  bpolydif  15188  dvdsmodexp  15395  modmulconst  15420  dvdsmod  15457  sadass  15599  gcdass  15670  rplpwr  15682  rppwr  15683  rpmulgcd2  15775  rpdvds  15779  rpexp  15836  prmdiveq  15895  hashgcdlem  15897  coprimeprodsq  15917  coprimeprodsq2  15918  pythagtriplem3  15927  pcdvdsb  15977  pcgcd1  15985  dvdsprmpweq  15992  pcbc  16008  0ram  16128  ramz2  16132  ramub1lem1  16134  mremre  16650  mrieqv2d  16685  lubun  17509  isnsgrp  17674  issubmnd  17704  gsumccat  17764  frmdss2  17787  sgrp2rid2ex  17801  mulgnn0p1  17939  mulgnnsubcl  17940  mulgneg  17946  mulgdirlem  17957  nmzsubg  18019  ghmmulg  18056  pmtrfv  18255  pmtrmvd  18259  pmtrfb  18268  odmodnn0  18343  oddvdsnn0  18347  odnncl  18348  odmod  18349  oddvds  18350  odeq  18353  odmulgid  18355  odmulg  18357  odmulgeq  18358  odbezout  18359  odf1o1  18371  odf1o2  18372  odngen  18376  odcau  18403  pgpssslw  18413  fislw  18424  lsmless1x  18443  lsmless2x  18444  lsmsubm  18452  lsmmod  18472  lsmmod2  18473  efgsfo  18537  cntzcmn  18631  odadd1  18637  odadd2  18638  odadd  18639  lsmcomx  18645  prdscmnd  18650  gsumconst  18720  ring1eq0  18977  cntzsubr  19204  isabvd  19212  rmodislmod  19323  lspss  19379  0lmhm  19435  reslmhm2  19448  pwssplit0  19453  pwssplit1  19454  lbspss  19477  lspfixed  19523  lspfixedOLD  19524  lsmcv  19537  lspsnat  19541  issubassa  19721  aspss  19729  coe1subfv  20032  coe1tm  20039  xrsdsreclblem  20188  obselocv  20471  frlmsplit2  20516  frlmsslss2  20518  frlmup4  20544  lindff1  20563  lsslindf  20573  lsslinds  20574  islindf4  20581  mpt2matmul  20657  mamutpos  20669  submaval  20792  mdetdiag  20810  mdetunilem1  20823  mdetunilem3  20825  mdetunilem9  20831  mdetmul  20834  maducoeval2  20851  madurid  20855  minmar1val  20859  cramer  20904  cpmatel2  20925  m2cpm  20953  decpmatmul  20984  pmatcollpw1lem2  20987  pmatcollpw1  20988  pmatcollpw2lem  20989  pm2mpcl  21009  mply1topmatcl  21017  mp2pm2mplem2  21019  mp2pm2mplem4  21021  pm2mpghmlem2  21024  pm2mpghmlem1  21025  cayhamlem2  21096  neiint  21316  topssnei  21336  cnrest2  21498  cnprest2  21502  cnt0  21558  cnt1  21562  cnhaus  21566  cncmp  21604  fiuncmp  21616  sscmp  21617  hauscmp  21619  cnconn  21634  unconn  21641  comppfsc  21744  kgen2ss  21767  ptpjopn  21824  ptrescn  21851  qtopss  21927  kqfvima  21942  r0cld  21950  cmphaushmeo  22012  fbssint  22050  fbasrn  22096  filuni  22097  ufilmax  22119  fin1aufil  22144  fmf  22157  fmss  22158  rnelfmlem  22164  rnelfm  22165  fmufil  22171  fmco  22173  flimss2  22184  flimss1  22185  flimrest  22195  cnpflf2  22212  cnpflf  22213  flfcnp  22216  lmflf  22217  supnfcls  22232  fclsss1  22234  fclsss2  22235  cnpfcfi  22252  subgntr  22318  opnsubg  22319  cldsubg  22322  ustuqtop1  22453  ucncn  22497  bldisj  22611  blgt0  22612  bl2in  22613  blss2ps  22616  blss2  22617  xbln0  22627  blssps  22637  blss  22638  lpbl  22716  blcld  22718  blcls  22719  stdbdmopn  22731  metcnp2  22755  txmetcnp  22760  blval2  22775  restmetu  22783  nmoix  22941  nmoi2  22942  nmoeq0  22948  nmotri  22951  metdsge  23060  metds0  23061  metdseq0  23065  icoopnst  23146  iccpnfhmeo  23152  xrhmeo  23153  nmhmcn  23327  cphsqrtcl2  23393  cphsqrtcl3  23394  fmcfil  23478  bcthlem5  23534  cmetcusp1  23559  cssbn  23581  pjth  23645  ovolunnul  23704  volun  23749  voliunlem2  23755  itg2const  23944  iblconst  24021  itgconst  24022  limcvallem  24072  dvcnp2  24120  dvcn  24121  deg1mul3le  24313  deg1tmle  24314  ig1pdvds  24373  coe11  24446  dgrmulc  24464  dvply1  24476  aaliou2  24532  efcvx  24640  tanord  24722  logdivlti  24803  logccv  24846  recxpcl  24858  cxplea  24879  cxple2a  24882  ang180  24992  isosctrlem2  24997  cxp2lim  25155  amgm  25169  muval1  25311  dvdssqf  25316  mumullem2  25358  bcmono  25454  lgsneg  25498  lgsmod  25500  lgsdirprm  25508  lgsdir  25509  lgsdi  25511  brbtwn2  26254  colinearalglem1  26255  colinearalg  26259  axcgrtr  26264  axcontlem2  26314  upgrewlkle2  26954  wlksoneq1eq2  27011  crctcshwlkn0lem5  27163  wspthsnwspthsnon  27296  lppthon  27554  upgriseupth  27610  4cyclusnfrgr  27700  numclwwlk1lem2foa  27769  numclwwlk1lem2foaOLD  27770  numclwwlk5  27820  nvmul0or  28077  shless  28790  shlej1  28791  pjspansn  29008  kbmul  29386  homco2  29408  kbass2  29548  fnpreimac  30036  padct  30063  eliccelico  30103  elicoelioo  30104  iocinioc2  30105  difioo  30108  xrge0npcan  30256  isarchi2  30301  archiabl  30314  mdetlap1  30490  pstmfval  30537  fmcncfil  30575  zrhnm  30611  qqhnm  30632  nexple  30669  volfiniune  30891  omsmeas  30983  eulerpartlemb  31028  probinc  31082  cndprob01  31096  signswmnd  31234  cvmsss2  31855  dvdspw  32230  funsseq  32259  frpomin  32327  sltres  32404  nolt02olem  32433  nolt02o  32434  nosupbnd1lem1  32443  nosupbnd1lem4  32446  nosupbnd1lem5  32447  nosupbnd1lem6  32448  cgrtriv  32698  5segofs  32702  btwntriv2  32708  btwnxfr  32752  segcon2  32801  brsegle2  32805  seglelin  32812  outsideofeu  32827  lindsenlbs  34030  mblfinlem2  34073  blbnd  34210  rrndstprj2  34254  zerdivemp1x  34370  lsmsat  35162  lsatfixedN  35163  lssat  35170  lkrlsp  35256  lshpkrlem4  35267  cvrcon3b  35431  leat3  35449  atlen0  35464  atnle  35471  atlatmstc  35473  atlatle  35474  cvlcvr1  35493  cvlsupr2  35497  hlsupr2  35541  hlrelat2  35557  cvrexchlem  35573  cvratlem  35575  lnnat  35581  atexchcvrN  35594  1cvratlt  35628  1cvrjat  35629  3atlem3  35639  3atlem7  35643  llni2  35666  atcvrlln2  35673  llnexatN  35675  llncmp  35676  2llnmat  35678  2at0mat0  35679  2atnelpln  35698  llncvrlpln2  35711  2lplnmN  35713  2llnmj  35714  lplncmp  35716  lplnexatN  35717  2llnjaN  35720  lvoli3  35731  islvol2aN  35746  4atlem3a  35751  4atlem4a  35753  4atlem4b  35754  4atlem11  35763  4atlem12  35766  lplncvrlvol2  35769  lvolcmp  35771  2lplnmj  35776  islinei  35894  linepmap  35929  lneq2at  35932  2llnma3r  35942  elpaddn0  35954  elpaddatriN  35957  elpaddat  35958  paddcom  35967  paddss1  35971  paddss2  35972  paddasslem6  35979  paddasslem7  35980  paddasslem10  35983  paddasslem15  35988  pmodlem2  36001  pmodl42N  36005  pmapjoin  36006  atmod1i1m  36012  llnmod1i2  36014  llnexchb2lem  36022  polcon2bN  36074  pclfinclN  36104  poml4N  36107  poml6N  36109  osumcllem11N  36120  osumclN  36121  pmapojoinN  36122  pexmidlem2N  36125  pexmidlem3N  36126  pexmidlem4N  36127  pexmidlem6N  36129  pexmidlem7N  36130  pl42lem2N  36134  pl42lem3N  36135  pl42lem4N  36136  pl42N  36137  lhpexle3lem  36165  lhpmcvr3  36179  lhp2at0nle  36189  lhprelat3N  36194  lauteq  36249  lautco  36251  ltrncoidN  36282  ltrneq2  36302  ltrnnidn  36328  ltrnideq  36329  trlnle  36340  cdlemc  36351  cdlemd4  36355  cdlemd5  36356  cdlemd9  36360  cdlemd  36361  ltrneq3  36362  cdlemefrs29pre00  36549  cdlemefrs29cpre1  36552  cdlemefrs29clN  36553  cdlemefrs32fva  36554  cdlemefr29exN  36556  cdlemefr27cl  36557  cdlemefs27cl  36567  cdlemefs32sn1aw  36568  cdleme32fva  36591  cdleme32d  36598  cdleme32f  36600  cdleme32le  36601  cdleme40n  36622  cdleme41snaw  36630  cdleme17d3  36650  cdleme48fvg  36654  cdlemeg46fvcl  36660  cdlemeg46fgN  36688  cdleme48fgv  36692  ltrniotavalbN  36738  cdlemb3  36760  cdlemg15  36810  cdlemg17dN  36817  trlco  36881  cdlemg44b  36886  ltrncom  36892  trljco  36894  tendococl  36926  tendoplcl  36935  tendoplcom  36936  tendotr  36984  cdlemk36  37067  cdlemk35s-id  37092  cdlemk39s-id  37094  cdlemk19x  37097  cdlemk53b  37110  cdlemk55  37115  cdlemk35u  37118  cdlemk55u  37120  cdlemk39u  37122  cdlemk19u  37124  cdlemk56  37125  tendoex  37129  cdleml5N  37134  dihord2pre  37379  dihord6apre  37410  dihord5b  37413  dihord5apre  37416  dihord  37418  dihmeetlem1N  37444  dihmeetlem2N  37453  dihglbcpreN  37454  dihmeetbN  37457  dihmeetlem4preN  37460  dihmeetlem5  37462  dihmeetlem6  37463  dihmeetlem7N  37464  dihmeetlem10N  37470  dihmeetlem11N  37471  dihmeetlem12N  37472  dihmeetlem13N  37473  dihmeetlem15N  37475  dihmeetlem17N  37477  dihmeetlem18N  37478  dihmeetlem19N  37479  dihmeetALTN  37481  dih1dimatlem0  37482  dihlspsnssN  37486  dvh3dim2  37602  resubcan2  38195  mzpsubst  38271  diophrw  38282  eldioph2lem1  38283  rencldnfi  38345  pellexlem2  38354  pellqrexplicit  38401  infmrgelbi  38402  rmxycomplete  38441  congadd  38492  acongeq  38509  jm2.19  38519  jm2.22  38521  jm2.20nn  38523  jm2.25lem1  38524  jm2.27  38534  jm3.1  38546  lmhmlnmsplit  38616  pwssplit4  38618  hbtlem2  38653  dgraa0p  38678  idomrootle  38732  proot1hash  38737  iocunico  38754  relexpxpmin  38966  brtrclfv2  38976  ntrclsk3  39324  suprnmpt  40279  wessf1ornlem  40294  choicefi  40313  supxrgere  40457  supxrgelem  40461  supxrge  40462  infleinflem2  40495  snunioo1  40647  iccintsng  40658  fmul01  40720  lptre2pt  40780  0ellimcdiv  40789  fnlimfvre  40814  limsupmnfuzlem  40866  climisp  40886  limsupgtlem  40917  ibliccsinexp  41094  iblioosinexp  41096  volioc  41115  iblspltprt  41116  stoweidlem20  41164  stoweidlem22  41166  stoweidlem34  41178  stoweidlem44  41188  stoweidlem60  41204  wallispilem3  41211  fourierdlem42  41293  fourierdlem51  41301  fourierdlem54  41304  fourierdlem87  41337  fourierdlem97  41347  ioorrnopnlem  41448  sge0seq  41587  hoicvr  41689  lincresunit3lem3  43278  lindssnlvec  43290  rrx2linesl  43479  line2  43488  itsclc0lem3  43494  itsclc0yqsollem1  43498  itscnhlc0xyqsol  43501  itschlc0xyqsol1  43502  itsclc0  43507  itscnhlinecirc02plem2  43519  itscnhlinecirc02plem3  43520