Theorem simpl3 1206

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simpl13  1263  simpl23  1266  simpl33  1269  simp1l3  1281  simp2l3  1287  simp3l3  1293  3anandirs  1492  2nreu  4397  predtrss  6305  frpomin  6323  f1prex  7264  fcofo  7268  soisores  7307  weniso  7334  knatar  7337  ofmpteq  7679  funelss  8024  frrlem10  8271  fprlem1  8276  smocdmdom  8334  nnmord  8597  nnmword  8598  naddasslem1  8660  naddasslem2  8661  difsnen  9027  mapunen  9114  ac6sfi  9224  fipreima  9298  wemaplem2  9492  wemapso2lem  9497  ttrclselem2  9678  en2eqpr  9960  indcardi  9994  acndom  10004  fodomfi2  10013  infmap2  10170  cflim2  10217  coftr  10227  infpssrlem4  10260  fin23lem11  10271  fincssdom  10277  isf32lem9  10315  fin1a2lem9  10362  gchpwdom  10625  gruima  10757  prpssnq  10945  distrlem4pr  10981  dedekind  11343  addcan  11364  addcan2  11365  divmulass  11865  supmul1  12158  uzsupss  12938  xaddass  13249  xleadd1a  13253  xlesubadd  13263  xmulasslem3  13286  xmulass  13287  xadddilem  13294  xadddi  13295  ixxun  13362  icoshftf1o  13475  snunioc  13481  difelfzle  13643  fzo1fzo0n0  13718  ssfzoulel  13763  modmuladd  13923  modifeq2int  13943  modaddmulmod  13948  modsubdir  13950  ltexp2a  14176  leexp2  14181  ltexp2r  14183  exple1  14187  expnlbnd2  14244  mulsubdivbinom2  14272  hashtpg  14495  ccatass  14599  ccatopth  14726  pfxccatin12lem2a  14737  pfxccat3  14744  cshinj  14821  2cshw  14823  s2f1o  14926  limsupgre  15491  addcn2  15604  mulcn2  15606  binomrisefac  16055  bpolydif  16068  dvdsmodexp  16277  modmulconst  16305  dvdsexp2im  16344  dvdsmod  16346  sadass  16488  gcdass  16564  rplpwr  16575  rpmulgcd2  16673  rpdvds  16677  rpexp  16740  prmdiveq  16804  hashgcdlem  16806  coprimeprodsq  16827  coprimeprodsq2  16828  pythagtriplem3  16837  pcdvdsb  16888  pcgcd1  16896  dvdsprmpweq  16903  pcbc  16919  0ram  17039  ramz2  17043  ramub1lem1  17045  mremre  17615  mrieqv2d  17654  lubun  18530  isnsgrp  18740  issubmnd  18778  frmdss2  18880  submefmnd  18912  sgrp2rid2ex  18947  mulgnn0p1  19110  mulgnnsubcl  19111  mulgneg  19117  mulgdirlem  19130  nmzsubg  19189  ghmmulg  19251  pmtrfv  19475  pmtrmvd  19479  pmtrfb  19488  odmodnn0  19563  oddvdsnn0  19567  odnncl  19568  odmod  19569  oddvds  19570  odeq  19573  odmulgid  19577  odmulg  19579  odmulgeq  19580  odbezout  19581  odf1o1  19595  odf1o2  19596  odngen  19600  odcau  19627  pgpssslw  19637  fislw  19648  lsmless1x  19667  lsmless2x  19668  lsmsubm  19676  lsmmod  19698  lsmmod2  19699  efgsfo  19762  cntzcmn  19863  odadd1  19871  odadd2  19872  odadd  19873  lsmcomx  19879  prdscmnd  19884  gsumconst  19957  ring1eq0  20327  cntzsubrng  20596  cntzsubr  20635  isabvd  20841  rmodislmod  20977  lspss  21031  0lmhm  21087  reslmhm2  21100  pwssplit0  21105  pwssplit1  21106  lbspss  21129  lspfixed  21178  lsmcv  21191  lspsnat  21195  2idlcpblrng  21321  cnfldfunALT  21419  xrsdsreclblem  21445  obselocv  21760  frlmsplit2  21805  frlmsslss2  21807  frlmup4  21833  lindff1  21852  lsslindf  21862  lsslinds  21863  islindf4  21870  issubassa  21899  aspss  21908  coe1subfv  22309  coe1tm  22316  mpomatmul  22486  mamutpos  22498  submaval  22621  mdetdiag  22639  mdetunilem1  22652  mdetunilem3  22654  mdetunilem9  22660  mdetmul  22663  maducoeval2  22680  madurid  22684  minmar1val  22688  cramer  22731  cpmatel2  22753  m2cpm  22781  decpmatmul  22812  pmatcollpw1lem2  22815  pmatcollpw1  22816  pmatcollpw2lem  22817  pm2mpcl  22837  mply1topmatcl  22845  mp2pm2mplem2  22847  mp2pm2mplem4  22849  pm2mpghmlem2  22852  pm2mpghmlem1  22853  cayhamlem2  22924  neiint  23144  topssnei  23164  cnrest2  23326  cnprest2  23330  cnt0  23386  cnt1  23390  cnhaus  23394  cncmp  23432  fiuncmp  23444  sscmp  23445  hauscmp  23447  cnconn  23462  unconn  23469  comppfsc  23572  kgen2ss  23595  ptpjopn  23652  ptrescn  23679  qtopss  23755  kqfvima  23770  r0cld  23778  cmphaushmeo  23840  fbssint  23878  fbasrn  23924  filuni  23925  ufilmax  23947  fin1aufil  23972  fmf  23985  fmss  23986  rnelfmlem  23992  rnelfm  23993  fmufil  23999  fmco  24001  flimss2  24012  flimss1  24013  flimrest  24023  cnpflf2  24040  cnpflf  24041  flfcnp  24044  lmflf  24045  supnfcls  24060  fclsss1  24062  fclsss2  24063  cnpfcfi  24080  subgntr  24147  opnsubg  24148  cldsubg  24151  ustuqtop1  24281  ucncn  24324  bldisj  24438  blgt0  24439  bl2in  24440  blss2ps  24443  blss2  24444  xbln0  24454  blssps  24464  blss  24465  lpbl  24543  blcld  24545  blcls  24546  stdbdmopn  24558  metcnp2  24582  txmetcnp  24587  blval2  24602  restmetu  24610  nmoix  24769  nmoi2  24770  nmoeq0  24776  nmotri  24779  metdsge  24890  metds0  24891  metdseq0  24895  icoopnst  24981  iccpnfhmeo  24987  xrhmeo  24988  nmhmcn  25162  cphsqrtcl2  25228  cphsqrtcl3  25229  fmcfil  25314  bcthlem5  25370  cmetcusp1  25395  cssbn  25417  pjth  25481  ovolunnul  25542  volun  25587  voliunlem2  25593  itg2const  25782  iblconst  25860  itgconst  25861  limcvallem  25913  dvcnp2  25962  dvcn  25963  deg1mul3le  26157  deg1tmle  26158  idomrootle  26213  ig1pdvds  26220  coe11  26293  dgrmulc  26311  dvply1  26325  aaliou2  26381  efcvx  26489  tanord  26580  logdivlti  26662  logccv  26705  recxpcl  26717  cxplea  26738  cxple2a  26741  ang180  26856  isosctrlem2  26861  cxp2lim  27018  amgm  27032  muval1  27174  dvdssqf  27179  mumullem2  27221  bcmono  27318  lgsneg  27362  lgsmod  27364  lgsdirprm  27372  lgsdir  27373  lgsdi  27375  ltsres  27703  nolt02olem  27735  nolt02o  27736  nogt01o  27737  nosupbnd1lem1  27749  nosupbnd1lem4  27752  nosupbnd1lem5  27753  nosupbnd1lem6  27754  noinfbnd1lem1  27764  noinfbnd1lem4  27767  noinfbnd1lem6  27769  noinfbnd2  27772  noetainflem3  27780  ltslpss  27978  cofslts  27988  coinitslts  27989  cofcutrtime  27997  addsass  28075  addsdi  28225  mulsass  28236  ltmuls2  28241  norecdiv  28260  z12bdaylem  28554  brbtwn2  29052  colinearalglem1  29053  colinearalg  29057  axcgrtr  29062  axcontlem2  29112  upgrewlkle2  29753  wlksoneq1eq2  29809  crctcshwlkn0lem5  29960  wspthsnwspthsnon  30062  lppthon  30299  upgriseupth  30355  4cyclusnfrgr  30440  numclwwlk1lem2foa  30502  numclwwlk5  30536  nvmul0or  30799  shless  31508  shlej1  31509  pjspansn  31726  kbmul  32104  homco2  32126  kbass2  32266  fnpreimac  32822  padct  32870  eliccelico  32929  elicoelioo  32930  iocinioc2  32931  difioo  32934  nexple  32996  swrdrn2  33093  swrdrn3  33094  xrge0npcan  33159  isarchi2  33326  archiabl  33339  pidlnz  33523  lindssn  33525  ssmxidl  33623  mdetlap1  34084  zarclsiin  34129  pstmfval  34154  fmcncfil  34189  zrhnm  34225  qqhnm  34248  volfiniune  34488  omsmeas  34581  eulerpartlemb  34626  probinc  34679  cndprob01  34693  signswmnd  34815  cvmsss2  35588  funsseq  36082  cgrtriv  36316  5segofs  36320  btwntriv2  36326  btwnxfr  36370  segcon2  36419  brsegle2  36423  seglelin  36430  outsideofeu  36445  weiunpo  36789  weiunfr  36791  weiunse  36792  lindsenlbs  38078  mblfinlem2  38121  blbnd  38250  rrndstprj2  38294  zerdivemp1x  38410  lsmsat  39596  lsatfixedN  39597  lssat  39604  lkrlsp  39690  lshpkrlem4  39701  cvrcon3b  39865  leat3  39883  atlen0  39898  atnle  39905  atlatmstc  39907  atlatle  39908  cvlcvr1  39927  cvlsupr2  39931  hlsupr2  39975  hlrelat2  39991  cvrexchlem  40007  cvratlem  40009  lnnat  40015  atexchcvrN  40028  1cvratlt  40062  1cvrjat  40063  3atlem3  40073  3atlem7  40077  llni2  40100  atcvrlln2  40107  llnexatN  40109  llncmp  40110  2llnmat  40112  2at0mat0  40113  2atnelpln  40132  llncvrlpln2  40145  2lplnmN  40147  2llnmj  40148  lplncmp  40150  lplnexatN  40151  2llnjaN  40154  lvoli3  40165  islvol2aN  40180  4atlem3a  40185  4atlem4a  40187  4atlem4b  40188  4atlem11  40197  4atlem12  40200  lplncvrlvol2  40203  lvolcmp  40205  2lplnmj  40210  islinei  40328  linepmap  40363  lneq2at  40366  2llnma3r  40376  elpaddn0  40388  elpaddatriN  40391  elpaddat  40392  paddcom  40401  paddss1  40405  paddss2  40406  paddasslem6  40413  paddasslem7  40414  paddasslem10  40417  paddasslem15  40422  pmodlem2  40435  pmodl42N  40439  pmapjoin  40440  atmod1i1m  40446  llnmod1i2  40448  llnexchb2lem  40456  polcon2bN  40508  pclfinclN  40538  poml4N  40541  poml6N  40543  osumcllem11N  40554  osumclN  40555  pmapojoinN  40556  pexmidlem2N  40559  pexmidlem3N  40560  pexmidlem4N  40561  pexmidlem6N  40563  pexmidlem7N  40564  pl42lem2N  40568  pl42lem3N  40569  pl42lem4N  40570  pl42N  40571  lhpexle3lem  40599  lhpmcvr3  40613  lhp2at0nle  40623  lhprelat3N  40628  lauteq  40683  lautco  40685  ltrncoidN  40716  ltrneq2  40736  ltrnnidn  40762  ltrnideq  40763  trlnle  40774  cdlemc  40785  cdlemd4  40789  cdlemd5  40790  cdlemd9  40794  cdlemd  40795  ltrneq3  40796  cdlemefrs29pre00  40983  cdlemefrs29cpre1  40986  cdlemefrs29clN  40987  cdlemefrs32fva  40988  cdlemefr29exN  40990  cdlemefr27cl  40991  cdlemefs27cl  41001  cdlemefs32sn1aw  41002  cdleme32fva  41025  cdleme32d  41032  cdleme32f  41034  cdleme32le  41035  cdleme40n  41056  cdleme41snaw  41064  cdleme17d3  41084  cdleme48fvg  41088  cdlemeg46fvcl  41094  cdlemeg46fgN  41122  cdleme48fgv  41126  ltrniotavalbN  41172  cdlemb3  41194  cdlemg15  41244  cdlemg17dN  41251  trlco  41315  cdlemg44b  41320  ltrncom  41326  trljco  41328  tendococl  41360  tendoplcl  41369  tendoplcom  41370  tendotr  41418  cdlemk36  41501  cdlemk35s-id  41526  cdlemk39s-id  41528  cdlemk19x  41531  cdlemk53b  41544  cdlemk55  41549  cdlemk35u  41552  cdlemk55u  41554  cdlemk39u  41556  cdlemk19u  41558  cdlemk56  41559  tendoex  41563  cdleml5N  41568  dihord2pre  41813  dihord6apre  41844  dihord5b  41847  dihord5apre  41850  dihord  41852  dihmeetlem1N  41878  dihmeetlem2N  41887  dihglbcpreN  41888  dihmeetbN  41891  dihmeetlem4preN  41894  dihmeetlem5  41896  dihmeetlem6  41897  dihmeetlem7N  41898  dihmeetlem10N  41904  dihmeetlem11N  41905  dihmeetlem12N  41906  dihmeetlem13N  41907  dihmeetlem15N  41909  dihmeetlem17N  41911  dihmeetlem18N  41912  dihmeetlem19N  41913  dihmeetALTN  41915  dih1dimatlem0  41916  dihlspsnssN  41920  dvh3dim2  42036  sticksstones1  42727  sticksstones2  42728  sticksstones12  42739  aks6d1c6isolem1  42755  dvdsexpnn  42906  resubcan2  42961  mzpsubst  43293  diophrw  43304  eldioph2lem1  43305  rencldnfi  43362  pellexlem2  43371  pellqrexplicit  43418  infmrgelbi  43419  rmxycomplete  43458  congadd  43507  acongeq  43524  jm2.19  43534  jm2.22  43536  jm2.20nn  43538  jm2.25lem1  43539  jm2.27  43549  jm3.1  43561  lmhmlnmsplit  43628  pwssplit4  43630  hbtlem2  43665  dgraa0p  43690  proot1hash  43736  iocunico  43752  cantnf2  43866  dflim5  43870  omcl2  43874  tfsconcatrn  43883  nadd2rabex  43927  relexpxpmin  44257  brtrclfv2  44267  ntrclsk3  44610  grur1cld  44772  ismnu  44801  suprnmpt  45716  wessf1ornlem  45727  choicefi  45741  supxrgere  45873  supxrgelem  45877  supxrge  45878  infleinflem2  45910  snunioo1  46052  iccintsng  46063  fmul01  46120  lptre2pt  46178  0ellimcdiv  46187  fnlimfvre  46212  limsupmnfuzlem  46264  climisp  46284  limsupgtlem  46315  ibliccsinexp  46489  iblioosinexp  46491  volioc  46510  iblspltprt  46511  stoweidlem20  46558  stoweidlem22  46560  stoweidlem34  46572  stoweidlem44  46582  stoweidlem60  46598  wallispilem3  46605  fourierdlem42  46687  fourierdlem51  46695  fourierdlem54  46698  fourierdlem87  46731  fourierdlem97  46741  ioorrnopnlem  46842  sge0seq  46984  hoicvr  47086  fsupdm  47380  finfdm  47384  3f1oss1  47633  funfocofob  47636  imasetpreimafvbijlemfv  47972  uhgrimisgrgric  48517  uhgrimgrlim  48573  fprmappr  48931  lincresunit3lem3  49060  lindssnlvec  49072  rrx2linesl  49329  line2  49338  itsclc0lem3  49344  itsclc0yqsollem1  49348  itscnhlc0xyqsol  49351  itschlc0xyqsol1  49352  itsclc0  49357  itscnhlinecirc02plem2  49369  itscnhlinecirc02plem3  49370  uptrlem1  49795  uptr2  49806  setc1onsubc  50187