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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  simpl13  1251  simpl23  1254  simpl33  1257  simp1l3  1269  simp2l3  1275  simp3l3  1281  3anandirs  1473  2nreu  4442  predtrss  6324  frpomin  6342  f1prex  7282  fcofo  7286  soisores  7324  weniso  7351  knatar  7354  ofmpteq  7692  funelss  8033  frrlem10  8280  fprlem1  8285  smocdmdom  8368  nnmord  8632  nnmword  8633  naddasslem1  8693  naddasslem2  8694  difsnen  9053  mapunen  9146  ac6sfi  9287  fipreima  9358  wemaplem2  9542  wemapso2lem  9547  ttrclselem2  9721  en2eqpr  10002  indcardi  10036  acndom  10046  fodomfi2  10055  infmap2  10213  cflim2  10258  coftr  10268  infpssrlem4  10301  fin23lem11  10312  fincssdom  10318  isf32lem9  10356  fin1a2lem9  10403  gchpwdom  10665  gruima  10797  prpssnq  10985  distrlem4pr  11021  dedekind  11377  addcan  11398  addcan2  11399  divmulass  11895  supmul1  12183  uzsupss  12924  xaddass  13228  xleadd1a  13232  xlesubadd  13242  xmulasslem3  13265  xmulass  13266  xadddilem  13273  xadddi  13274  ixxun  13340  icoshftf1o  13451  snunioc  13457  difelfzle  13614  fzo1fzo0n0  13683  ssfzoulel  13726  modmuladd  13878  modifeq2int  13898  modaddmulmod  13903  modsubdir  13905  ltexp2a  14131  leexp2  14136  ltexp2r  14138  exple1  14141  expnlbnd2  14197  mulsubdivbinom2  14222  hashtpg  14446  ccatass  14538  ccatopth  14666  pfxccatin12lem2a  14677  pfxccat3  14684  cshinj  14761  2cshw  14763  s2f1o  14867  limsupgre  15425  addcn2  15538  mulcn2  15540  binomrisefac  15986  bpolydif  15999  dvdsmodexp  16205  modmulconst  16231  dvdsexp2im  16270  dvdsmod  16272  sadass  16412  gcdass  16489  rplpwr  16499  rpmulgcd2  16593  rpdvds  16597  rpexp  16659  prmdiveq  16719  hashgcdlem  16721  coprimeprodsq  16741  coprimeprodsq2  16742  pythagtriplem3  16751  pcdvdsb  16802  pcgcd1  16810  dvdsprmpweq  16817  pcbc  16833  0ram  16953  ramz2  16957  ramub1lem1  16959  mremre  17548  mrieqv2d  17583  lubun  18468  isnsgrp  18614  issubmnd  18652  frmdss2  18744  submefmnd  18776  sgrp2rid2ex  18808  mulgnn0p1  18965  mulgnnsubcl  18966  mulgneg  18972  mulgdirlem  18985  nmzsubg  19045  ghmmulg  19104  pmtrfv  19320  pmtrmvd  19324  pmtrfb  19333  odmodnn0  19408  oddvdsnn0  19412  odnncl  19413  odmod  19414  oddvds  19415  odeq  19418  odmulgid  19422  odmulg  19424  odmulgeq  19425  odbezout  19426  odf1o1  19440  odf1o2  19441  odngen  19445  odcau  19472  pgpssslw  19482  fislw  19493  lsmless1x  19512  lsmless2x  19513  lsmsubm  19521  lsmmod  19543  lsmmod2  19544  efgsfo  19607  cntzcmn  19708  odadd1  19716  odadd2  19717  odadd  19718  lsmcomx  19724  prdscmnd  19729  gsumconst  19802  ring1eq0  20110  cntzsubr  20353  isabvd  20428  rmodislmod  20540  rmodislmodOLD  20541  lspss  20595  0lmhm  20651  reslmhm2  20664  pwssplit0  20669  pwssplit1  20670  lbspss  20693  lspfixed  20741  lsmcv  20754  lspsnat  20758  cnfldfunALT  20957  xrsdsreclblem  20991  obselocv  21283  frlmsplit2  21328  frlmsslss2  21330  frlmup4  21356  lindff1  21375  lsslindf  21385  lsslinds  21386  islindf4  21393  issubassa  21421  aspss  21431  coe1subfv  21788  coe1tm  21795  mpomatmul  21948  mamutpos  21960  submaval  22083  mdetdiag  22101  mdetunilem1  22114  mdetunilem3  22116  mdetunilem9  22122  mdetmul  22125  maducoeval2  22142  madurid  22146  minmar1val  22150  cramer  22193  cpmatel2  22215  m2cpm  22243  decpmatmul  22274  pmatcollpw1lem2  22277  pmatcollpw1  22278  pmatcollpw2lem  22279  pm2mpcl  22299  mply1topmatcl  22307  mp2pm2mplem2  22309  mp2pm2mplem4  22311  pm2mpghmlem2  22314  pm2mpghmlem1  22315  cayhamlem2  22386  neiint  22608  topssnei  22628  cnrest2  22790  cnprest2  22794  cnt0  22850  cnt1  22854  cnhaus  22858  cncmp  22896  fiuncmp  22908  sscmp  22909  hauscmp  22911  cnconn  22926  unconn  22933  comppfsc  23036  kgen2ss  23059  ptpjopn  23116  ptrescn  23143  qtopss  23219  kqfvima  23234  r0cld  23242  cmphaushmeo  23304  fbssint  23342  fbasrn  23388  filuni  23389  ufilmax  23411  fin1aufil  23436  fmf  23449  fmss  23450  rnelfmlem  23456  rnelfm  23457  fmufil  23463  fmco  23465  flimss2  23476  flimss1  23477  flimrest  23487  cnpflf2  23504  cnpflf  23505  flfcnp  23508  lmflf  23509  supnfcls  23524  fclsss1  23526  fclsss2  23527  cnpfcfi  23544  subgntr  23611  opnsubg  23612  cldsubg  23615  ustuqtop1  23746  ucncn  23790  bldisj  23904  blgt0  23905  bl2in  23906  blss2ps  23909  blss2  23910  xbln0  23920  blssps  23930  blss  23931  lpbl  24012  blcld  24014  blcls  24015  stdbdmopn  24027  metcnp2  24051  txmetcnp  24056  blval2  24071  restmetu  24079  nmoix  24246  nmoi2  24247  nmoeq0  24253  nmotri  24256  metdsge  24365  metds0  24366  metdseq0  24370  icoopnst  24455  iccpnfhmeo  24461  xrhmeo  24462  nmhmcn  24636  cphsqrtcl2  24703  cphsqrtcl3  24704  fmcfil  24789  bcthlem5  24845  cmetcusp1  24870  cssbn  24892  pjth  24956  ovolunnul  25017  volun  25062  voliunlem2  25068  itg2const  25258  iblconst  25335  itgconst  25336  limcvallem  25388  dvcnp2  25437  dvcn  25438  deg1mul3le  25634  deg1tmle  25635  ig1pdvds  25694  coe11  25767  dgrmulc  25785  dvply1  25797  aaliou2  25853  efcvx  25961  tanord  26047  logdivlti  26128  logccv  26171  recxpcl  26183  cxplea  26204  cxple2a  26207  ang180  26319  isosctrlem2  26324  cxp2lim  26481  amgm  26495  muval1  26637  dvdssqf  26642  mumullem2  26684  bcmono  26780  lgsneg  26824  lgsmod  26826  lgsdirprm  26834  lgsdir  26835  lgsdi  26837  sltres  27165  nolt02olem  27197  nolt02o  27198  nogt01o  27199  nosupbnd1lem1  27211  nosupbnd1lem4  27214  nosupbnd1lem5  27215  nosupbnd1lem6  27216  noinfbnd1lem1  27226  noinfbnd1lem4  27229  noinfbnd1lem6  27231  noinfbnd2  27234  noetainflem3  27242  sltlpss  27401  cofsslt  27405  coinitsslt  27406  cofcutrtime  27414  addsass  27488  addsdi  27610  mulsass  27621  sltmul2  27623  norecdiv  27638  brbtwn2  28163  colinearalglem1  28164  colinearalg  28168  axcgrtr  28173  axcontlem2  28223  upgrewlkle2  28863  wlksoneq1eq2  28921  crctcshwlkn0lem5  29068  wspthsnwspthsnon  29170  lppthon  29404  upgriseupth  29460  4cyclusnfrgr  29545  numclwwlk1lem2foa  29607  numclwwlk5  29641  nvmul0or  29903  shless  30612  shlej1  30613  pjspansn  30830  kbmul  31208  homco2  31230  kbass2  31370  fnpreimac  31896  padct  31944  eliccelico  31988  elicoelioo  31989  iocinioc2  31990  difioo  31993  swrdrn2  32118  swrdrn3  32119  xrge0npcan  32195  isarchi2  32331  archiabl  32344  pidlnz  32488  lindssn  32494  ssmxidl  32590  mdetlap1  32806  zarclsiin  32851  pstmfval  32876  fmcncfil  32911  zrhnm  32949  qqhnm  32970  nexple  33007  volfiniune  33228  omsmeas  33322  eulerpartlemb  33367  probinc  33420  cndprob01  33434  signswmnd  33568  cvmsss2  34265  funsseq  34739  cgrtriv  34974  5segofs  34978  btwntriv2  34984  btwnxfr  35028  segcon2  35077  brsegle2  35081  seglelin  35088  outsideofeu  35103  gg-dvcnp2  35174  lindsenlbs  36483  mblfinlem2  36526  blbnd  36655  rrndstprj2  36699  zerdivemp1x  36815  lsmsat  37878  lsatfixedN  37879  lssat  37886  lkrlsp  37972  lshpkrlem4  37983  cvrcon3b  38147  leat3  38165  atlen0  38180  atnle  38187  atlatmstc  38189  atlatle  38190  cvlcvr1  38209  cvlsupr2  38213  hlsupr2  38258  hlrelat2  38274  cvrexchlem  38290  cvratlem  38292  lnnat  38298  atexchcvrN  38311  1cvratlt  38345  1cvrjat  38346  3atlem3  38356  3atlem7  38360  llni2  38383  atcvrlln2  38390  llnexatN  38392  llncmp  38393  2llnmat  38395  2at0mat0  38396  2atnelpln  38415  llncvrlpln2  38428  2lplnmN  38430  2llnmj  38431  lplncmp  38433  lplnexatN  38434  2llnjaN  38437  lvoli3  38448  islvol2aN  38463  4atlem3a  38468  4atlem4a  38470  4atlem4b  38471  4atlem11  38480  4atlem12  38483  lplncvrlvol2  38486  lvolcmp  38488  2lplnmj  38493  islinei  38611  linepmap  38646  lneq2at  38649  2llnma3r  38659  elpaddn0  38671  elpaddatriN  38674  elpaddat  38675  paddcom  38684  paddss1  38688  paddss2  38689  paddasslem6  38696  paddasslem7  38697  paddasslem10  38700  paddasslem15  38705  pmodlem2  38718  pmodl42N  38722  pmapjoin  38723  atmod1i1m  38729  llnmod1i2  38731  llnexchb2lem  38739  polcon2bN  38791  pclfinclN  38821  poml4N  38824  poml6N  38826  osumcllem11N  38837  osumclN  38838  pmapojoinN  38839  pexmidlem2N  38842  pexmidlem3N  38843  pexmidlem4N  38844  pexmidlem6N  38846  pexmidlem7N  38847  pl42lem2N  38851  pl42lem3N  38852  pl42lem4N  38853  pl42N  38854  lhpexle3lem  38882  lhpmcvr3  38896  lhp2at0nle  38906  lhprelat3N  38911  lauteq  38966  lautco  38968  ltrncoidN  38999  ltrneq2  39019  ltrnnidn  39045  ltrnideq  39046  trlnle  39057  cdlemc  39068  cdlemd4  39072  cdlemd5  39073  cdlemd9  39077  cdlemd  39078  ltrneq3  39079  cdlemefrs29pre00  39266  cdlemefrs29cpre1  39269  cdlemefrs29clN  39270  cdlemefrs32fva  39271  cdlemefr29exN  39273  cdlemefr27cl  39274  cdlemefs27cl  39284  cdlemefs32sn1aw  39285  cdleme32fva  39308  cdleme32d  39315  cdleme32f  39317  cdleme32le  39318  cdleme40n  39339  cdleme41snaw  39347  cdleme17d3  39367  cdleme48fvg  39371  cdlemeg46fvcl  39377  cdlemeg46fgN  39405  cdleme48fgv  39409  ltrniotavalbN  39455  cdlemb3  39477  cdlemg15  39527  cdlemg17dN  39534  trlco  39598  cdlemg44b  39603  ltrncom  39609  trljco  39611  tendococl  39643  tendoplcl  39652  tendoplcom  39653  tendotr  39701  cdlemk36  39784  cdlemk35s-id  39809  cdlemk39s-id  39811  cdlemk19x  39814  cdlemk53b  39827  cdlemk55  39832  cdlemk35u  39835  cdlemk55u  39837  cdlemk39u  39839  cdlemk19u  39841  cdlemk56  39842  tendoex  39846  cdleml5N  39851  dihord2pre  40096  dihord6apre  40127  dihord5b  40130  dihord5apre  40133  dihord  40135  dihmeetlem1N  40161  dihmeetlem2N  40170  dihglbcpreN  40171  dihmeetbN  40174  dihmeetlem4preN  40177  dihmeetlem5  40179  dihmeetlem6  40180  dihmeetlem7N  40181  dihmeetlem10N  40187  dihmeetlem11N  40188  dihmeetlem12N  40189  dihmeetlem13N  40190  dihmeetlem15N  40192  dihmeetlem17N  40194  dihmeetlem18N  40195  dihmeetlem19N  40196  dihmeetALTN  40198  dih1dimatlem0  40199  dihlspsnssN  40203  dvh3dim2  40319  sticksstones1  40962  sticksstones2  40963  sticksstones12  40974  dvdsexpnn  41231  resubcan2  41261  mzpsubst  41486  diophrw  41497  eldioph2lem1  41498  rencldnfi  41559  pellexlem2  41568  pellqrexplicit  41615  infmrgelbi  41616  rmxycomplete  41656  congadd  41705  acongeq  41722  jm2.19  41732  jm2.22  41734  jm2.20nn  41736  jm2.25lem1  41737  jm2.27  41747  jm3.1  41759  lmhmlnmsplit  41829  pwssplit4  41831  hbtlem2  41866  dgraa0p  41891  idomrootle  41937  proot1hash  41942  iocunico  41960  cantnf2  42075  dflim5  42079  omcl2  42083  tfsconcatrn  42092  nadd2rabex  42136  relexpxpmin  42468  brtrclfv2  42478  ntrclsk3  42821  grur1cld  42991  ismnu  43020  suprnmpt  43870  wessf1ornlem  43882  choicefi  43899  supxrgere  44043  supxrgelem  44047  supxrge  44048  infleinflem2  44081  snunioo1  44225  iccintsng  44236  fmul01  44296  lptre2pt  44356  0ellimcdiv  44365  fnlimfvre  44390  limsupmnfuzlem  44442  climisp  44462  limsupgtlem  44493  ibliccsinexp  44667  iblioosinexp  44669  volioc  44688  iblspltprt  44689  stoweidlem20  44736  stoweidlem22  44738  stoweidlem34  44750  stoweidlem44  44760  stoweidlem60  44776  wallispilem3  44783  fourierdlem42  44865  fourierdlem51  44873  fourierdlem54  44876  fourierdlem87  44909  fourierdlem97  44919  ioorrnopnlem  45020  sge0seq  45162  hoicvr  45264  fsupdm  45558  finfdm  45562  funfocofob  45786  imasetpreimafvbijlemfv  46070  cntzsubrng  46746  2idlcpblrng  46766  fprmappr  47021  lincresunit3lem3  47155  lindssnlvec  47167  rrx2linesl  47429  line2  47438  itsclc0lem3  47444  itsclc0yqsollem1  47448  itscnhlc0xyqsol  47451  itschlc0xyqsol1  47452  itsclc0  47457  itscnhlinecirc02plem2  47469  itscnhlinecirc02plem3  47470