Theorem simpl3 1210

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simpl13  1267  simpl23  1270  simpl33  1273  simp1l3  1285  simp2l3  1291  simp3l3  1297  3anandirs  1496  2nreu  4401  predtrss  6313  frpomin  6331  f1prex  7272  fcofo  7276  soisores  7315  weniso  7342  knatar  7345  ofmpteq  7687  funelss  8032  frrlem10  8280  fprlem1  8285  smocdmdom  8343  nnmord  8606  nnmword  8607  naddasslem1  8669  naddasslem2  8670  difsnen  9035  mapunen  9122  ac6sfi  9232  fipreima  9303  wemaplem2  9497  wemapso2lem  9502  ttrclselem2  9683  en2eqpr  9979  indcardi  10013  acndom  10023  fodomfi2  10032  infmap2  10188  cflim2  10235  coftr  10245  infpssrlem4  10278  fin23lem11  10289  fincssdom  10295  isf32lem9  10333  fin1a2lem9  10380  gchpwdom  10643  gruima  10775  prpssnq  10963  distrlem4pr  10999  dedekind  11361  addcan  11382  addcan2  11383  divmulass  11883  supmul1  12175  uzsupss  12955  xaddass  13266  xleadd1a  13270  xlesubadd  13280  xmulasslem3  13303  xmulass  13304  xadddilem  13311  xadddi  13312  ixxun  13379  icoshftf1o  13492  snunioc  13498  difelfzle  13660  fzo1fzo0n0  13735  ssfzoulel  13780  modmuladd  13940  modifeq2int  13960  modaddmulmod  13965  modsubdir  13967  ltexp2a  14193  leexp2  14198  ltexp2r  14200  exple1  14204  expnlbnd2  14261  mulsubdivbinom2  14289  hashtpg  14512  ccatass  14616  ccatopth  14743  pfxccatin12lem2a  14754  pfxccat3  14761  cshinj  14838  2cshw  14840  s2f1o  14943  limsupgre  15522  addcn2  15635  mulcn2  15637  binomrisefac  16086  bpolydif  16099  dvdsmodexp  16308  modmulconst  16336  dvdsexp2im  16375  dvdsmod  16377  sadass  16519  gcdass  16595  rplpwr  16606  rpmulgcd2  16704  rpdvds  16708  rpexp  16771  prmdiveq  16835  hashgcdlem  16837  coprimeprodsq  16858  coprimeprodsq2  16859  pythagtriplem3  16868  pcdvdsb  16919  pcgcd1  16927  dvdsprmpweq  16934  pcbc  16950  0ram  17070  ramz2  17074  ramub1lem1  17076  mremre  17646  mrieqv2d  17685  lubun  18561  isnsgrp  18771  issubmnd  18809  frmdss2  18912  submefmnd  18944  sgrp2rid2ex  18979  mulgnn0p1  19142  mulgnnsubcl  19143  mulgneg  19149  mulgdirlem  19162  nmzsubg  19222  ghmmulg  19289  pmtrfv  19513  pmtrmvd  19517  pmtrfb  19526  odmodnn0  19601  oddvdsnn0  19605  odnncl  19606  odmod  19607  oddvds  19608  odeq  19611  odmulgid  19615  odmulg  19617  odmulgeq  19618  odbezout  19619  odf1o1  19633  odf1o2  19634  odngen  19638  odcau  19665  pgpssslw  19675  fislw  19686  lsmless1x  19705  lsmless2x  19706  lsmsubm  19714  lsmmod  19736  lsmmod2  19737  efgsfo  19800  cntzcmn  19901  odadd1  19909  odadd2  19910  odadd  19911  lsmcomx  19917  prdscmnd  19922  gsumconst  19995  ring1eq0  20372  cntzsubrng  20643  cntzsubr  20682  isabvd  20884  rmodislmod  21020  lspss  21074  0lmhm  21130  reslmhm2  21143  pwssplit0  21148  pwssplit1  21149  lbspss  21172  lspfixed  21221  lsmcv  21234  lspsnat  21238  2idlcpblrng  21372  cnfldfunALT  21497  xrsdsreclblem  21523  obselocv  21838  frlmsplit2  21883  frlmsslss2  21885  frlmup4  21911  lindff1  21930  lsslindf  21940  lsslinds  21941  islindf4  21948  issubassa  21977  aspss  21986  coe1subfv  22387  coe1tm  22394  mpomatmul  22564  mamutpos  22576  submaval  22699  mdetdiag  22717  mdetunilem1  22730  mdetunilem3  22732  mdetunilem9  22738  mdetmul  22741  maducoeval2  22758  madurid  22762  minmar1val  22766  cramer  22809  cpmatel2  22831  m2cpm  22859  decpmatmul  22890  pmatcollpw1lem2  22893  pmatcollpw1  22894  pmatcollpw2lem  22895  pm2mpcl  22915  mply1topmatcl  22923  mp2pm2mplem2  22925  mp2pm2mplem4  22927  pm2mpghmlem2  22930  pm2mpghmlem1  22931  cayhamlem2  23002  neiint  23222  topssnei  23242  cnrest2  23404  cnprest2  23408  cnt0  23464  cnt1  23468  cnhaus  23472  cncmp  23510  fiuncmp  23522  sscmp  23523  hauscmp  23525  cnconn  23540  unconn  23547  comppfsc  23650  kgen2ss  23673  ptpjopn  23730  ptrescn  23757  qtopss  23833  kqfvima  23848  r0cld  23856  cmphaushmeo  23918  fbssint  23956  fbasrn  24002  filuni  24003  ufilmax  24025  fin1aufil  24050  fmf  24063  fmss  24064  rnelfmlem  24070  rnelfm  24071  fmufil  24077  fmco  24079  flimss2  24090  flimss1  24091  flimrest  24101  cnpflf2  24118  cnpflf  24119  flfcnp  24122  lmflf  24123  supnfcls  24138  fclsss1  24140  fclsss2  24141  cnpfcfi  24158  subgntr  24225  opnsubg  24226  cldsubg  24229  ustuqtop1  24359  ucncn  24402  bldisj  24516  blgt0  24517  bl2in  24518  blss2ps  24521  blss2  24522  xbln0  24532  blssps  24542  blss  24543  lpbl  24621  blcld  24623  blcls  24624  stdbdmopn  24636  metcnp2  24660  txmetcnp  24665  blval2  24680  restmetu  24688  nmoix  24847  nmoi2  24848  nmoeq0  24854  nmotri  24857  metdsge  24968  metds0  24969  metdseq0  24973  icoopnst  25059  iccpnfhmeo  25065  xrhmeo  25066  nmhmcn  25240  cphsqrtcl2  25306  cphsqrtcl3  25307  fmcfil  25392  bcthlem5  25448  cmetcusp1  25473  cssbn  25495  pjth  25559  ovolunnul  25620  volun  25665  voliunlem2  25671  itg2const  25860  iblconst  25938  itgconst  25939  limcvallem  25991  dvcnp2  26040  dvcn  26041  deg1mul3le  26235  deg1tmle  26236  idomrootle  26291  ig1pdvds  26298  coe11  26371  dgrmulc  26389  dvply1  26406  aaliou2  26462  efcvx  26570  tanord  26661  logdivlti  26743  logccv  26786  recxpcl  26798  cxplea  26819  cxple2a  26822  ang180  26937  isosctrlem2  26942  cxp2lim  27099  amgm  27113  muval1  27255  dvdssqf  27260  mumullem2  27302  bcmono  27399  lgsneg  27443  lgsmod  27445  lgsdirprm  27453  lgsdir  27454  lgsdi  27456  ltsres  27784  nolt02olem  27816  nolt02o  27817  nogt01o  27818  nosupbnd1lem1  27830  nosupbnd1lem4  27833  nosupbnd1lem5  27834  nosupbnd1lem6  27835  noinfbnd1lem1  27845  noinfbnd1lem4  27848  noinfbnd1lem6  27850  noinfbnd2  27853  noetainflem3  27861  ltslpss  28059  cofslts  28069  coinitslts  28070  cofcutrtime  28078  addsass  28156  addsdi  28306  mulsass  28317  ltmuls2  28322  norecdiv  28341  z12bdaylem  28635  brbtwn2  29164  colinearalglem1  29165  colinearalg  29169  axcgrtr  29174  axcontlem2  29224  upgrewlkle2  29865  wlksoneq1eq2  29921  crctcshwlkn0lem5  30072  wspthsnwspthsnon  30174  lppthon  30411  upgriseupth  30467  4cyclusnfrgr  30552  numclwwlk1lem2foa  30614  numclwwlk5  30648  nvmul0or  30911  shless  31620  shlej1  31621  pjspansn  31838  kbmul  32216  homco2  32238  kbass2  32378  fnpreimac  32927  padct  32975  eliccelico  33034  elicoelioo  33035  iocinioc2  33036  difioo  33039  nexple  33090  swrdrn2  33187  swrdrn3  33188  xrge0npcan  33253  isarchi2  33418  archiabl  33431  pidlnz  33605  lindssn  33607  ssmxidl  33674  mdetlap1  34133  zarclsiin  34178  pstmfval  34203  fmcncfil  34238  zrhnm  34274  qqhnm  34297  volfiniune  34537  omsmeas  34630  eulerpartlemb  34675  probinc  34728  cndprob01  34742  signswmnd  34861  cvmsss2  35637  funsseq  36131  cgrtriv  36365  5segofs  36369  btwntriv2  36375  btwnxfr  36419  segcon2  36468  brsegle2  36472  seglelin  36479  outsideofeu  36494  weiunpo  36838  weiunfr  36840  weiunse  36841  lindsenlbs  38126  mblfinlem2  38169  blbnd  38298  rrndstprj2  38342  zerdivemp1x  38458  lsmsat  39644  lsatfixedN  39645  lssat  39652  lkrlsp  39738  lshpkrlem4  39749  cvrcon3b  39913  leat3  39931  atlen0  39946  atnle  39953  atlatmstc  39955  atlatle  39956  cvlcvr1  39975  cvlsupr2  39979  hlsupr2  40023  hlrelat2  40039  cvrexchlem  40055  cvratlem  40057  lnnat  40063  atexchcvrN  40076  1cvratlt  40110  1cvrjat  40111  3atlem3  40121  3atlem7  40125  llni2  40148  atcvrlln2  40155  llnexatN  40157  llncmp  40158  2llnmat  40160  2at0mat0  40161  2atnelpln  40180  llncvrlpln2  40193  2lplnmN  40195  2llnmj  40196  lplncmp  40198  lplnexatN  40199  2llnjaN  40202  lvoli3  40213  islvol2aN  40228  4atlem3a  40233  4atlem4a  40235  4atlem4b  40236  4atlem11  40245  4atlem12  40248  lplncvrlvol2  40251  lvolcmp  40253  2lplnmj  40258  islinei  40376  linepmap  40411  lneq2at  40414  2llnma3r  40424  elpaddn0  40436  elpaddatriN  40439  elpaddat  40440  paddcom  40449  paddss1  40453  paddss2  40454  paddasslem6  40461  paddasslem7  40462  paddasslem10  40465  paddasslem15  40470  pmodlem2  40483  pmodl42N  40487  pmapjoin  40488  atmod1i1m  40494  llnmod1i2  40496  llnexchb2lem  40504  polcon2bN  40556  pclfinclN  40586  poml4N  40589  poml6N  40591  osumcllem11N  40602  osumclN  40603  pmapojoinN  40604  pexmidlem2N  40607  pexmidlem3N  40608  pexmidlem4N  40609  pexmidlem6N  40611  pexmidlem7N  40612  pl42lem2N  40616  pl42lem3N  40617  pl42lem4N  40618  pl42N  40619  lhpexle3lem  40647  lhpmcvr3  40661  lhp2at0nle  40671  lhprelat3N  40676  lauteq  40731  lautco  40733  ltrncoidN  40764  ltrneq2  40784  ltrnnidn  40810  ltrnideq  40811  trlnle  40822  cdlemc  40833  cdlemd4  40837  cdlemd5  40838  cdlemd9  40842  cdlemd  40843  ltrneq3  40844  cdlemefrs29pre00  41031  cdlemefrs29cpre1  41034  cdlemefrs29clN  41035  cdlemefrs32fva  41036  cdlemefr29exN  41038  cdlemefr27cl  41039  cdlemefs27cl  41049  cdlemefs32sn1aw  41050  cdleme32fva  41073  cdleme32d  41080  cdleme32f  41082  cdleme32le  41083  cdleme40n  41104  cdleme41snaw  41112  cdleme17d3  41132  cdleme48fvg  41136  cdlemeg46fvcl  41142  cdlemeg46fgN  41170  cdleme48fgv  41174  ltrniotavalbN  41220  cdlemb3  41242  cdlemg15  41292  cdlemg17dN  41299  trlco  41363  cdlemg44b  41368  ltrncom  41374  trljco  41376  tendococl  41408  tendoplcl  41417  tendoplcom  41418  tendotr  41466  cdlemk36  41549  cdlemk35s-id  41574  cdlemk39s-id  41576  cdlemk19x  41579  cdlemk53b  41592  cdlemk55  41597  cdlemk35u  41600  cdlemk55u  41602  cdlemk39u  41604  cdlemk19u  41606  cdlemk56  41607  tendoex  41611  cdleml5N  41616  dihord2pre  41861  dihord6apre  41892  dihord5b  41895  dihord5apre  41898  dihord  41900  dihmeetlem1N  41926  dihmeetlem2N  41935  dihglbcpreN  41936  dihmeetbN  41939  dihmeetlem4preN  41942  dihmeetlem5  41944  dihmeetlem6  41945  dihmeetlem7N  41946  dihmeetlem10N  41952  dihmeetlem11N  41953  dihmeetlem12N  41954  dihmeetlem13N  41955  dihmeetlem15N  41957  dihmeetlem17N  41959  dihmeetlem18N  41960  dihmeetlem19N  41961  dihmeetALTN  41963  dih1dimatlem0  41964  dihlspsnssN  41968  dvh3dim2  42084  sticksstones1  42775  sticksstones2  42776  sticksstones12  42787  aks6d1c6isolem1  42803  dvdsexpnn  42954  resubcan2  43009  mzpsubst  43341  diophrw  43352  eldioph2lem1  43353  rencldnfi  43410  pellexlem2  43419  pellqrexplicit  43466  infmrgelbi  43467  rmxycomplete  43506  congadd  43555  acongeq  43572  jm2.19  43582  jm2.22  43584  jm2.20nn  43586  jm2.25lem1  43587  jm2.27  43597  jm3.1  43609  lmhmlnmsplit  43676  pwssplit4  43678  hbtlem2  43713  dgraa0p  43738  proot1hash  43784  iocunico  43800  cantnf2  43914  dflim5  43918  omcl2  43922  tfsconcatrn  43931  nadd2rabex  43975  relexpxpmin  44305  brtrclfv2  44315  ntrclsk3  44658  grur1cld  44820  ismnu  44835  suprnmpt  45750  wessf1ornlem  45761  choicefi  45775  supxrgere  45907  supxrgelem  45911  supxrge  45912  infleinflem2  45944  snunioo1  46086  iccintsng  46097  fmul01  46154  lptre2pt  46212  0ellimcdiv  46221  fnlimfvre  46246  limsupmnfuzlem  46298  climisp  46318  limsupgtlem  46349  ibliccsinexp  46523  iblioosinexp  46525  volioc  46544  iblspltprt  46545  stoweidlem20  46592  stoweidlem22  46594  stoweidlem34  46606  stoweidlem44  46616  stoweidlem60  46632  wallispilem3  46639  fourierdlem42  46721  fourierdlem51  46729  fourierdlem54  46732  fourierdlem87  46765  fourierdlem97  46775  ioorrnopnlem  46876  sge0seq  47018  hoicvr  47120  fsupdm  47414  finfdm  47418  3f1oss1  47667  funfocofob  47670  imasetpreimafvbijlemfv  48006  uhgrimisgrgric  48551  uhgrimgrlim  48607  fprmappr  48976  lincresunit3lem3  49105  lindssnlvec  49117  rrx2linesl  49374  line2  49383  itsclc0lem3  49389  itsclc0yqsollem1  49393  itscnhlc0xyqsol  49396  itschlc0xyqsol1  49397  itsclc0  49402  itscnhlinecirc02plem2  49414  itscnhlinecirc02plem3  49415  uptrlem1  49839  uptr2  49850  setc1onsubc  50231