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  4419  predtrss  6311  frpomin  6329  f1prex  7276  fcofo  7280  soisores  7319  weniso  7346  knatar  7349  ofmpteq  7692  funelss  8044  frrlem10  8292  fprlem1  8297  smocdmdom  8380  nnmord  8642  nnmword  8643  naddasslem1  8704  naddasslem2  8705  difsnen  9065  mapunen  9158  ac6sfi  9290  fipreima  9368  wemaplem2  9559  wemapso2lem  9564  ttrclselem2  9738  en2eqpr  10019  indcardi  10053  acndom  10063  fodomfi2  10072  infmap2  10229  cflim2  10275  coftr  10285  infpssrlem4  10318  fin23lem11  10329  fincssdom  10335  isf32lem9  10373  fin1a2lem9  10420  gchpwdom  10682  gruima  10814  prpssnq  11002  distrlem4pr  11038  dedekind  11396  addcan  11417  addcan2  11418  divmulass  11917  supmul1  12209  uzsupss  12954  xaddass  13263  xleadd1a  13267  xlesubadd  13277  xmulasslem3  13300  xmulass  13301  xadddilem  13308  xadddi  13309  ixxun  13376  icoshftf1o  13489  snunioc  13495  difelfzle  13656  fzo1fzo0n0  13729  ssfzoulel  13774  modmuladd  13929  modifeq2int  13949  modaddmulmod  13954  modsubdir  13956  ltexp2a  14182  leexp2  14187  ltexp2r  14189  exple1  14193  expnlbnd2  14250  mulsubdivbinom2  14278  hashtpg  14501  ccatass  14604  ccatopth  14732  pfxccatin12lem2a  14743  pfxccat3  14750  cshinj  14827  2cshw  14829  s2f1o  14933  limsupgre  15495  addcn2  15608  mulcn2  15610  binomrisefac  16056  bpolydif  16069  dvdsmodexp  16278  modmulconst  16305  dvdsexp2im  16344  dvdsmod  16346  sadass  16488  gcdass  16564  rplpwr  16575  rpmulgcd2  16673  rpdvds  16677  rpexp  16739  prmdiveq  16803  hashgcdlem  16805  coprimeprodsq  16826  coprimeprodsq2  16827  pythagtriplem3  16836  pcdvdsb  16887  pcgcd1  16895  dvdsprmpweq  16902  pcbc  16918  0ram  17038  ramz2  17042  ramub1lem1  17044  mremre  17614  mrieqv2d  17649  lubun  18523  isnsgrp  18699  issubmnd  18737  frmdss2  18839  submefmnd  18871  sgrp2rid2ex  18903  mulgnn0p1  19066  mulgnnsubcl  19067  mulgneg  19073  mulgdirlem  19086  nmzsubg  19146  ghmmulg  19209  pmtrfv  19431  pmtrmvd  19435  pmtrfb  19444  odmodnn0  19519  oddvdsnn0  19523  odnncl  19524  odmod  19525  oddvds  19526  odeq  19529  odmulgid  19533  odmulg  19535  odmulgeq  19536  odbezout  19537  odf1o1  19551  odf1o2  19552  odngen  19556  odcau  19583  pgpssslw  19593  fislw  19604  lsmless1x  19623  lsmless2x  19624  lsmsubm  19632  lsmmod  19654  lsmmod2  19655  efgsfo  19718  cntzcmn  19819  odadd1  19827  odadd2  19828  odadd  19829  lsmcomx  19835  prdscmnd  19840  gsumconst  19913  ring1eq0  20256  cntzsubrng  20525  cntzsubr  20564  isabvd  20770  rmodislmod  20885  lspss  20939  0lmhm  20996  reslmhm2  21009  pwssplit0  21014  pwssplit1  21015  lbspss  21038  lspfixed  21087  lsmcv  21100  lspsnat  21104  2idlcpblrng  21230  cnfldfunALT  21328  cnfldfunALTOLD  21341  xrsdsreclblem  21378  obselocv  21686  frlmsplit2  21731  frlmsslss2  21733  frlmup4  21759  lindff1  21778  lsslindf  21788  lsslinds  21789  islindf4  21796  issubassa  21825  aspss  21835  coe1subfv  22201  coe1tm  22208  mpomatmul  22382  mamutpos  22394  submaval  22517  mdetdiag  22535  mdetunilem1  22548  mdetunilem3  22550  mdetunilem9  22556  mdetmul  22559  maducoeval2  22576  madurid  22580  minmar1val  22584  cramer  22627  cpmatel2  22649  m2cpm  22677  decpmatmul  22708  pmatcollpw1lem2  22711  pmatcollpw1  22712  pmatcollpw2lem  22713  pm2mpcl  22733  mply1topmatcl  22741  mp2pm2mplem2  22743  mp2pm2mplem4  22745  pm2mpghmlem2  22748  pm2mpghmlem1  22749  cayhamlem2  22820  neiint  23040  topssnei  23060  cnrest2  23222  cnprest2  23226  cnt0  23282  cnt1  23286  cnhaus  23290  cncmp  23328  fiuncmp  23340  sscmp  23341  hauscmp  23343  cnconn  23358  unconn  23365  comppfsc  23468  kgen2ss  23491  ptpjopn  23548  ptrescn  23575  qtopss  23651  kqfvima  23666  r0cld  23674  cmphaushmeo  23736  fbssint  23774  fbasrn  23820  filuni  23821  ufilmax  23843  fin1aufil  23868  fmf  23881  fmss  23882  rnelfmlem  23888  rnelfm  23889  fmufil  23895  fmco  23897  flimss2  23908  flimss1  23909  flimrest  23919  cnpflf2  23936  cnpflf  23937  flfcnp  23940  lmflf  23941  supnfcls  23956  fclsss1  23958  fclsss2  23959  cnpfcfi  23976  subgntr  24043  opnsubg  24044  cldsubg  24047  ustuqtop1  24178  ucncn  24221  bldisj  24335  blgt0  24336  bl2in  24337  blss2ps  24340  blss2  24341  xbln0  24351  blssps  24361  blss  24362  lpbl  24440  blcld  24442  blcls  24443  stdbdmopn  24455  metcnp2  24479  txmetcnp  24484  blval2  24499  restmetu  24507  nmoix  24666  nmoi2  24667  nmoeq0  24673  nmotri  24676  metdsge  24787  metds0  24788  metdseq0  24792  icoopnst  24885  iccpnfhmeo  24892  xrhmeo  24893  nmhmcn  25069  cphsqrtcl2  25136  cphsqrtcl3  25137  fmcfil  25222  bcthlem5  25278  cmetcusp1  25303  cssbn  25325  pjth  25389  ovolunnul  25451  volun  25496  voliunlem2  25502  itg2const  25691  iblconst  25769  itgconst  25770  limcvallem  25822  dvcnp2  25871  dvcnp2OLD  25872  dvcn  25873  deg1mul3le  26072  deg1tmle  26073  idomrootle  26128  ig1pdvds  26135  coe11  26208  dgrmulc  26227  dvply1  26241  aaliou2  26298  efcvx  26409  tanord  26497  logdivlti  26579  logccv  26622  recxpcl  26634  cxplea  26655  cxple2a  26658  ang180  26774  isosctrlem2  26779  cxp2lim  26937  amgm  26951  muval1  27093  dvdssqf  27098  mumullem2  27140  bcmono  27238  lgsneg  27282  lgsmod  27284  lgsdirprm  27292  lgsdir  27293  lgsdi  27295  sltres  27624  nolt02olem  27656  nolt02o  27657  nogt01o  27658  nosupbnd1lem1  27670  nosupbnd1lem4  27673  nosupbnd1lem5  27674  nosupbnd1lem6  27675  noinfbnd1lem1  27685  noinfbnd1lem4  27688  noinfbnd1lem6  27690  noinfbnd2  27693  noetainflem3  27701  sltlpss  27862  cofsslt  27869  coinitsslt  27870  cofcutrtime  27878  addsass  27955  addsdi  28098  mulsass  28109  sltmul2  28114  norecdiv  28133  brbtwn2  28830  colinearalglem1  28831  colinearalg  28835  axcgrtr  28840  axcontlem2  28890  upgrewlkle2  29532  wlksoneq1eq2  29590  crctcshwlkn0lem5  29742  wspthsnwspthsnon  29844  lppthon  30078  upgriseupth  30134  4cyclusnfrgr  30219  numclwwlk1lem2foa  30281  numclwwlk5  30315  nvmul0or  30577  shless  31286  shlej1  31287  pjspansn  31504  kbmul  31882  homco2  31904  kbass2  32044  fnpreimac  32595  padct  32643  eliccelico  32700  elicoelioo  32701  iocinioc2  32702  difioo  32705  nexple  32769  swrdrn2  32876  swrdrn3  32877  xrge0npcan  32961  isarchi2  33129  archiabl  33142  pidlnz  33337  lindssn  33339  ssmxidl  33435  mdetlap1  33803  zarclsiin  33848  pstmfval  33873  fmcncfil  33908  zrhnm  33944  qqhnm  33967  volfiniune  34207  omsmeas  34301  eulerpartlemb  34346  probinc  34399  cndprob01  34413  signswmnd  34535  cvmsss2  35242  funsseq  35731  cgrtriv  35966  5segofs  35970  btwntriv2  35976  btwnxfr  36020  segcon2  36069  brsegle2  36073  seglelin  36080  outsideofeu  36095  weiunpo  36429  weiunfr  36431  weiunse  36432  lindsenlbs  37585  mblfinlem2  37628  blbnd  37757  rrndstprj2  37801  zerdivemp1x  37917  lsmsat  38972  lsatfixedN  38973  lssat  38980  lkrlsp  39066  lshpkrlem4  39077  cvrcon3b  39241  leat3  39259  atlen0  39274  atnle  39281  atlatmstc  39283  atlatle  39284  cvlcvr1  39303  cvlsupr2  39307  hlsupr2  39352  hlrelat2  39368  cvrexchlem  39384  cvratlem  39386  lnnat  39392  atexchcvrN  39405  1cvratlt  39439  1cvrjat  39440  3atlem3  39450  3atlem7  39454  llni2  39477  atcvrlln2  39484  llnexatN  39486  llncmp  39487  2llnmat  39489  2at0mat0  39490  2atnelpln  39509  llncvrlpln2  39522  2lplnmN  39524  2llnmj  39525  lplncmp  39527  lplnexatN  39528  2llnjaN  39531  lvoli3  39542  islvol2aN  39557  4atlem3a  39562  4atlem4a  39564  4atlem4b  39565  4atlem11  39574  4atlem12  39577  lplncvrlvol2  39580  lvolcmp  39582  2lplnmj  39587  islinei  39705  linepmap  39740  lneq2at  39743  2llnma3r  39753  elpaddn0  39765  elpaddatriN  39768  elpaddat  39769  paddcom  39778  paddss1  39782  paddss2  39783  paddasslem6  39790  paddasslem7  39791  paddasslem10  39794  paddasslem15  39799  pmodlem2  39812  pmodl42N  39816  pmapjoin  39817  atmod1i1m  39823  llnmod1i2  39825  llnexchb2lem  39833  polcon2bN  39885  pclfinclN  39915  poml4N  39918  poml6N  39920  osumcllem11N  39931  osumclN  39932  pmapojoinN  39933  pexmidlem2N  39936  pexmidlem3N  39937  pexmidlem4N  39938  pexmidlem6N  39940  pexmidlem7N  39941  pl42lem2N  39945  pl42lem3N  39946  pl42lem4N  39947  pl42N  39948  lhpexle3lem  39976  lhpmcvr3  39990  lhp2at0nle  40000  lhprelat3N  40005  lauteq  40060  lautco  40062  ltrncoidN  40093  ltrneq2  40113  ltrnnidn  40139  ltrnideq  40140  trlnle  40151  cdlemc  40162  cdlemd4  40166  cdlemd5  40167  cdlemd9  40171  cdlemd  40172  ltrneq3  40173  cdlemefrs29pre00  40360  cdlemefrs29cpre1  40363  cdlemefrs29clN  40364  cdlemefrs32fva  40365  cdlemefr29exN  40367  cdlemefr27cl  40368  cdlemefs27cl  40378  cdlemefs32sn1aw  40379  cdleme32fva  40402  cdleme32d  40409  cdleme32f  40411  cdleme32le  40412  cdleme40n  40433  cdleme41snaw  40441  cdleme17d3  40461  cdleme48fvg  40465  cdlemeg46fvcl  40471  cdlemeg46fgN  40499  cdleme48fgv  40503  ltrniotavalbN  40549  cdlemb3  40571  cdlemg15  40621  cdlemg17dN  40628  trlco  40692  cdlemg44b  40697  ltrncom  40703  trljco  40705  tendococl  40737  tendoplcl  40746  tendoplcom  40747  tendotr  40795  cdlemk36  40878  cdlemk35s-id  40903  cdlemk39s-id  40905  cdlemk19x  40908  cdlemk53b  40921  cdlemk55  40926  cdlemk35u  40929  cdlemk55u  40931  cdlemk39u  40933  cdlemk19u  40935  cdlemk56  40936  tendoex  40940  cdleml5N  40945  dihord2pre  41190  dihord6apre  41221  dihord5b  41224  dihord5apre  41227  dihord  41229  dihmeetlem1N  41255  dihmeetlem2N  41264  dihglbcpreN  41265  dihmeetbN  41268  dihmeetlem4preN  41271  dihmeetlem5  41273  dihmeetlem6  41274  dihmeetlem7N  41275  dihmeetlem10N  41281  dihmeetlem11N  41282  dihmeetlem12N  41283  dihmeetlem13N  41284  dihmeetlem15N  41286  dihmeetlem17N  41288  dihmeetlem18N  41289  dihmeetlem19N  41290  dihmeetALTN  41292  dih1dimatlem0  41293  dihlspsnssN  41297  dvh3dim2  41413  sticksstones1  42105  sticksstones2  42106  sticksstones12  42117  aks6d1c6isolem1  42133  dvdsexpnn  42329  resubcan2  42378  mzpsubst  42718  diophrw  42729  eldioph2lem1  42730  rencldnfi  42791  pellexlem2  42800  pellqrexplicit  42847  infmrgelbi  42848  rmxycomplete  42888  congadd  42937  acongeq  42954  jm2.19  42964  jm2.22  42966  jm2.20nn  42968  jm2.25lem1  42969  jm2.27  42979  jm3.1  42991  lmhmlnmsplit  43058  pwssplit4  43060  hbtlem2  43095  dgraa0p  43120  proot1hash  43166  iocunico  43182  cantnf2  43296  dflim5  43300  omcl2  43304  tfsconcatrn  43313  nadd2rabex  43357  relexpxpmin  43688  brtrclfv2  43698  ntrclsk3  44041  grur1cld  44204  ismnu  44233  suprnmpt  45146  wessf1ornlem  45157  choicefi  45172  supxrgere  45308  supxrgelem  45312  supxrge  45313  infleinflem2  45346  snunioo1  45489  iccintsng  45500  fmul01  45557  lptre2pt  45617  0ellimcdiv  45626  fnlimfvre  45651  limsupmnfuzlem  45703  climisp  45723  limsupgtlem  45754  ibliccsinexp  45928  iblioosinexp  45930  volioc  45949  iblspltprt  45950  stoweidlem20  45997  stoweidlem22  45999  stoweidlem34  46011  stoweidlem44  46021  stoweidlem60  46037  wallispilem3  46044  fourierdlem42  46126  fourierdlem51  46134  fourierdlem54  46137  fourierdlem87  46170  fourierdlem97  46180  ioorrnopnlem  46281  sge0seq  46423  hoicvr  46525  fsupdm  46819  finfdm  46823  3f1oss1  47052  funfocofob  47055  imasetpreimafvbijlemfv  47364  uhgrimisgrgric  47892  uhgrimgrlim  47947  fprmappr  48268  lincresunit3lem3  48398  lindssnlvec  48410  rrx2linesl  48671  line2  48680  itsclc0lem3  48686  itsclc0yqsollem1  48690  itscnhlc0xyqsol  48693  itschlc0xyqsol1  48694  itsclc0  48699  itscnhlinecirc02plem2  48711  itscnhlinecirc02plem3  48712  setc1onsubc  49427