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  4407  predtrss  6295  frpomin  6313  f1prex  7259  fcofo  7263  soisores  7302  weniso  7329  knatar  7332  ofmpteq  7676  funelss  8026  frrlem10  8274  fprlem1  8279  smocdmdom  8337  nnmord  8596  nnmword  8597  naddasslem1  8658  naddasslem2  8659  difsnen  9023  mapunen  9110  ac6sfi  9231  fipreima  9309  wemaplem2  9500  wemapso2lem  9505  ttrclselem2  9679  en2eqpr  9960  indcardi  9994  acndom  10004  fodomfi2  10013  infmap2  10170  cflim2  10216  coftr  10226  infpssrlem4  10259  fin23lem11  10270  fincssdom  10276  isf32lem9  10314  fin1a2lem9  10361  gchpwdom  10623  gruima  10755  prpssnq  10943  distrlem4pr  10979  dedekind  11337  addcan  11358  addcan2  11359  divmulass  11860  supmul1  12152  uzsupss  12899  xaddass  13209  xleadd1a  13213  xlesubadd  13223  xmulasslem3  13246  xmulass  13247  xadddilem  13254  xadddi  13255  ixxun  13322  icoshftf1o  13435  snunioc  13441  difelfzle  13602  fzo1fzo0n0  13676  ssfzoulel  13721  modmuladd  13878  modifeq2int  13898  modaddmulmod  13903  modsubdir  13905  ltexp2a  14131  leexp2  14136  ltexp2r  14138  exple1  14142  expnlbnd2  14199  mulsubdivbinom2  14227  hashtpg  14450  ccatass  14553  ccatopth  14681  pfxccatin12lem2a  14692  pfxccat3  14699  cshinj  14776  2cshw  14778  s2f1o  14882  limsupgre  15447  addcn2  15560  mulcn2  15562  binomrisefac  16008  bpolydif  16021  dvdsmodexp  16230  modmulconst  16258  dvdsexp2im  16297  dvdsmod  16299  sadass  16441  gcdass  16517  rplpwr  16528  rpmulgcd2  16626  rpdvds  16630  rpexp  16692  prmdiveq  16756  hashgcdlem  16758  coprimeprodsq  16779  coprimeprodsq2  16780  pythagtriplem3  16789  pcdvdsb  16840  pcgcd1  16848  dvdsprmpweq  16855  pcbc  16871  0ram  16991  ramz2  16995  ramub1lem1  16997  mremre  17565  mrieqv2d  17600  lubun  18474  isnsgrp  18650  issubmnd  18688  frmdss2  18790  submefmnd  18822  sgrp2rid2ex  18854  mulgnn0p1  19017  mulgnnsubcl  19018  mulgneg  19024  mulgdirlem  19037  nmzsubg  19097  ghmmulg  19160  pmtrfv  19382  pmtrmvd  19386  pmtrfb  19395  odmodnn0  19470  oddvdsnn0  19474  odnncl  19475  odmod  19476  oddvds  19477  odeq  19480  odmulgid  19484  odmulg  19486  odmulgeq  19487  odbezout  19488  odf1o1  19502  odf1o2  19503  odngen  19507  odcau  19534  pgpssslw  19544  fislw  19555  lsmless1x  19574  lsmless2x  19575  lsmsubm  19583  lsmmod  19605  lsmmod2  19606  efgsfo  19669  cntzcmn  19770  odadd1  19778  odadd2  19779  odadd  19780  lsmcomx  19786  prdscmnd  19791  gsumconst  19864  ring1eq0  20207  cntzsubrng  20476  cntzsubr  20515  isabvd  20721  rmodislmod  20836  lspss  20890  0lmhm  20947  reslmhm2  20960  pwssplit0  20965  pwssplit1  20966  lbspss  20989  lspfixed  21038  lsmcv  21051  lspsnat  21055  2idlcpblrng  21181  cnfldfunALT  21279  cnfldfunALTOLD  21292  xrsdsreclblem  21329  obselocv  21637  frlmsplit2  21682  frlmsslss2  21684  frlmup4  21710  lindff1  21729  lsslindf  21739  lsslinds  21740  islindf4  21747  issubassa  21776  aspss  21786  coe1subfv  22152  coe1tm  22159  mpomatmul  22333  mamutpos  22345  submaval  22468  mdetdiag  22486  mdetunilem1  22499  mdetunilem3  22501  mdetunilem9  22507  mdetmul  22510  maducoeval2  22527  madurid  22531  minmar1val  22535  cramer  22578  cpmatel2  22600  m2cpm  22628  decpmatmul  22659  pmatcollpw1lem2  22662  pmatcollpw1  22663  pmatcollpw2lem  22664  pm2mpcl  22684  mply1topmatcl  22692  mp2pm2mplem2  22694  mp2pm2mplem4  22696  pm2mpghmlem2  22699  pm2mpghmlem1  22700  cayhamlem2  22771  neiint  22991  topssnei  23011  cnrest2  23173  cnprest2  23177  cnt0  23233  cnt1  23237  cnhaus  23241  cncmp  23279  fiuncmp  23291  sscmp  23292  hauscmp  23294  cnconn  23309  unconn  23316  comppfsc  23419  kgen2ss  23442  ptpjopn  23499  ptrescn  23526  qtopss  23602  kqfvima  23617  r0cld  23625  cmphaushmeo  23687  fbssint  23725  fbasrn  23771  filuni  23772  ufilmax  23794  fin1aufil  23819  fmf  23832  fmss  23833  rnelfmlem  23839  rnelfm  23840  fmufil  23846  fmco  23848  flimss2  23859  flimss1  23860  flimrest  23870  cnpflf2  23887  cnpflf  23888  flfcnp  23891  lmflf  23892  supnfcls  23907  fclsss1  23909  fclsss2  23910  cnpfcfi  23927  subgntr  23994  opnsubg  23995  cldsubg  23998  ustuqtop1  24129  ucncn  24172  bldisj  24286  blgt0  24287  bl2in  24288  blss2ps  24291  blss2  24292  xbln0  24302  blssps  24312  blss  24313  lpbl  24391  blcld  24393  blcls  24394  stdbdmopn  24406  metcnp2  24430  txmetcnp  24435  blval2  24450  restmetu  24458  nmoix  24617  nmoi2  24618  nmoeq0  24624  nmotri  24627  metdsge  24738  metds0  24739  metdseq0  24743  icoopnst  24836  iccpnfhmeo  24843  xrhmeo  24844  nmhmcn  25020  cphsqrtcl2  25086  cphsqrtcl3  25087  fmcfil  25172  bcthlem5  25228  cmetcusp1  25253  cssbn  25275  pjth  25339  ovolunnul  25401  volun  25446  voliunlem2  25452  itg2const  25641  iblconst  25719  itgconst  25720  limcvallem  25772  dvcnp2  25821  dvcnp2OLD  25822  dvcn  25823  deg1mul3le  26022  deg1tmle  26023  idomrootle  26078  ig1pdvds  26085  coe11  26158  dgrmulc  26177  dvply1  26191  aaliou2  26248  efcvx  26359  tanord  26447  logdivlti  26529  logccv  26572  recxpcl  26584  cxplea  26605  cxple2a  26608  ang180  26724  isosctrlem2  26729  cxp2lim  26887  amgm  26901  muval1  27043  dvdssqf  27048  mumullem2  27090  bcmono  27188  lgsneg  27232  lgsmod  27234  lgsdirprm  27242  lgsdir  27243  lgsdi  27245  sltres  27574  nolt02olem  27606  nolt02o  27607  nogt01o  27608  nosupbnd1lem1  27620  nosupbnd1lem4  27623  nosupbnd1lem5  27624  nosupbnd1lem6  27625  noinfbnd1lem1  27635  noinfbnd1lem4  27638  noinfbnd1lem6  27640  noinfbnd2  27643  noetainflem3  27651  sltlpss  27819  cofsslt  27826  coinitsslt  27827  cofcutrtime  27835  addsass  27912  addsdi  28058  mulsass  28069  sltmul2  28074  norecdiv  28093  brbtwn2  28832  colinearalglem1  28833  colinearalg  28837  axcgrtr  28842  axcontlem2  28892  upgrewlkle2  29534  wlksoneq1eq2  29592  crctcshwlkn0lem5  29744  wspthsnwspthsnon  29846  lppthon  30080  upgriseupth  30136  4cyclusnfrgr  30221  numclwwlk1lem2foa  30283  numclwwlk5  30317  nvmul0or  30579  shless  31288  shlej1  31289  pjspansn  31506  kbmul  31884  homco2  31906  kbass2  32046  fnpreimac  32595  padct  32643  eliccelico  32700  elicoelioo  32701  iocinioc2  32702  difioo  32705  nexple  32769  swrdrn2  32876  swrdrn3  32877  xrge0npcan  32961  isarchi2  33139  archiabl  33152  pidlnz  33347  lindssn  33349  ssmxidl  33445  mdetlap1  33816  zarclsiin  33861  pstmfval  33886  fmcncfil  33921  zrhnm  33957  qqhnm  33980  volfiniune  34220  omsmeas  34314  eulerpartlemb  34359  probinc  34412  cndprob01  34426  signswmnd  34548  cvmsss2  35261  funsseq  35755  cgrtriv  35990  5segofs  35994  btwntriv2  36000  btwnxfr  36044  segcon2  36093  brsegle2  36097  seglelin  36104  outsideofeu  36119  weiunpo  36453  weiunfr  36455  weiunse  36456  lindsenlbs  37609  mblfinlem2  37652  blbnd  37781  rrndstprj2  37825  zerdivemp1x  37941  lsmsat  39001  lsatfixedN  39002  lssat  39009  lkrlsp  39095  lshpkrlem4  39106  cvrcon3b  39270  leat3  39288  atlen0  39303  atnle  39310  atlatmstc  39312  atlatle  39313  cvlcvr1  39332  cvlsupr2  39336  hlsupr2  39381  hlrelat2  39397  cvrexchlem  39413  cvratlem  39415  lnnat  39421  atexchcvrN  39434  1cvratlt  39468  1cvrjat  39469  3atlem3  39479  3atlem7  39483  llni2  39506  atcvrlln2  39513  llnexatN  39515  llncmp  39516  2llnmat  39518  2at0mat0  39519  2atnelpln  39538  llncvrlpln2  39551  2lplnmN  39553  2llnmj  39554  lplncmp  39556  lplnexatN  39557  2llnjaN  39560  lvoli3  39571  islvol2aN  39586  4atlem3a  39591  4atlem4a  39593  4atlem4b  39594  4atlem11  39603  4atlem12  39606  lplncvrlvol2  39609  lvolcmp  39611  2lplnmj  39616  islinei  39734  linepmap  39769  lneq2at  39772  2llnma3r  39782  elpaddn0  39794  elpaddatriN  39797  elpaddat  39798  paddcom  39807  paddss1  39811  paddss2  39812  paddasslem6  39819  paddasslem7  39820  paddasslem10  39823  paddasslem15  39828  pmodlem2  39841  pmodl42N  39845  pmapjoin  39846  atmod1i1m  39852  llnmod1i2  39854  llnexchb2lem  39862  polcon2bN  39914  pclfinclN  39944  poml4N  39947  poml6N  39949  osumcllem11N  39960  osumclN  39961  pmapojoinN  39962  pexmidlem2N  39965  pexmidlem3N  39966  pexmidlem4N  39967  pexmidlem6N  39969  pexmidlem7N  39970  pl42lem2N  39974  pl42lem3N  39975  pl42lem4N  39976  pl42N  39977  lhpexle3lem  40005  lhpmcvr3  40019  lhp2at0nle  40029  lhprelat3N  40034  lauteq  40089  lautco  40091  ltrncoidN  40122  ltrneq2  40142  ltrnnidn  40168  ltrnideq  40169  trlnle  40180  cdlemc  40191  cdlemd4  40195  cdlemd5  40196  cdlemd9  40200  cdlemd  40201  ltrneq3  40202  cdlemefrs29pre00  40389  cdlemefrs29cpre1  40392  cdlemefrs29clN  40393  cdlemefrs32fva  40394  cdlemefr29exN  40396  cdlemefr27cl  40397  cdlemefs27cl  40407  cdlemefs32sn1aw  40408  cdleme32fva  40431  cdleme32d  40438  cdleme32f  40440  cdleme32le  40441  cdleme40n  40462  cdleme41snaw  40470  cdleme17d3  40490  cdleme48fvg  40494  cdlemeg46fvcl  40500  cdlemeg46fgN  40528  cdleme48fgv  40532  ltrniotavalbN  40578  cdlemb3  40600  cdlemg15  40650  cdlemg17dN  40657  trlco  40721  cdlemg44b  40726  ltrncom  40732  trljco  40734  tendococl  40766  tendoplcl  40775  tendoplcom  40776  tendotr  40824  cdlemk36  40907  cdlemk35s-id  40932  cdlemk39s-id  40934  cdlemk19x  40937  cdlemk53b  40950  cdlemk55  40955  cdlemk35u  40958  cdlemk55u  40960  cdlemk39u  40962  cdlemk19u  40964  cdlemk56  40965  tendoex  40969  cdleml5N  40974  dihord2pre  41219  dihord6apre  41250  dihord5b  41253  dihord5apre  41256  dihord  41258  dihmeetlem1N  41284  dihmeetlem2N  41293  dihglbcpreN  41294  dihmeetbN  41297  dihmeetlem4preN  41300  dihmeetlem5  41302  dihmeetlem6  41303  dihmeetlem7N  41304  dihmeetlem10N  41310  dihmeetlem11N  41311  dihmeetlem12N  41312  dihmeetlem13N  41313  dihmeetlem15N  41315  dihmeetlem17N  41317  dihmeetlem18N  41318  dihmeetlem19N  41319  dihmeetALTN  41321  dih1dimatlem0  41322  dihlspsnssN  41326  dvh3dim2  41442  sticksstones1  42134  sticksstones2  42135  sticksstones12  42146  aks6d1c6isolem1  42162  dvdsexpnn  42321  resubcan2  42376  mzpsubst  42736  diophrw  42747  eldioph2lem1  42748  rencldnfi  42809  pellexlem2  42818  pellqrexplicit  42865  infmrgelbi  42866  rmxycomplete  42906  congadd  42955  acongeq  42972  jm2.19  42982  jm2.22  42984  jm2.20nn  42986  jm2.25lem1  42987  jm2.27  42997  jm3.1  43009  lmhmlnmsplit  43076  pwssplit4  43078  hbtlem2  43113  dgraa0p  43138  proot1hash  43184  iocunico  43200  cantnf2  43314  dflim5  43318  omcl2  43322  tfsconcatrn  43331  nadd2rabex  43375  relexpxpmin  43706  brtrclfv2  43716  ntrclsk3  44059  grur1cld  44221  ismnu  44250  suprnmpt  45168  wessf1ornlem  45179  choicefi  45194  supxrgere  45329  supxrgelem  45333  supxrge  45334  infleinflem2  45367  snunioo1  45510  iccintsng  45521  fmul01  45578  lptre2pt  45638  0ellimcdiv  45647  fnlimfvre  45672  limsupmnfuzlem  45724  climisp  45744  limsupgtlem  45775  ibliccsinexp  45949  iblioosinexp  45951  volioc  45970  iblspltprt  45971  stoweidlem20  46018  stoweidlem22  46020  stoweidlem34  46032  stoweidlem44  46042  stoweidlem60  46058  wallispilem3  46065  fourierdlem42  46147  fourierdlem51  46155  fourierdlem54  46158  fourierdlem87  46191  fourierdlem97  46201  ioorrnopnlem  46302  sge0seq  46444  hoicvr  46546  fsupdm  46840  finfdm  46844  3f1oss1  47076  funfocofob  47079  imasetpreimafvbijlemfv  47403  uhgrimisgrgric  47931  uhgrimgrlim  47986  fprmappr  48333  lincresunit3lem3  48463  lindssnlvec  48475  rrx2linesl  48732  line2  48741  itsclc0lem3  48747  itsclc0yqsollem1  48751  itscnhlc0xyqsol  48754  itschlc0xyqsol1  48755  itsclc0  48760  itscnhlinecirc02plem2  48772  itscnhlinecirc02plem3  48773  uptrlem1  49199  uptr2  49210  setc1onsubc  49591