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  1469  2nreu  4442  predtrss  6328  frpomin  6346  f1prex  7293  fcofo  7297  soisores  7335  weniso  7362  knatar  7365  ofmpteq  7707  funelss  8051  frrlem10  8300  fprlem1  8305  smocdmdom  8388  nnmord  8652  nnmword  8653  naddasslem1  8714  naddasslem2  8715  difsnen  9077  mapunen  9170  ac6sfi  9311  fipreima  9382  wemaplem2  9570  wemapso2lem  9575  ttrclselem2  9749  en2eqpr  10030  indcardi  10064  acndom  10074  fodomfi2  10083  infmap2  10241  cflim2  10286  coftr  10296  infpssrlem4  10329  fin23lem11  10340  fincssdom  10346  isf32lem9  10384  fin1a2lem9  10431  gchpwdom  10693  gruima  10825  prpssnq  11013  distrlem4pr  11049  dedekind  11407  addcan  11428  addcan2  11429  divmulass  11925  supmul1  12213  uzsupss  12954  xaddass  13260  xleadd1a  13264  xlesubadd  13274  xmulasslem3  13297  xmulass  13298  xadddilem  13305  xadddi  13306  ixxun  13372  icoshftf1o  13483  snunioc  13489  difelfzle  13646  fzo1fzo0n0  13715  ssfzoulel  13758  modmuladd  13910  modifeq2int  13930  modaddmulmod  13935  modsubdir  13937  ltexp2a  14162  leexp2  14167  ltexp2r  14169  exple1  14172  expnlbnd2  14228  mulsubdivbinom2  14253  hashtpg  14478  ccatass  14570  ccatopth  14698  pfxccatin12lem2a  14709  pfxccat3  14716  cshinj  14793  2cshw  14795  s2f1o  14899  limsupgre  15457  addcn2  15570  mulcn2  15572  binomrisefac  16018  bpolydif  16031  dvdsmodexp  16238  modmulconst  16264  dvdsexp2im  16303  dvdsmod  16305  sadass  16445  gcdass  16522  rplpwr  16532  rpmulgcd2  16626  rpdvds  16630  rpexp  16693  prmdiveq  16754  hashgcdlem  16756  coprimeprodsq  16776  coprimeprodsq2  16777  pythagtriplem3  16786  pcdvdsb  16837  pcgcd1  16845  dvdsprmpweq  16852  pcbc  16868  0ram  16988  ramz2  16992  ramub1lem1  16994  mremre  17583  mrieqv2d  17618  lubun  18506  isnsgrp  18682  issubmnd  18720  frmdss2  18814  submefmnd  18846  sgrp2rid2ex  18878  mulgnn0p1  19039  mulgnnsubcl  19040  mulgneg  19046  mulgdirlem  19059  nmzsubg  19119  ghmmulg  19181  pmtrfv  19406  pmtrmvd  19410  pmtrfb  19419  odmodnn0  19494  oddvdsnn0  19498  odnncl  19499  odmod  19500  oddvds  19501  odeq  19504  odmulgid  19508  odmulg  19510  odmulgeq  19511  odbezout  19512  odf1o1  19526  odf1o2  19527  odngen  19531  odcau  19558  pgpssslw  19568  fislw  19579  lsmless1x  19598  lsmless2x  19599  lsmsubm  19607  lsmmod  19629  lsmmod2  19630  efgsfo  19693  cntzcmn  19794  odadd1  19802  odadd2  19803  odadd  19804  lsmcomx  19810  prdscmnd  19815  gsumconst  19888  ring1eq0  20233  cntzsubrng  20503  cntzsubr  20544  isabvd  20699  rmodislmod  20812  rmodislmodOLD  20813  lspss  20867  0lmhm  20924  reslmhm2  20937  pwssplit0  20942  pwssplit1  20943  lbspss  20966  lspfixed  21015  lsmcv  21028  lspsnat  21032  2idlcpblrng  21164  cnfldfunALT  21293  cnfldfunALTOLD  21306  xrsdsreclblem  21344  obselocv  21661  frlmsplit2  21706  frlmsslss2  21708  frlmup4  21734  lindff1  21753  lsslindf  21763  lsslinds  21764  islindf4  21771  issubassa  21799  aspss  21809  coe1subfv  22184  coe1tm  22191  mpomatmul  22347  mamutpos  22359  submaval  22482  mdetdiag  22500  mdetunilem1  22513  mdetunilem3  22515  mdetunilem9  22521  mdetmul  22524  maducoeval2  22541  madurid  22545  minmar1val  22549  cramer  22592  cpmatel2  22614  m2cpm  22642  decpmatmul  22673  pmatcollpw1lem2  22676  pmatcollpw1  22677  pmatcollpw2lem  22678  pm2mpcl  22698  mply1topmatcl  22706  mp2pm2mplem2  22708  mp2pm2mplem4  22710  pm2mpghmlem2  22713  pm2mpghmlem1  22714  cayhamlem2  22785  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  24189  bldisj  24303  blgt0  24304  bl2in  24305  blss2ps  24308  blss2  24309  xbln0  24319  blssps  24329  blss  24330  lpbl  24411  blcld  24413  blcls  24414  stdbdmopn  24426  metcnp2  24450  txmetcnp  24455  blval2  24470  restmetu  24478  nmoix  24645  nmoi2  24646  nmoeq0  24652  nmotri  24655  metdsge  24764  metds0  24765  metdseq0  24769  icoopnst  24862  iccpnfhmeo  24869  xrhmeo  24870  nmhmcn  25046  cphsqrtcl2  25113  cphsqrtcl3  25114  fmcfil  25199  bcthlem5  25255  cmetcusp1  25280  cssbn  25302  pjth  25366  ovolunnul  25428  volun  25473  voliunlem2  25479  itg2const  25669  iblconst  25746  itgconst  25747  limcvallem  25799  dvcnp2  25848  dvcnp2OLD  25849  dvcn  25850  deg1mul3le  26051  deg1tmle  26052  idomrootle  26106  ig1pdvds  26113  coe11  26186  dgrmulc  26205  dvply1  26217  aaliou2  26274  efcvx  26385  tanord  26471  logdivlti  26553  logccv  26596  recxpcl  26608  cxplea  26629  cxple2a  26632  ang180  26745  isosctrlem2  26750  cxp2lim  26908  amgm  26922  muval1  27064  dvdssqf  27069  mumullem2  27111  bcmono  27209  lgsneg  27253  lgsmod  27255  lgsdirprm  27263  lgsdir  27264  lgsdi  27266  sltres  27594  nolt02olem  27626  nolt02o  27627  nogt01o  27628  nosupbnd1lem1  27640  nosupbnd1lem4  27643  nosupbnd1lem5  27644  nosupbnd1lem6  27645  noinfbnd1lem1  27655  noinfbnd1lem4  27658  noinfbnd1lem6  27660  noinfbnd2  27663  noetainflem3  27671  sltlpss  27832  cofsslt  27837  coinitsslt  27838  cofcutrtime  27846  addsass  27921  addsdi  28054  mulsass  28065  sltmul2  28070  norecdiv  28089  brbtwn2  28715  colinearalglem1  28716  colinearalg  28720  axcgrtr  28725  axcontlem2  28775  upgrewlkle2  29419  wlksoneq1eq2  29477  crctcshwlkn0lem5  29624  wspthsnwspthsnon  29726  lppthon  29960  upgriseupth  30016  4cyclusnfrgr  30101  numclwwlk1lem2foa  30163  numclwwlk5  30197  nvmul0or  30459  shless  31168  shlej1  31169  pjspansn  31386  kbmul  31764  homco2  31786  kbass2  31926  fnpreimac  32456  padct  32501  eliccelico  32545  elicoelioo  32546  iocinioc2  32547  difioo  32550  swrdrn2  32675  swrdrn3  32676  xrge0npcan  32750  isarchi2  32893  archiabl  32906  pidlnz  33087  lindssn  33093  ssmxidl  33187  mdetlap1  33427  zarclsiin  33472  pstmfval  33497  fmcncfil  33532  zrhnm  33570  qqhnm  33591  nexple  33628  volfiniune  33849  omsmeas  33943  eulerpartlemb  33988  probinc  34041  cndprob01  34055  signswmnd  34189  cvmsss2  34884  funsseq  35363  cgrtriv  35598  5segofs  35602  btwntriv2  35608  btwnxfr  35652  segcon2  35701  brsegle2  35705  seglelin  35712  outsideofeu  35727  lindsenlbs  37088  mblfinlem2  37131  blbnd  37260  rrndstprj2  37304  zerdivemp1x  37420  lsmsat  38480  lsatfixedN  38481  lssat  38488  lkrlsp  38574  lshpkrlem4  38585  cvrcon3b  38749  leat3  38767  atlen0  38782  atnle  38789  atlatmstc  38791  atlatle  38792  cvlcvr1  38811  cvlsupr2  38815  hlsupr2  38860  hlrelat2  38876  cvrexchlem  38892  cvratlem  38894  lnnat  38900  atexchcvrN  38913  1cvratlt  38947  1cvrjat  38948  3atlem3  38958  3atlem7  38962  llni2  38985  atcvrlln2  38992  llnexatN  38994  llncmp  38995  2llnmat  38997  2at0mat0  38998  2atnelpln  39017  llncvrlpln2  39030  2lplnmN  39032  2llnmj  39033  lplncmp  39035  lplnexatN  39036  2llnjaN  39039  lvoli3  39050  islvol2aN  39065  4atlem3a  39070  4atlem4a  39072  4atlem4b  39073  4atlem11  39082  4atlem12  39085  lplncvrlvol2  39088  lvolcmp  39090  2lplnmj  39095  islinei  39213  linepmap  39248  lneq2at  39251  2llnma3r  39261  elpaddn0  39273  elpaddatriN  39276  elpaddat  39277  paddcom  39286  paddss1  39290  paddss2  39291  paddasslem6  39298  paddasslem7  39299  paddasslem10  39302  paddasslem15  39307  pmodlem2  39320  pmodl42N  39324  pmapjoin  39325  atmod1i1m  39331  llnmod1i2  39333  llnexchb2lem  39341  polcon2bN  39393  pclfinclN  39423  poml4N  39426  poml6N  39428  osumcllem11N  39439  osumclN  39440  pmapojoinN  39441  pexmidlem2N  39444  pexmidlem3N  39445  pexmidlem4N  39446  pexmidlem6N  39448  pexmidlem7N  39449  pl42lem2N  39453  pl42lem3N  39454  pl42lem4N  39455  pl42N  39456  lhpexle3lem  39484  lhpmcvr3  39498  lhp2at0nle  39508  lhprelat3N  39513  lauteq  39568  lautco  39570  ltrncoidN  39601  ltrneq2  39621  ltrnnidn  39647  ltrnideq  39648  trlnle  39659  cdlemc  39670  cdlemd4  39674  cdlemd5  39675  cdlemd9  39679  cdlemd  39680  ltrneq3  39681  cdlemefrs29pre00  39868  cdlemefrs29cpre1  39871  cdlemefrs29clN  39872  cdlemefrs32fva  39873  cdlemefr29exN  39875  cdlemefr27cl  39876  cdlemefs27cl  39886  cdlemefs32sn1aw  39887  cdleme32fva  39910  cdleme32d  39917  cdleme32f  39919  cdleme32le  39920  cdleme40n  39941  cdleme41snaw  39949  cdleme17d3  39969  cdleme48fvg  39973  cdlemeg46fvcl  39979  cdlemeg46fgN  40007  cdleme48fgv  40011  ltrniotavalbN  40057  cdlemb3  40079  cdlemg15  40129  cdlemg17dN  40136  trlco  40200  cdlemg44b  40205  ltrncom  40211  trljco  40213  tendococl  40245  tendoplcl  40254  tendoplcom  40255  tendotr  40303  cdlemk36  40386  cdlemk35s-id  40411  cdlemk39s-id  40413  cdlemk19x  40416  cdlemk53b  40429  cdlemk55  40434  cdlemk35u  40437  cdlemk55u  40439  cdlemk39u  40441  cdlemk19u  40443  cdlemk56  40444  tendoex  40448  cdleml5N  40453  dihord2pre  40698  dihord6apre  40729  dihord5b  40732  dihord5apre  40735  dihord  40737  dihmeetlem1N  40763  dihmeetlem2N  40772  dihglbcpreN  40773  dihmeetbN  40776  dihmeetlem4preN  40779  dihmeetlem5  40781  dihmeetlem6  40782  dihmeetlem7N  40783  dihmeetlem10N  40789  dihmeetlem11N  40790  dihmeetlem12N  40791  dihmeetlem13N  40792  dihmeetlem15N  40794  dihmeetlem17N  40796  dihmeetlem18N  40797  dihmeetlem19N  40798  dihmeetALTN  40800  dih1dimatlem0  40801  dihlspsnssN  40805  dvh3dim2  40921  sticksstones1  41618  sticksstones2  41619  sticksstones12  41630  aks6d1c6isolem1  41646  dvdsexpnn  41900  resubcan2  41943  mzpsubst  42168  diophrw  42179  eldioph2lem1  42180  rencldnfi  42241  pellexlem2  42250  pellqrexplicit  42297  infmrgelbi  42298  rmxycomplete  42338  congadd  42387  acongeq  42404  jm2.19  42414  jm2.22  42416  jm2.20nn  42418  jm2.25lem1  42419  jm2.27  42429  jm3.1  42441  lmhmlnmsplit  42511  pwssplit4  42513  hbtlem2  42548  dgraa0p  42573  proot1hash  42623  iocunico  42639  cantnf2  42754  dflim5  42758  omcl2  42762  tfsconcatrn  42771  nadd2rabex  42815  relexpxpmin  43147  brtrclfv2  43157  ntrclsk3  43500  grur1cld  43669  ismnu  43698  suprnmpt  44547  wessf1ornlem  44558  choicefi  44573  supxrgere  44715  supxrgelem  44719  supxrge  44720  infleinflem2  44753  snunioo1  44897  iccintsng  44908  fmul01  44968  lptre2pt  45028  0ellimcdiv  45037  fnlimfvre  45062  limsupmnfuzlem  45114  climisp  45134  limsupgtlem  45165  ibliccsinexp  45339  iblioosinexp  45341  volioc  45360  iblspltprt  45361  stoweidlem20  45408  stoweidlem22  45410  stoweidlem34  45422  stoweidlem44  45432  stoweidlem60  45448  wallispilem3  45455  fourierdlem42  45537  fourierdlem51  45545  fourierdlem54  45548  fourierdlem87  45581  fourierdlem97  45591  ioorrnopnlem  45692  sge0seq  45834  hoicvr  45936  fsupdm  46230  finfdm  46234  funfocofob  46458  imasetpreimafvbijlemfv  46742  fprmappr  47409  lincresunit3lem3  47542  lindssnlvec  47554  rrx2linesl  47816  line2  47825  itsclc0lem3  47831  itsclc0yqsollem1  47835  itscnhlc0xyqsol  47838  itschlc0xyqsol1  47839  itsclc0  47844  itscnhlinecirc02plem2  47856  itscnhlinecirc02plem3  47857