Theorem simpl3 1193

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  simpl13  1250  simpl23  1253  simpl33  1256  simp1l3  1268  simp2l3  1274  simp3l3  1280  3anandirs  1472  2nreu  4406  predtrss  6281  frpomin  6299  f1prex  7235  fcofo  7239  soisores  7277  weniso  7304  knatar  7307  ofmpteq  7644  funelss  7984  frrlem10  8231  fprlem1  8236  smocdmdom  8319  nnmord  8584  nnmword  8585  naddasslem1  8645  naddasslem2  8646  difsnen  9004  mapunen  9097  ac6sfi  9238  fipreima  9309  wemaplem2  9492  wemapso2lem  9497  ttrclselem2  9671  en2eqpr  9952  indcardi  9986  acndom  9996  fodomfi2  10005  infmap2  10163  cflim2  10208  coftr  10218  infpssrlem4  10251  fin23lem11  10262  fincssdom  10268  isf32lem9  10306  fin1a2lem9  10353  gchpwdom  10615  gruima  10747  prpssnq  10935  distrlem4pr  10971  dedekind  11327  addcan  11348  addcan2  11349  divmulass  11845  supmul1  12133  uzsupss  12874  xaddass  13178  xleadd1a  13182  xlesubadd  13192  xmulasslem3  13215  xmulass  13216  xadddilem  13223  xadddi  13224  ixxun  13290  icoshftf1o  13401  snunioc  13407  difelfzle  13564  fzo1fzo0n0  13633  ssfzoulel  13676  modmuladd  13828  modifeq2int  13848  modaddmulmod  13853  modsubdir  13855  ltexp2a  14081  leexp2  14086  ltexp2r  14088  exple1  14091  expnlbnd2  14147  mulsubdivbinom2  14172  hashtpg  14396  ccatass  14488  ccatopth  14616  pfxccatin12lem2a  14627  pfxccat3  14634  cshinj  14711  2cshw  14713  s2f1o  14817  limsupgre  15375  addcn2  15488  mulcn2  15490  binomrisefac  15936  bpolydif  15949  dvdsmodexp  16155  modmulconst  16181  dvdsexp2im  16220  dvdsmod  16222  sadass  16362  gcdass  16439  rplpwr  16449  rpmulgcd2  16543  rpdvds  16547  rpexp  16609  prmdiveq  16669  hashgcdlem  16671  coprimeprodsq  16691  coprimeprodsq2  16692  pythagtriplem3  16701  pcdvdsb  16752  pcgcd1  16760  dvdsprmpweq  16767  pcbc  16783  0ram  16903  ramz2  16907  ramub1lem1  16909  mremre  17498  mrieqv2d  17533  lubun  18418  isnsgrp  18564  issubmnd  18597  frmdss2  18687  submefmnd  18719  sgrp2rid2ex  18751  mulgnn0p1  18901  mulgnnsubcl  18902  mulgneg  18908  mulgdirlem  18921  nmzsubg  18981  ghmmulg  19034  pmtrfv  19248  pmtrmvd  19252  pmtrfb  19261  odmodnn0  19336  oddvdsnn0  19340  odnncl  19341  odmod  19342  oddvds  19343  odeq  19346  odmulgid  19350  odmulg  19352  odmulgeq  19353  odbezout  19354  odf1o1  19368  odf1o2  19369  odngen  19373  odcau  19400  pgpssslw  19410  fislw  19421  lsmless1x  19440  lsmless2x  19441  lsmsubm  19449  lsmmod  19471  lsmmod2  19472  efgsfo  19535  cntzcmn  19632  odadd1  19640  odadd2  19641  odadd  19642  lsmcomx  19648  prdscmnd  19653  gsumconst  19725  ring1eq0  20028  cntzsubr  20305  isabvd  20335  rmodislmod  20447  rmodislmodOLD  20448  lspss  20502  0lmhm  20558  reslmhm2  20571  pwssplit0  20576  pwssplit1  20577  lbspss  20600  lspfixed  20648  lsmcv  20661  lspsnat  20665  cnfldfunALT  20846  xrsdsreclblem  20880  obselocv  21171  frlmsplit2  21216  frlmsslss2  21218  frlmup4  21244  lindff1  21263  lsslindf  21273  lsslinds  21274  islindf4  21281  issubassa  21309  aspss  21317  coe1subfv  21674  coe1tm  21681  mpomatmul  21832  mamutpos  21844  submaval  21967  mdetdiag  21985  mdetunilem1  21998  mdetunilem3  22000  mdetunilem9  22006  mdetmul  22009  maducoeval2  22026  madurid  22030  minmar1val  22034  cramer  22077  cpmatel2  22099  m2cpm  22127  decpmatmul  22158  pmatcollpw1lem2  22161  pmatcollpw1  22162  pmatcollpw2lem  22163  pm2mpcl  22183  mply1topmatcl  22191  mp2pm2mplem2  22193  mp2pm2mplem4  22195  pm2mpghmlem2  22198  pm2mpghmlem1  22199  cayhamlem2  22270  neiint  22492  topssnei  22512  cnrest2  22674  cnprest2  22678  cnt0  22734  cnt1  22738  cnhaus  22742  cncmp  22780  fiuncmp  22792  sscmp  22793  hauscmp  22795  cnconn  22810  unconn  22817  comppfsc  22920  kgen2ss  22943  ptpjopn  23000  ptrescn  23027  qtopss  23103  kqfvima  23118  r0cld  23126  cmphaushmeo  23188  fbssint  23226  fbasrn  23272  filuni  23273  ufilmax  23295  fin1aufil  23320  fmf  23333  fmss  23334  rnelfmlem  23340  rnelfm  23341  fmufil  23347  fmco  23349  flimss2  23360  flimss1  23361  flimrest  23371  cnpflf2  23388  cnpflf  23389  flfcnp  23392  lmflf  23393  supnfcls  23408  fclsss1  23410  fclsss2  23411  cnpfcfi  23428  subgntr  23495  opnsubg  23496  cldsubg  23499  ustuqtop1  23630  ucncn  23674  bldisj  23788  blgt0  23789  bl2in  23790  blss2ps  23793  blss2  23794  xbln0  23804  blssps  23814  blss  23815  lpbl  23896  blcld  23898  blcls  23899  stdbdmopn  23911  metcnp2  23935  txmetcnp  23940  blval2  23955  restmetu  23963  nmoix  24130  nmoi2  24131  nmoeq0  24137  nmotri  24140  metdsge  24249  metds0  24250  metdseq0  24254  icoopnst  24339  iccpnfhmeo  24345  xrhmeo  24346  nmhmcn  24520  cphsqrtcl2  24587  cphsqrtcl3  24588  fmcfil  24673  bcthlem5  24729  cmetcusp1  24754  cssbn  24776  pjth  24840  ovolunnul  24901  volun  24946  voliunlem2  24952  itg2const  25142  iblconst  25219  itgconst  25220  limcvallem  25272  dvcnp2  25321  dvcn  25322  deg1mul3le  25518  deg1tmle  25519  ig1pdvds  25578  coe11  25651  dgrmulc  25669  dvply1  25681  aaliou2  25737  efcvx  25845  tanord  25931  logdivlti  26012  logccv  26055  recxpcl  26067  cxplea  26088  cxple2a  26091  ang180  26201  isosctrlem2  26206  cxp2lim  26363  amgm  26377  muval1  26519  dvdssqf  26524  mumullem2  26566  bcmono  26662  lgsneg  26706  lgsmod  26708  lgsdirprm  26716  lgsdir  26717  lgsdi  26719  sltres  27047  nolt02olem  27079  nolt02o  27080  nogt01o  27081  nosupbnd1lem1  27093  nosupbnd1lem4  27096  nosupbnd1lem5  27097  nosupbnd1lem6  27098  noinfbnd1lem1  27108  noinfbnd1lem4  27111  noinfbnd1lem6  27113  noinfbnd2  27116  noetainflem3  27124  sltlpss  27279  cofsslt  27280  coinitsslt  27281  cofcutrtime  27289  addsass  27356  brbtwn2  27917  colinearalglem1  27918  colinearalg  27922  axcgrtr  27927  axcontlem2  27977  upgrewlkle2  28617  wlksoneq1eq2  28675  crctcshwlkn0lem5  28822  wspthsnwspthsnon  28924  lppthon  29158  upgriseupth  29214  4cyclusnfrgr  29299  numclwwlk1lem2foa  29361  numclwwlk5  29395  nvmul0or  29655  shless  30364  shlej1  30365  pjspansn  30582  kbmul  30960  homco2  30982  kbass2  31122  fnpreimac  31654  padct  31704  eliccelico  31748  elicoelioo  31749  iocinioc2  31750  difioo  31753  swrdrn2  31878  swrdrn3  31879  xrge0npcan  31955  isarchi2  32091  archiabl  32104  pidlnz  32236  lindssn  32238  ssmxidl  32315  mdetlap1  32496  zarclsiin  32541  pstmfval  32566  fmcncfil  32601  zrhnm  32639  qqhnm  32660  nexple  32697  volfiniune  32918  omsmeas  33012  eulerpartlemb  33057  probinc  33110  cndprob01  33124  signswmnd  33258  cvmsss2  33955  funsseq  34428  cgrtriv  34663  5segofs  34667  btwntriv2  34673  btwnxfr  34717  segcon2  34766  brsegle2  34770  seglelin  34777  outsideofeu  34792  lindsenlbs  36146  mblfinlem2  36189  blbnd  36319  rrndstprj2  36363  zerdivemp1x  36479  lsmsat  37543  lsatfixedN  37544  lssat  37551  lkrlsp  37637  lshpkrlem4  37648  cvrcon3b  37812  leat3  37830  atlen0  37845  atnle  37852  atlatmstc  37854  atlatle  37855  cvlcvr1  37874  cvlsupr2  37878  hlsupr2  37923  hlrelat2  37939  cvrexchlem  37955  cvratlem  37957  lnnat  37963  atexchcvrN  37976  1cvratlt  38010  1cvrjat  38011  3atlem3  38021  3atlem7  38025  llni2  38048  atcvrlln2  38055  llnexatN  38057  llncmp  38058  2llnmat  38060  2at0mat0  38061  2atnelpln  38080  llncvrlpln2  38093  2lplnmN  38095  2llnmj  38096  lplncmp  38098  lplnexatN  38099  2llnjaN  38102  lvoli3  38113  islvol2aN  38128  4atlem3a  38133  4atlem4a  38135  4atlem4b  38136  4atlem11  38145  4atlem12  38148  lplncvrlvol2  38151  lvolcmp  38153  2lplnmj  38158  islinei  38276  linepmap  38311  lneq2at  38314  2llnma3r  38324  elpaddn0  38336  elpaddatriN  38339  elpaddat  38340  paddcom  38349  paddss1  38353  paddss2  38354  paddasslem6  38361  paddasslem7  38362  paddasslem10  38365  paddasslem15  38370  pmodlem2  38383  pmodl42N  38387  pmapjoin  38388  atmod1i1m  38394  llnmod1i2  38396  llnexchb2lem  38404  polcon2bN  38456  pclfinclN  38486  poml4N  38489  poml6N  38491  osumcllem11N  38502  osumclN  38503  pmapojoinN  38504  pexmidlem2N  38507  pexmidlem3N  38508  pexmidlem4N  38509  pexmidlem6N  38511  pexmidlem7N  38512  pl42lem2N  38516  pl42lem3N  38517  pl42lem4N  38518  pl42N  38519  lhpexle3lem  38547  lhpmcvr3  38561  lhp2at0nle  38571  lhprelat3N  38576  lauteq  38631  lautco  38633  ltrncoidN  38664  ltrneq2  38684  ltrnnidn  38710  ltrnideq  38711  trlnle  38722  cdlemc  38733  cdlemd4  38737  cdlemd5  38738  cdlemd9  38742  cdlemd  38743  ltrneq3  38744  cdlemefrs29pre00  38931  cdlemefrs29cpre1  38934  cdlemefrs29clN  38935  cdlemefrs32fva  38936  cdlemefr29exN  38938  cdlemefr27cl  38939  cdlemefs27cl  38949  cdlemefs32sn1aw  38950  cdleme32fva  38973  cdleme32d  38980  cdleme32f  38982  cdleme32le  38983  cdleme40n  39004  cdleme41snaw  39012  cdleme17d3  39032  cdleme48fvg  39036  cdlemeg46fvcl  39042  cdlemeg46fgN  39070  cdleme48fgv  39074  ltrniotavalbN  39120  cdlemb3  39142  cdlemg15  39192  cdlemg17dN  39199  trlco  39263  cdlemg44b  39268  ltrncom  39274  trljco  39276  tendococl  39308  tendoplcl  39317  tendoplcom  39318  tendotr  39366  cdlemk36  39449  cdlemk35s-id  39474  cdlemk39s-id  39476  cdlemk19x  39479  cdlemk53b  39492  cdlemk55  39497  cdlemk35u  39500  cdlemk55u  39502  cdlemk39u  39504  cdlemk19u  39506  cdlemk56  39507  tendoex  39511  cdleml5N  39516  dihord2pre  39761  dihord6apre  39792  dihord5b  39795  dihord5apre  39798  dihord  39800  dihmeetlem1N  39826  dihmeetlem2N  39835  dihglbcpreN  39836  dihmeetbN  39839  dihmeetlem4preN  39842  dihmeetlem5  39844  dihmeetlem6  39845  dihmeetlem7N  39846  dihmeetlem10N  39852  dihmeetlem11N  39853  dihmeetlem12N  39854  dihmeetlem13N  39855  dihmeetlem15N  39857  dihmeetlem17N  39859  dihmeetlem18N  39860  dihmeetlem19N  39861  dihmeetALTN  39863  dih1dimatlem0  39864  dihlspsnssN  39868  dvh3dim2  39984  sticksstones1  40627  sticksstones2  40628  sticksstones12  40639  dvdsexpnn  40884  resubcan2  40915  mzpsubst  41129  diophrw  41140  eldioph2lem1  41141  rencldnfi  41202  pellexlem2  41211  pellqrexplicit  41258  infmrgelbi  41259  rmxycomplete  41299  congadd  41348  acongeq  41365  jm2.19  41375  jm2.22  41377  jm2.20nn  41379  jm2.25lem1  41380  jm2.27  41390  jm3.1  41402  lmhmlnmsplit  41472  pwssplit4  41474  hbtlem2  41509  dgraa0p  41534  idomrootle  41580  proot1hash  41585  iocunico  41603  cantnf2  41718  dflim5  41722  omcl2  41726  tfsconcatrn  41735  nadd2rabex  41779  relexpxpmin  42111  brtrclfv2  42121  ntrclsk3  42464  grur1cld  42634  ismnu  42663  suprnmpt  43513  wessf1ornlem  43525  choicefi  43542  supxrgere  43688  supxrgelem  43692  supxrge  43693  infleinflem2  43726  snunioo1  43870  iccintsng  43881  fmul01  43941  lptre2pt  44001  0ellimcdiv  44010  fnlimfvre  44035  limsupmnfuzlem  44087  climisp  44107  limsupgtlem  44138  ibliccsinexp  44312  iblioosinexp  44314  volioc  44333  iblspltprt  44334  stoweidlem20  44381  stoweidlem22  44383  stoweidlem34  44395  stoweidlem44  44405  stoweidlem60  44421  wallispilem3  44428  fourierdlem42  44510  fourierdlem51  44518  fourierdlem54  44521  fourierdlem87  44554  fourierdlem97  44564  ioorrnopnlem  44665  sge0seq  44807  hoicvr  44909  fsupdm  45203  finfdm  45207  funfocofob  45430  imasetpreimafvbijlemfv  45714  fprmappr  46541  lincresunit3lem3  46675  lindssnlvec  46687  rrx2linesl  46949  line2  46958  itsclc0lem3  46964  itsclc0yqsollem1  46968  itscnhlc0xyqsol  46971  itschlc0xyqsol1  46972  itsclc0  46977  itscnhlinecirc02plem2  46989  itscnhlinecirc02plem3  46990