Theorem simpl3 1191

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 1185	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simpl13  1248  simpl23  1251  simpl33  1254  simp1l3  1266  simp2l3  1272  simp3l3  1278  3anandirs  1470  2nreu  4372  predtrss  6214  frpomin  6228  f1prex  7136  fcofo  7140  soisores  7178  weniso  7205  knatar  7208  ofmpteq  7533  funelss  7861  frrlem10  8082  fprlem1  8087  smorndom  8170  nnmord  8425  nnmword  8426  difsnen  8794  mapunen  8882  ac6sfi  8988  fipreima  9055  wemaplem2  9236  wemapso2lem  9241  en2eqpr  9694  indcardi  9728  acndom  9738  fodomfi2  9747  infmap2  9905  cflim2  9950  coftr  9960  infpssrlem4  9993  fin23lem11  10004  fincssdom  10010  isf32lem9  10048  fin1a2lem9  10095  gchpwdom  10357  gruima  10489  prpssnq  10677  distrlem4pr  10713  dedekind  11068  addcan  11089  addcan2  11090  divmulass  11586  supmul1  11874  uzsupss  12609  xaddass  12912  xleadd1a  12916  xlesubadd  12926  xmulasslem3  12949  xmulass  12950  xadddilem  12957  xadddi  12958  ixxun  13024  icoshftf1o  13135  snunioc  13141  difelfzle  13298  fzo1fzo0n0  13366  ssfzoulel  13409  modmuladd  13561  modifeq2int  13581  modaddmulmod  13586  modsubdir  13588  ltexp2a  13812  leexp2  13817  ltexp2r  13819  exple1  13822  expnlbnd2  13877  mulsubdivbinom2  13904  hashtpg  14127  ccatass  14221  ccatopth  14357  pfxccatin12lem2a  14368  pfxccat3  14375  cshinj  14452  2cshw  14454  s2f1o  14557  limsupgre  15118  addcn2  15231  mulcn2  15233  binomrisefac  15680  bpolydif  15693  dvdsmodexp  15899  modmulconst  15925  dvdsexp2im  15964  dvdsmod  15966  sadass  16106  gcdass  16183  rplpwr  16195  rpmulgcd2  16289  rpdvds  16293  rpexp  16355  prmdiveq  16415  hashgcdlem  16417  coprimeprodsq  16437  coprimeprodsq2  16438  pythagtriplem3  16447  pcdvdsb  16498  pcgcd1  16506  dvdsprmpweq  16513  pcbc  16529  0ram  16649  ramz2  16653  ramub1lem1  16655  mremre  17230  mrieqv2d  17265  lubun  18148  isnsgrp  18294  issubmnd  18327  gsumccatOLD  18394  frmdss2  18417  submefmnd  18449  sgrp2rid2ex  18481  mulgnn0p1  18630  mulgnnsubcl  18631  mulgneg  18637  mulgdirlem  18649  nmzsubg  18708  ghmmulg  18761  pmtrfv  18975  pmtrmvd  18979  pmtrfb  18988  odmodnn0  19063  oddvdsnn0  19067  odnncl  19068  odmod  19069  oddvds  19070  odeq  19073  odmulgid  19076  odmulg  19078  odmulgeq  19079  odbezout  19080  odf1o1  19092  odf1o2  19093  odngen  19097  odcau  19124  pgpssslw  19134  fislw  19145  lsmless1x  19164  lsmless2x  19165  lsmsubm  19173  lsmmod  19196  lsmmod2  19197  efgsfo  19260  cntzcmn  19356  odadd1  19364  odadd2  19365  odadd  19366  lsmcomx  19372  prdscmnd  19377  gsumconst  19450  ring1eq0  19744  cntzsubr  19972  isabvd  19995  rmodislmod  20106  rmodislmodOLD  20107  lspss  20161  0lmhm  20217  reslmhm2  20230  pwssplit0  20235  pwssplit1  20236  lbspss  20259  lspfixed  20305  lsmcv  20318  lspsnat  20322  xrsdsreclblem  20556  obselocv  20845  frlmsplit2  20890  frlmsslss2  20892  frlmup4  20918  lindff1  20937  lsslindf  20947  lsslinds  20948  islindf4  20955  issubassa  20983  aspss  20991  coe1subfv  21347  coe1tm  21354  mpomatmul  21503  mamutpos  21515  submaval  21638  mdetdiag  21656  mdetunilem1  21669  mdetunilem3  21671  mdetunilem9  21677  mdetmul  21680  maducoeval2  21697  madurid  21701  minmar1val  21705  cramer  21748  cpmatel2  21770  m2cpm  21798  decpmatmul  21829  pmatcollpw1lem2  21832  pmatcollpw1  21833  pmatcollpw2lem  21834  pm2mpcl  21854  mply1topmatcl  21862  mp2pm2mplem2  21864  mp2pm2mplem4  21866  pm2mpghmlem2  21869  pm2mpghmlem1  21870  cayhamlem2  21941  neiint  22163  topssnei  22183  cnrest2  22345  cnprest2  22349  cnt0  22405  cnt1  22409  cnhaus  22413  cncmp  22451  fiuncmp  22463  sscmp  22464  hauscmp  22466  cnconn  22481  unconn  22488  comppfsc  22591  kgen2ss  22614  ptpjopn  22671  ptrescn  22698  qtopss  22774  kqfvima  22789  r0cld  22797  cmphaushmeo  22859  fbssint  22897  fbasrn  22943  filuni  22944  ufilmax  22966  fin1aufil  22991  fmf  23004  fmss  23005  rnelfmlem  23011  rnelfm  23012  fmufil  23018  fmco  23020  flimss2  23031  flimss1  23032  flimrest  23042  cnpflf2  23059  cnpflf  23060  flfcnp  23063  lmflf  23064  supnfcls  23079  fclsss1  23081  fclsss2  23082  cnpfcfi  23099  subgntr  23166  opnsubg  23167  cldsubg  23170  ustuqtop1  23301  ucncn  23345  bldisj  23459  blgt0  23460  bl2in  23461  blss2ps  23464  blss2  23465  xbln0  23475  blssps  23485  blss  23486  lpbl  23565  blcld  23567  blcls  23568  stdbdmopn  23580  metcnp2  23604  txmetcnp  23609  blval2  23624  restmetu  23632  nmoix  23799  nmoi2  23800  nmoeq0  23806  nmotri  23809  metdsge  23918  metds0  23919  metdseq0  23923  icoopnst  24008  iccpnfhmeo  24014  xrhmeo  24015  nmhmcn  24189  cphsqrtcl2  24255  cphsqrtcl3  24256  fmcfil  24341  bcthlem5  24397  cmetcusp1  24422  cssbn  24444  pjth  24508  ovolunnul  24569  volun  24614  voliunlem2  24620  itg2const  24810  iblconst  24887  itgconst  24888  limcvallem  24940  dvcnp2  24989  dvcn  24990  deg1mul3le  25186  deg1tmle  25187  ig1pdvds  25246  coe11  25319  dgrmulc  25337  dvply1  25349  aaliou2  25405  efcvx  25513  tanord  25599  logdivlti  25680  logccv  25723  recxpcl  25735  cxplea  25756  cxple2a  25759  ang180  25869  isosctrlem2  25874  cxp2lim  26031  amgm  26045  muval1  26187  dvdssqf  26192  mumullem2  26234  bcmono  26330  lgsneg  26374  lgsmod  26376  lgsdirprm  26384  lgsdir  26385  lgsdi  26387  brbtwn2  27176  colinearalglem1  27177  colinearalg  27181  axcgrtr  27186  axcontlem2  27236  upgrewlkle2  27876  wlksoneq1eq2  27934  crctcshwlkn0lem5  28080  wspthsnwspthsnon  28182  lppthon  28416  upgriseupth  28472  4cyclusnfrgr  28557  numclwwlk1lem2foa  28619  numclwwlk5  28653  nvmul0or  28913  shless  29622  shlej1  29623  pjspansn  29840  kbmul  30218  homco2  30240  kbass2  30380  fnpreimac  30910  padct  30956  eliccelico  31000  elicoelioo  31001  iocinioc2  31002  difioo  31005  swrdrn2  31128  swrdrn3  31129  xrge0npcan  31205  isarchi2  31341  archiabl  31354  pidlnz  31473  lindssn  31475  ssmxidl  31544  mdetlap1  31678  zarclsiin  31723  pstmfval  31748  fmcncfil  31783  zrhnm  31819  qqhnm  31840  nexple  31877  volfiniune  32098  omsmeas  32190  eulerpartlemb  32235  probinc  32288  cndprob01  32302  signswmnd  32436  cvmsss2  33136  funsseq  33648  ttrclselem2  33712  sltres  33792  nolt02olem  33824  nolt02o  33825  nogt01o  33826  nosupbnd1lem1  33838  nosupbnd1lem4  33841  nosupbnd1lem5  33842  nosupbnd1lem6  33843  noinfbnd1lem1  33853  noinfbnd1lem4  33856  noinfbnd1lem6  33858  noinfbnd2  33861  noetainflem3  33869  sltlpss  34014  cofsslt  34015  coinitsslt  34016  cofcutrtime  34020  cgrtriv  34231  5segofs  34235  btwntriv2  34241  btwnxfr  34285  segcon2  34334  brsegle2  34338  seglelin  34345  outsideofeu  34360  lindsenlbs  35699  mblfinlem2  35742  blbnd  35872  rrndstprj2  35916  zerdivemp1x  36032  lsmsat  36949  lsatfixedN  36950  lssat  36957  lkrlsp  37043  lshpkrlem4  37054  cvrcon3b  37218  leat3  37236  atlen0  37251  atnle  37258  atlatmstc  37260  atlatle  37261  cvlcvr1  37280  cvlsupr2  37284  hlsupr2  37328  hlrelat2  37344  cvrexchlem  37360  cvratlem  37362  lnnat  37368  atexchcvrN  37381  1cvratlt  37415  1cvrjat  37416  3atlem3  37426  3atlem7  37430  llni2  37453  atcvrlln2  37460  llnexatN  37462  llncmp  37463  2llnmat  37465  2at0mat0  37466  2atnelpln  37485  llncvrlpln2  37498  2lplnmN  37500  2llnmj  37501  lplncmp  37503  lplnexatN  37504  2llnjaN  37507  lvoli3  37518  islvol2aN  37533  4atlem3a  37538  4atlem4a  37540  4atlem4b  37541  4atlem11  37550  4atlem12  37553  lplncvrlvol2  37556  lvolcmp  37558  2lplnmj  37563  islinei  37681  linepmap  37716  lneq2at  37719  2llnma3r  37729  elpaddn0  37741  elpaddatriN  37744  elpaddat  37745  paddcom  37754  paddss1  37758  paddss2  37759  paddasslem6  37766  paddasslem7  37767  paddasslem10  37770  paddasslem15  37775  pmodlem2  37788  pmodl42N  37792  pmapjoin  37793  atmod1i1m  37799  llnmod1i2  37801  llnexchb2lem  37809  polcon2bN  37861  pclfinclN  37891  poml4N  37894  poml6N  37896  osumcllem11N  37907  osumclN  37908  pmapojoinN  37909  pexmidlem2N  37912  pexmidlem3N  37913  pexmidlem4N  37914  pexmidlem6N  37916  pexmidlem7N  37917  pl42lem2N  37921  pl42lem3N  37922  pl42lem4N  37923  pl42N  37924  lhpexle3lem  37952  lhpmcvr3  37966  lhp2at0nle  37976  lhprelat3N  37981  lauteq  38036  lautco  38038  ltrncoidN  38069  ltrneq2  38089  ltrnnidn  38115  ltrnideq  38116  trlnle  38127  cdlemc  38138  cdlemd4  38142  cdlemd5  38143  cdlemd9  38147  cdlemd  38148  ltrneq3  38149  cdlemefrs29pre00  38336  cdlemefrs29cpre1  38339  cdlemefrs29clN  38340  cdlemefrs32fva  38341  cdlemefr29exN  38343  cdlemefr27cl  38344  cdlemefs27cl  38354  cdlemefs32sn1aw  38355  cdleme32fva  38378  cdleme32d  38385  cdleme32f  38387  cdleme32le  38388  cdleme40n  38409  cdleme41snaw  38417  cdleme17d3  38437  cdleme48fvg  38441  cdlemeg46fvcl  38447  cdlemeg46fgN  38475  cdleme48fgv  38479  ltrniotavalbN  38525  cdlemb3  38547  cdlemg15  38597  cdlemg17dN  38604  trlco  38668  cdlemg44b  38673  ltrncom  38679  trljco  38681  tendococl  38713  tendoplcl  38722  tendoplcom  38723  tendotr  38771  cdlemk36  38854  cdlemk35s-id  38879  cdlemk39s-id  38881  cdlemk19x  38884  cdlemk53b  38897  cdlemk55  38902  cdlemk35u  38905  cdlemk55u  38907  cdlemk39u  38909  cdlemk19u  38911  cdlemk56  38912  tendoex  38916  cdleml5N  38921  dihord2pre  39166  dihord6apre  39197  dihord5b  39200  dihord5apre  39203  dihord  39205  dihmeetlem1N  39231  dihmeetlem2N  39240  dihglbcpreN  39241  dihmeetbN  39244  dihmeetlem4preN  39247  dihmeetlem5  39249  dihmeetlem6  39250  dihmeetlem7N  39251  dihmeetlem10N  39257  dihmeetlem11N  39258  dihmeetlem12N  39259  dihmeetlem13N  39260  dihmeetlem15N  39262  dihmeetlem17N  39264  dihmeetlem18N  39265  dihmeetlem19N  39266  dihmeetALTN  39268  dih1dimatlem0  39269  dihlspsnssN  39273  dvh3dim2  39389  sticksstones1  40030  sticksstones2  40031  sticksstones12  40042  dvdsexpnn  40261  resubcan2  40292  mzpsubst  40486  diophrw  40497  eldioph2lem1  40498  rencldnfi  40559  pellexlem2  40568  pellqrexplicit  40615  infmrgelbi  40616  rmxycomplete  40655  congadd  40704  acongeq  40721  jm2.19  40731  jm2.22  40733  jm2.20nn  40735  jm2.25lem1  40736  jm2.27  40746  jm3.1  40758  lmhmlnmsplit  40828  pwssplit4  40830  hbtlem2  40865  dgraa0p  40890  idomrootle  40936  proot1hash  40941  iocunico  40958  relexpxpmin  41214  brtrclfv2  41224  ntrclsk3  41569  grur1cld  41739  ismnu  41768  suprnmpt  42599  wessf1ornlem  42611  choicefi  42629  supxrgere  42762  supxrgelem  42766  supxrge  42767  infleinflem2  42800  snunioo1  42940  iccintsng  42951  fmul01  43011  lptre2pt  43071  0ellimcdiv  43080  fnlimfvre  43105  limsupmnfuzlem  43157  climisp  43177  limsupgtlem  43208  ibliccsinexp  43382  iblioosinexp  43384  volioc  43403  iblspltprt  43404  stoweidlem20  43451  stoweidlem22  43453  stoweidlem34  43465  stoweidlem44  43475  stoweidlem60  43491  wallispilem3  43498  fourierdlem42  43580  fourierdlem51  43588  fourierdlem54  43591  fourierdlem87  43624  fourierdlem97  43634  ioorrnopnlem  43735  sge0seq  43874  hoicvr  43976  funfocofob  44457  imasetpreimafvbijlemfv  44742  fprmappr  45569  lincresunit3lem3  45703  lindssnlvec  45715  rrx2linesl  45977  line2  45986  itsclc0lem3  45992  itsclc0yqsollem1  45996  itscnhlc0xyqsol  45999  itschlc0xyqsol1  46000  itsclc0  46005  itscnhlinecirc02plem2  46017  itscnhlinecirc02plem3  46018