Theorem simpl3 1212

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl13  1269  simpl23  1272  simpl33  1275  simp1l3  1287  simp2l3  1293  simp3l3  1299  3anandirs  1502  2nreu  4405  predtrss  6343  frpomin  6361  f1prex  7315  fcofo  7319  soisores  7358  weniso  7387  knatar  7390  ofmpteq  7740  funelss  8083  frrlem10  8341  fprlem1  8346  smocdmdom  8404  nnmord  8669  nnmword  8670  naddasslem1  8732  naddasslem2  8733  difsnen  9106  mapunen  9193  ac6sfi  9303  fipreima  9375  wemaplem2  9568  wemapso2lem  9573  ttrclselem2  9754  en2eqpr  10113  indcardi  10147  acndom  10157  fodomfi2  10166  infmap2  10322  cflim2  10368  coftr  10378  infpssrlem4  10411  fin23lem11  10422  fincssdom  10428  isf32lem9  10466  fin1a2lem9  10513  gchpwdom  10782  gruima  10914  prpssnq  11102  distrlem4pr  11138  dedekind  11500  addcan  11521  addcan2  11522  divmulass  12024  supmul1  12313  uzsupss  13094  xaddass  13406  xleadd1a  13410  xlesubadd  13420  xmulasslem3  13443  xmulass  13444  xadddilem  13451  xadddi  13452  ixxun  13519  icoshftf1o  13632  snunioc  13638  difelfzle  13802  fzo1fzo0n0  13877  ssfzoulel  13922  modmuladd  14083  modifeq2int  14103  modaddmulmod  14108  modsubdir  14110  ltexp2a  14336  leexp2  14341  ltexp2r  14343  exple1  14347  expnlbnd2  14405  mulsubdivbinom2  14433  hashtpg  14657  ccatass  14761  swrdrn3  14830  ccatopth  14893  pfxccatin12lem2a  14904  pfxccat3  14911  cshinj  14990  2cshw  14992  s2f1o  15096  limsupgre  15677  addcn2  15790  mulcn2  15792  binomrisefac  16237  bpolydif  16250  dvdsmodexp  16459  modmulconst  16487  dvdsexp2im  16526  dvdsmod  16528  sadass  16670  gcdass  16749  rplpwr  16761  dvdsexpnn  16769  rpmulgcd2  16860  rpdvds  16864  rpexp  16927  prmdiveq  16992  hashgcdlem  16994  coprimeprodsq  17015  coprimeprodsq2  17016  pythagtriplem3  17025  pcdvdsb  17076  pcgcd1  17084  dvdsprmpweq  17091  pcbc  17107  0ram  17227  ramz2  17231  ramub1lem1  17233  mremre  17803  mrieqv2d  17842  lubun  18718  isnsgrp  18941  issubmnd  18982  frmdss2  19088  submefmnd  19120  sgrp2rid2ex  19155  mulgnn0p1  19324  mulgnnsubcl  19325  mulgneg  19331  mulgdirlem  19344  nmzsubg  19404  ghmmulg  19471  pmtrfv  19696  pmtrmvd  19700  pmtrfb  19709  odmodnn0  19784  oddvdsnn0  19788  odnncl  19789  odmod  19790  oddvds  19791  odeq  19794  odmulgid  19798  odmulg  19800  odmulgeq  19801  odbezout  19802  odf1o1  19816  odf1o2  19817  odngen  19821  odcau  19848  pgpssslw  19858  fislw  19869  lsmless1x  19888  lsmless2x  19889  lsmsubm  19897  lsmmod  19919  lsmmod2  19920  efgsfo  19983  cntzcmn  20084  odadd1  20092  odadd2  20093  odadd  20094  lsmcomx  20100  prdscmnd  20105  gsumconst  20178  ring1eq0  20559  cntzsubrng  20849  cntzsubr  20888  isabvd  21099  rmodislmod  21235  lspss  21289  0lmhm  21345  reslmhm2  21358  pwssplit0  21363  pwssplit1  21364  lbspss  21387  lspfixed  21436  lsmcv  21449  lspsnat  21453  pidlnz  21558  2idlcpblrng  21595  cnfldfunALT  21723  xrsdsreclblem  21749  obselocv  22064  frlmsplit2  22109  frlmsslss2  22111  frlmup4  22137  lindff1  22156  lsslindf  22166  lsslinds  22167  islindf4  22174  lindsenlbs  22187  issubassa  22205  aspss  22214  coe1subfv  22615  coe1tm  22622  mpomatmul  22791  mamutpos  22803  submaval  22926  mdetdiag  22944  mdetunilem1  22957  mdetunilem3  22959  mdetunilem9  22965  mdetmul  22968  maducoeval2  22985  madurid  22989  minmar1val  22993  cramer  23039  cpmatel2  23061  m2cpm  23089  decpmatmul  23120  pmatcollpw1lem2  23123  pmatcollpw1  23124  pmatcollpw2lem  23125  pm2mpcl  23145  mply1topmatcl  23153  mp2pm2mplem2  23155  mp2pm2mplem4  23157  pm2mpghmlem2  23160  pm2mpghmlem1  23161  cayhamlem2  23232  neiint  23452  topssnei  23472  cnrest2  23634  cnprest2  23638  cnt0  23694  cnt1  23698  cnhaus  23702  cncmp  23740  fiuncmp  23752  sscmp  23753  hauscmp  23755  cnconn  23770  unconn  23777  comppfsc  23881  kgen2ss  23904  ptpjopn  23961  ptrescn  23988  qtopss  24064  kqfvima  24079  r0cld  24087  cmphaushmeo  24149  fbssint  24187  fbasrn  24233  filuni  24234  ufilmax  24256  fin1aufil  24281  fmf  24294  fmss  24295  rnelfmlem  24301  rnelfm  24302  fmufil  24308  fmco  24310  flimss2  24321  flimss1  24322  flimrest  24332  cnpflf2  24349  cnpflf  24350  flfcnp  24353  lmflf  24354  supnfcls  24369  fclsss1  24371  fclsss2  24372  cnpfcfi  24389  subgntr  24456  opnsubg  24457  cldsubg  24460  ustuqtop1  24590  ucncn  24633  bldisj  24747  blgt0  24748  bl2in  24749  blss2ps  24752  blss2  24753  xbln0  24763  blssps  24773  blss  24774  lpbl  24852  blcld  24854  blcls  24855  stdbdmopn  24867  metcnp2  24891  txmetcnp  24896  blval2  24911  restmetu  24919  nmoix  25078  nmoi2  25079  nmoeq0  25085  nmotri  25088  metdsge  25199  metds0  25200  metdseq0  25204  icoopnst  25290  iccpnfhmeo  25296  xrhmeo  25297  nmhmcn  25471  cphsqrtcl2  25537  cphsqrtcl3  25538  fmcfil  25623  bcthlem5  25679  cmetcusp1  25704  cssbn  25726  pjth  25790  ovolunnul  25851  volun  25896  voliunlem2  25902  itg2const  26091  iblconst  26168  itgconst  26169  limcvallem  26221  dvcnp2  26270  dvcn  26271  deg1mul3le  26465  deg1tmle  26466  idomrootle  26521  ig1pdvds  26528  coe11  26602  dgrmulc  26620  dvply1  26635  aaliou2  26697  efcvx  26806  tanord  26896  logdivlti  26978  logccv  27021  recxpcl  27033  cxplea  27054  cxple2a  27057  ang180  27172  isosctrlem2  27177  cxp2lim  27334  amgm  27348  muval1  27490  dvdssqf  27495  mumullem2  27537  bcmono  27634  lgsneg  27678  lgsmod  27680  lgsdirprm  27688  lgsdir  27689  lgsdi  27691  ltsres  28049  nolt02olem  28081  nolt02o  28082  nogt01o  28083  nosupbnd1lem1  28095  nosupbnd1lem4  28098  nosupbnd1lem5  28099  nosupbnd1lem6  28100  noinfbnd1lem1  28110  noinfbnd1lem4  28113  noinfbnd1lem6  28115  noinfbnd2  28118  noetainflem3  28126  ltslpss  28324  cofslts  28334  coinitslts  28335  cofcutrtime  28343  addsass  28421  addsdi  28571  mulsass  28582  ltmuls2  28587  norecdiv  28606  z12bdaylem  28900  brbtwn2  29513  colinearalglem1  29514  colinearalg  29518  axcgrtr  29523  axcontlem2  29573  upgrewlkle2  30217  wlksoneq1eq2  30273  crctcshwlkn0lem5  30433  wspthsnwspthsnon  30535  lppthon  30772  upgriseupth  30838  4cyclusnfrgr  30923  numclwwlk1lem2foa  30985  numclwwlk5  31019  nvmul0or  31282  shless  31991  shlej1  31992  pjspansn  32209  kbmul  32587  homco2  32609  kbass2  32749  fnpreimac  33336  padct  33381  eliccelico  33439  elicoelioo  33440  iocinioc2  33441  difioo  33444  nexple  33494  swrdrn2  33587  xrge0npcan  33651  isarchi2  33816  archiabl  33829  lindssn  34003  ssmxidl  34069  mdetlap1  34528  zarclsiin  34573  pstmfval  34598  fmcncfil  34633  zrhnm  34669  qqhnm  34692  volfiniune  34933  omsmeas  35025  eulerpartlemb  35070  probinc  35123  cndprob01  35137  signswmnd  35256  cvmsss2  36206  funsseq  36711  cgrtriv  36945  5segofs  36949  btwntriv2  36955  btwnxfr  36999  segcon2  37048  brsegle2  37052  seglelin  37059  outsideofeu  37074  nmulss1  37141  ltnmul  37143  nmulle  37144  ltnadd  37145  naddle  37146  nadddi  37151  weiunpo  37431  weiunfr  37433  weiunse  37434  mblfinlem2  38768  blbnd  38913  rrndstprj2  38957  zerdivemp1x  39073  lsmsat  40257  lsatfixedN  40258  lssat  40265  lkrlsp  40351  lshpkrlem4  40362  cvrcon3b  40526  leat3  40544  atlen0  40559  atnle  40566  atlatmstc  40568  atlatle  40569  cvlcvr1  40588  cvlsupr2  40592  hlsupr2  40636  hlrelat2  40652  cvrexchlem  40668  cvratlem  40670  lnnat  40676  atexchcvrN  40689  1cvratlt  40723  1cvrjat  40724  3atlem3  40734  3atlem7  40738  llni2  40761  atcvrlln2  40768  llnexatN  40770  llncmp  40771  2llnmat  40773  2at0mat0  40774  2atnelpln  40793  llncvrlpln2  40806  2lplnmN  40808  2llnmj  40809  lplncmp  40811  lplnexatN  40812  2llnjaN  40815  lvoli3  40826  islvol2aN  40841  4atlem3a  40846  4atlem4a  40848  4atlem4b  40849  4atlem11  40858  4atlem12  40861  lplncvrlvol2  40864  lvolcmp  40866  2lplnmj  40871  islinei  40989  linepmap  41024  lneq2at  41027  2llnma3r  41037  elpaddn0  41049  elpaddatriN  41052  elpaddat  41053  paddcom  41062  paddss1  41066  paddss2  41067  paddasslem6  41074  paddasslem7  41075  paddasslem10  41078  paddasslem15  41083  pmodlem2  41096  pmodl42N  41100  pmapjoin  41101  atmod1i1m  41107  llnmod1i2  41109  llnexchb2lem  41117  polcon2bN  41169  pclfinclN  41199  poml4N  41202  poml6N  41204  osumcllem11N  41215  osumclN  41216  pmapojoinN  41217  pexmidlem2N  41220  pexmidlem3N  41221  pexmidlem4N  41222  pexmidlem6N  41224  pexmidlem7N  41225  pl42lem2N  41229  pl42lem3N  41230  pl42lem4N  41231  pl42N  41232  lhpexle3lem  41260  lhpmcvr3  41274  lhp2at0nle  41284  lhprelat3N  41289  lauteq  41344  lautco  41346  ltrncoidN  41377  ltrneq2  41397  ltrnnidn  41423  ltrnideq  41424  trlnle  41435  cdlemc  41446  cdlemd4  41450  cdlemd5  41451  cdlemd9  41455  cdlemd  41456  ltrneq3  41457  cdlemefrs29pre00  41644  cdlemefrs29cpre1  41647  cdlemefrs29clN  41648  cdlemefrs32fva  41649  cdlemefr29exN  41651  cdlemefr27cl  41652  cdlemefs27cl  41662  cdlemefs32sn1aw  41663  cdleme32fva  41686  cdleme32d  41693  cdleme32f  41695  cdleme32le  41696  cdleme40n  41717  cdleme41snaw  41725  cdleme17d3  41745  cdleme48fvg  41749  cdlemeg46fvcl  41755  cdlemeg46fgN  41783  cdleme48fgv  41787  ltrniotavalbN  41833  cdlemb3  41855  cdlemg15  41905  cdlemg17dN  41912  trlco  41976  cdlemg44b  41981  ltrncom  41987  trljco  41989  tendococl  42021  tendoplcl  42030  tendoplcom  42031  tendotr  42079  cdlemk36  42162  cdlemk35s-id  42187  cdlemk39s-id  42189  cdlemk19x  42192  cdlemk53b  42205  cdlemk55  42210  cdlemk35u  42213  cdlemk55u  42215  cdlemk39u  42217  cdlemk19u  42219  cdlemk56  42220  tendoex  42224  cdleml5N  42229  dihord2pre  42474  dihord6apre  42505  dihord5b  42508  dihord5apre  42511  dihord  42513  dihmeetlem1N  42539  dihmeetlem2N  42548  dihglbcpreN  42549  dihmeetbN  42552  dihmeetlem4preN  42555  dihmeetlem5  42557  dihmeetlem6  42558  dihmeetlem7N  42559  dihmeetlem10N  42565  dihmeetlem11N  42566  dihmeetlem12N  42567  dihmeetlem13N  42568  dihmeetlem15N  42570  dihmeetlem17N  42572  dihmeetlem18N  42573  dihmeetlem19N  42574  dihmeetALTN  42576  dih1dimatlem0  42577  dihlspsnssN  42581  dvh3dim2  42697  sticksstones1  43388  sticksstones2  43389  sticksstones12  43400  aks6d1c6isolem1  43416  resubcan2  43632  mzpsubst  43952  diophrw  43963  eldioph2lem1  43964  rencldnfi  44021  pellexlem2  44030  pellqrexplicit  44077  infmrgelbi  44078  rmxycomplete  44117  congadd  44166  acongeq  44183  jm2.19  44193  jm2.22  44195  jm2.20nn  44197  jm2.25lem1  44198  jm2.27  44208  jm3.1  44220  lmhmlnmsplit  44282  pwssplit4  44284  hbtlem2  44318  dgraa0p  44343  proot1hash  44389  iocunico  44405  cantnf2  44519  dflim5  44523  omcl2  44527  tfsconcatrn  44536  nadd2rabex  44580  relexpxpmin  44909  brtrclfv2  44919  ntrclsk3  45262  grur1cld  45422  ismnu  45437  suprnmpt  46394  wessf1ornlem  46405  choicefi  46419  supxrgere  46550  supxrgelem  46554  supxrge  46555  infleinflem2  46587  snunioo1  46729  iccintsng  46740  fmul01  46797  lptre2pt  46855  0ellimcdiv  46864  fnlimfvre  46889  limsupmnfuzlem  46941  climisp  46961  limsupgtlem  46992  ibliccsinexp  47166  iblioosinexp  47168  volioc  47187  iblspltprt  47188  stoweidlem20  47235  stoweidlem22  47237  stoweidlem34  47249  stoweidlem44  47259  stoweidlem60  47275  wallispilem3  47282  fourierdlem42  47364  fourierdlem51  47372  fourierdlem54  47375  fourierdlem87  47408  fourierdlem97  47418  ioorrnopnlem  47519  sge0seq  47661  hoicvr  47763  fsupdm  48057  finfdm  48061  3f1oss1  48350  funfocofob  48353  imasetpreimafvbijlemfv  48689  uhgrimisgrgric  49234  uhgrimgrlim  49290  fprmappr  49662  lincresunit3lem3  49791  lindssnlvec  49803  rrx2linesl  50060  itsclc0lem3  50075  itsclc0yqsollem1  50079  itscnhlc0xyqsol  50082  itschlc0xyqsol1  50083  itsclc0  50088  itscnhlinecirc02plem2  50100  itscnhlinecirc02plem3  50101  uptrlem1  50531  uptr2  50542  setc1onsubc  50945