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  4396  predtrss  6280  frpomin  6298  f1prex  7230  fcofo  7234  soisores  7273  weniso  7300  knatar  7303  ofmpteq  7645  funelss  7991  frrlem10  8237  fprlem1  8242  smocdmdom  8300  nnmord  8560  nnmword  8561  naddasslem1  8622  naddasslem2  8623  difsnen  8987  mapunen  9074  ac6sfi  9184  fipreima  9258  wemaplem2  9452  wemapso2lem  9457  ttrclselem2  9635  en2eqpr  9917  indcardi  9951  acndom  9961  fodomfi2  9970  infmap2  10127  cflim2  10173  coftr  10183  infpssrlem4  10216  fin23lem11  10227  fincssdom  10233  isf32lem9  10271  fin1a2lem9  10318  gchpwdom  10581  gruima  10713  prpssnq  10901  distrlem4pr  10937  dedekind  11296  addcan  11317  addcan2  11318  divmulass  11819  supmul1  12111  uzsupss  12853  xaddass  13164  xleadd1a  13168  xlesubadd  13178  xmulasslem3  13201  xmulass  13202  xadddilem  13209  xadddi  13210  ixxun  13277  icoshftf1o  13390  snunioc  13396  difelfzle  13557  fzo1fzo0n0  13631  ssfzoulel  13676  modmuladd  13836  modifeq2int  13856  modaddmulmod  13861  modsubdir  13863  ltexp2a  14089  leexp2  14094  ltexp2r  14096  exple1  14100  expnlbnd2  14157  mulsubdivbinom2  14185  hashtpg  14408  ccatass  14512  ccatopth  14639  pfxccatin12lem2a  14650  pfxccat3  14657  cshinj  14734  2cshw  14736  s2f1o  14839  limsupgre  15404  addcn2  15517  mulcn2  15519  binomrisefac  15965  bpolydif  15978  dvdsmodexp  16187  modmulconst  16215  dvdsexp2im  16254  dvdsmod  16256  sadass  16398  gcdass  16474  rplpwr  16485  rpmulgcd2  16583  rpdvds  16587  rpexp  16649  prmdiveq  16713  hashgcdlem  16715  coprimeprodsq  16736  coprimeprodsq2  16737  pythagtriplem3  16746  pcdvdsb  16797  pcgcd1  16805  dvdsprmpweq  16812  pcbc  16828  0ram  16948  ramz2  16952  ramub1lem1  16954  mremre  17523  mrieqv2d  17562  lubun  18438  isnsgrp  18648  issubmnd  18686  frmdss2  18788  submefmnd  18820  sgrp2rid2ex  18852  mulgnn0p1  19015  mulgnnsubcl  19016  mulgneg  19022  mulgdirlem  19035  nmzsubg  19094  ghmmulg  19157  pmtrfv  19381  pmtrmvd  19385  pmtrfb  19394  odmodnn0  19469  oddvdsnn0  19473  odnncl  19474  odmod  19475  oddvds  19476  odeq  19479  odmulgid  19483  odmulg  19485  odmulgeq  19486  odbezout  19487  odf1o1  19501  odf1o2  19502  odngen  19506  odcau  19533  pgpssslw  19543  fislw  19554  lsmless1x  19573  lsmless2x  19574  lsmsubm  19582  lsmmod  19604  lsmmod2  19605  efgsfo  19668  cntzcmn  19769  odadd1  19777  odadd2  19778  odadd  19779  lsmcomx  19785  prdscmnd  19790  gsumconst  19863  ring1eq0  20233  cntzsubrng  20500  cntzsubr  20539  isabvd  20745  rmodislmod  20881  lspss  20935  0lmhm  20992  reslmhm2  21005  pwssplit0  21010  pwssplit1  21011  lbspss  21034  lspfixed  21083  lsmcv  21096  lspsnat  21100  2idlcpblrng  21226  cnfldfunALT  21324  cnfldfunALTOLD  21337  xrsdsreclblem  21367  obselocv  21683  frlmsplit2  21728  frlmsslss2  21730  frlmup4  21756  lindff1  21775  lsslindf  21785  lsslinds  21786  islindf4  21793  issubassa  21822  aspss  21832  coe1subfv  22208  coe1tm  22215  mpomatmul  22390  mamutpos  22402  submaval  22525  mdetdiag  22543  mdetunilem1  22556  mdetunilem3  22558  mdetunilem9  22564  mdetmul  22567  maducoeval2  22584  madurid  22588  minmar1val  22592  cramer  22635  cpmatel2  22657  m2cpm  22685  decpmatmul  22716  pmatcollpw1lem2  22719  pmatcollpw1  22720  pmatcollpw2lem  22721  pm2mpcl  22741  mply1topmatcl  22749  mp2pm2mplem2  22751  mp2pm2mplem4  22753  pm2mpghmlem2  22756  pm2mpghmlem1  22757  cayhamlem2  22828  neiint  23048  topssnei  23068  cnrest2  23230  cnprest2  23234  cnt0  23290  cnt1  23294  cnhaus  23298  cncmp  23336  fiuncmp  23348  sscmp  23349  hauscmp  23351  cnconn  23366  unconn  23373  comppfsc  23476  kgen2ss  23499  ptpjopn  23556  ptrescn  23583  qtopss  23659  kqfvima  23674  r0cld  23682  cmphaushmeo  23744  fbssint  23782  fbasrn  23828  filuni  23829  ufilmax  23851  fin1aufil  23876  fmf  23889  fmss  23890  rnelfmlem  23896  rnelfm  23897  fmufil  23903  fmco  23905  flimss2  23916  flimss1  23917  flimrest  23927  cnpflf2  23944  cnpflf  23945  flfcnp  23948  lmflf  23949  supnfcls  23964  fclsss1  23966  fclsss2  23967  cnpfcfi  23984  subgntr  24051  opnsubg  24052  cldsubg  24055  ustuqtop1  24185  ucncn  24228  bldisj  24342  blgt0  24343  bl2in  24344  blss2ps  24347  blss2  24348  xbln0  24358  blssps  24368  blss  24369  lpbl  24447  blcld  24449  blcls  24450  stdbdmopn  24462  metcnp2  24486  txmetcnp  24491  blval2  24506  restmetu  24514  nmoix  24673  nmoi2  24674  nmoeq0  24680  nmotri  24683  metdsge  24794  metds0  24795  metdseq0  24799  icoopnst  24892  iccpnfhmeo  24899  xrhmeo  24900  nmhmcn  25076  cphsqrtcl2  25142  cphsqrtcl3  25143  fmcfil  25228  bcthlem5  25284  cmetcusp1  25309  cssbn  25331  pjth  25395  ovolunnul  25457  volun  25502  voliunlem2  25508  itg2const  25697  iblconst  25775  itgconst  25776  limcvallem  25828  dvcnp2  25877  dvcnp2OLD  25878  dvcn  25879  deg1mul3le  26078  deg1tmle  26079  idomrootle  26134  ig1pdvds  26141  coe11  26214  dgrmulc  26233  dvply1  26247  aaliou2  26304  efcvx  26415  tanord  26503  logdivlti  26585  logccv  26628  recxpcl  26640  cxplea  26661  cxple2a  26664  ang180  26780  isosctrlem2  26785  cxp2lim  26943  amgm  26957  muval1  27099  dvdssqf  27104  mumullem2  27146  bcmono  27244  lgsneg  27288  lgsmod  27290  lgsdirprm  27298  lgsdir  27299  lgsdi  27301  ltsres  27630  nolt02olem  27662  nolt02o  27663  nogt01o  27664  nosupbnd1lem1  27676  nosupbnd1lem4  27679  nosupbnd1lem5  27680  nosupbnd1lem6  27681  noinfbnd1lem1  27691  noinfbnd1lem4  27694  noinfbnd1lem6  27696  noinfbnd2  27699  noetainflem3  27707  ltslpss  27904  cofslts  27914  coinitslts  27915  cofcutrtime  27923  addsass  28001  addsdi  28151  mulsass  28162  ltmuls2  28167  norecdiv  28186  z12bdaylem  28480  brbtwn2  28978  colinearalglem1  28979  colinearalg  28983  axcgrtr  28988  axcontlem2  29038  upgrewlkle2  29680  wlksoneq1eq2  29736  crctcshwlkn0lem5  29887  wspthsnwspthsnon  29989  lppthon  30226  upgriseupth  30282  4cyclusnfrgr  30367  numclwwlk1lem2foa  30429  numclwwlk5  30463  nvmul0or  30725  shless  31434  shlej1  31435  pjspansn  31652  kbmul  32030  homco2  32052  kbass2  32192  fnpreimac  32749  padct  32797  eliccelico  32857  elicoelioo  32858  iocinioc2  32859  difioo  32862  nexple  32925  swrdrn2  33036  swrdrn3  33037  xrge0npcan  33102  isarchi2  33267  archiabl  33280  pidlnz  33457  lindssn  33459  ssmxidl  33555  mdetlap1  33983  zarclsiin  34028  pstmfval  34053  fmcncfil  34088  zrhnm  34124  qqhnm  34147  volfiniune  34387  omsmeas  34480  eulerpartlemb  34525  probinc  34578  cndprob01  34592  signswmnd  34714  cvmsss2  35468  funsseq  35962  cgrtriv  36196  5segofs  36200  btwntriv2  36206  btwnxfr  36250  segcon2  36299  brsegle2  36303  seglelin  36310  outsideofeu  36325  weiunpo  36659  weiunfr  36661  weiunse  36662  lindsenlbs  37812  mblfinlem2  37855  blbnd  37984  rrndstprj2  38028  zerdivemp1x  38144  lsmsat  39264  lsatfixedN  39265  lssat  39272  lkrlsp  39358  lshpkrlem4  39369  cvrcon3b  39533  leat3  39551  atlen0  39566  atnle  39573  atlatmstc  39575  atlatle  39576  cvlcvr1  39595  cvlsupr2  39599  hlsupr2  39643  hlrelat2  39659  cvrexchlem  39675  cvratlem  39677  lnnat  39683  atexchcvrN  39696  1cvratlt  39730  1cvrjat  39731  3atlem3  39741  3atlem7  39745  llni2  39768  atcvrlln2  39775  llnexatN  39777  llncmp  39778  2llnmat  39780  2at0mat0  39781  2atnelpln  39800  llncvrlpln2  39813  2lplnmN  39815  2llnmj  39816  lplncmp  39818  lplnexatN  39819  2llnjaN  39822  lvoli3  39833  islvol2aN  39848  4atlem3a  39853  4atlem4a  39855  4atlem4b  39856  4atlem11  39865  4atlem12  39868  lplncvrlvol2  39871  lvolcmp  39873  2lplnmj  39878  islinei  39996  linepmap  40031  lneq2at  40034  2llnma3r  40044  elpaddn0  40056  elpaddatriN  40059  elpaddat  40060  paddcom  40069  paddss1  40073  paddss2  40074  paddasslem6  40081  paddasslem7  40082  paddasslem10  40085  paddasslem15  40090  pmodlem2  40103  pmodl42N  40107  pmapjoin  40108  atmod1i1m  40114  llnmod1i2  40116  llnexchb2lem  40124  polcon2bN  40176  pclfinclN  40206  poml4N  40209  poml6N  40211  osumcllem11N  40222  osumclN  40223  pmapojoinN  40224  pexmidlem2N  40227  pexmidlem3N  40228  pexmidlem4N  40229  pexmidlem6N  40231  pexmidlem7N  40232  pl42lem2N  40236  pl42lem3N  40237  pl42lem4N  40238  pl42N  40239  lhpexle3lem  40267  lhpmcvr3  40281  lhp2at0nle  40291  lhprelat3N  40296  lauteq  40351  lautco  40353  ltrncoidN  40384  ltrneq2  40404  ltrnnidn  40430  ltrnideq  40431  trlnle  40442  cdlemc  40453  cdlemd4  40457  cdlemd5  40458  cdlemd9  40462  cdlemd  40463  ltrneq3  40464  cdlemefrs29pre00  40651  cdlemefrs29cpre1  40654  cdlemefrs29clN  40655  cdlemefrs32fva  40656  cdlemefr29exN  40658  cdlemefr27cl  40659  cdlemefs27cl  40669  cdlemefs32sn1aw  40670  cdleme32fva  40693  cdleme32d  40700  cdleme32f  40702  cdleme32le  40703  cdleme40n  40724  cdleme41snaw  40732  cdleme17d3  40752  cdleme48fvg  40756  cdlemeg46fvcl  40762  cdlemeg46fgN  40790  cdleme48fgv  40794  ltrniotavalbN  40840  cdlemb3  40862  cdlemg15  40912  cdlemg17dN  40919  trlco  40983  cdlemg44b  40988  ltrncom  40994  trljco  40996  tendococl  41028  tendoplcl  41037  tendoplcom  41038  tendotr  41086  cdlemk36  41169  cdlemk35s-id  41194  cdlemk39s-id  41196  cdlemk19x  41199  cdlemk53b  41212  cdlemk55  41217  cdlemk35u  41220  cdlemk55u  41222  cdlemk39u  41224  cdlemk19u  41226  cdlemk56  41227  tendoex  41231  cdleml5N  41236  dihord2pre  41481  dihord6apre  41512  dihord5b  41515  dihord5apre  41518  dihord  41520  dihmeetlem1N  41546  dihmeetlem2N  41555  dihglbcpreN  41556  dihmeetbN  41559  dihmeetlem4preN  41562  dihmeetlem5  41564  dihmeetlem6  41565  dihmeetlem7N  41566  dihmeetlem10N  41572  dihmeetlem11N  41573  dihmeetlem12N  41574  dihmeetlem13N  41575  dihmeetlem15N  41577  dihmeetlem17N  41579  dihmeetlem18N  41580  dihmeetlem19N  41581  dihmeetALTN  41583  dih1dimatlem0  41584  dihlspsnssN  41588  dvh3dim2  41704  sticksstones1  42396  sticksstones2  42397  sticksstones12  42408  aks6d1c6isolem1  42424  dvdsexpnn  42584  resubcan2  42639  mzpsubst  42986  diophrw  42997  eldioph2lem1  42998  rencldnfi  43059  pellexlem2  43068  pellqrexplicit  43115  infmrgelbi  43116  rmxycomplete  43155  congadd  43204  acongeq  43221  jm2.19  43231  jm2.22  43233  jm2.20nn  43235  jm2.25lem1  43236  jm2.27  43246  jm3.1  43258  lmhmlnmsplit  43325  pwssplit4  43327  hbtlem2  43362  dgraa0p  43387  proot1hash  43433  iocunico  43449  cantnf2  43563  dflim5  43567  omcl2  43571  tfsconcatrn  43580  nadd2rabex  43624  relexpxpmin  43954  brtrclfv2  43964  ntrclsk3  44307  grur1cld  44469  ismnu  44498  suprnmpt  45414  wessf1ornlem  45425  choicefi  45440  supxrgere  45574  supxrgelem  45578  supxrge  45579  infleinflem2  45611  snunioo1  45754  iccintsng  45765  fmul01  45822  lptre2pt  45880  0ellimcdiv  45889  fnlimfvre  45914  limsupmnfuzlem  45966  climisp  45986  limsupgtlem  46017  ibliccsinexp  46191  iblioosinexp  46193  volioc  46212  iblspltprt  46213  stoweidlem20  46260  stoweidlem22  46262  stoweidlem34  46274  stoweidlem44  46284  stoweidlem60  46300  wallispilem3  46307  fourierdlem42  46389  fourierdlem51  46397  fourierdlem54  46400  fourierdlem87  46433  fourierdlem97  46443  ioorrnopnlem  46544  sge0seq  46686  hoicvr  46788  fsupdm  47082  finfdm  47086  3f1oss1  47317  funfocofob  47320  imasetpreimafvbijlemfv  47644  uhgrimisgrgric  48173  uhgrimgrlim  48229  fprmappr  48587  lincresunit3lem3  48716  lindssnlvec  48728  rrx2linesl  48985  line2  48994  itsclc0lem3  49000  itsclc0yqsollem1  49004  itscnhlc0xyqsol  49007  itschlc0xyqsol1  49008  itsclc0  49013  itscnhlinecirc02plem2  49025  itscnhlinecirc02plem3  49026  uptrlem1  49451  uptr2  49462  setc1onsubc  49843