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 1087

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 1089

This theorem is referenced by:  simpl13  1251  simpl23  1254  simpl33  1257  simp1l3  1269  simp2l3  1275  simp3l3  1281  3anandirs  1474  2nreu  4444  predtrss  6343  frpomin  6361  f1prex  7304  fcofo  7308  soisores  7347  weniso  7374  knatar  7377  ofmpteq  7720  funelss  8072  frrlem10  8320  fprlem1  8325  smocdmdom  8408  nnmord  8670  nnmword  8671  naddasslem1  8732  naddasslem2  8733  difsnen  9093  mapunen  9186  ac6sfi  9320  fipreima  9398  wemaplem2  9587  wemapso2lem  9592  ttrclselem2  9766  en2eqpr  10047  indcardi  10081  acndom  10091  fodomfi2  10100  infmap2  10257  cflim2  10303  coftr  10313  infpssrlem4  10346  fin23lem11  10357  fincssdom  10363  isf32lem9  10401  fin1a2lem9  10448  gchpwdom  10710  gruima  10842  prpssnq  11030  distrlem4pr  11066  dedekind  11424  addcan  11445  addcan2  11446  divmulass  11945  supmul1  12237  uzsupss  12982  xaddass  13291  xleadd1a  13295  xlesubadd  13305  xmulasslem3  13328  xmulass  13329  xadddilem  13336  xadddi  13337  ixxun  13403  icoshftf1o  13514  snunioc  13520  difelfzle  13681  fzo1fzo0n0  13754  ssfzoulel  13799  modmuladd  13954  modifeq2int  13974  modaddmulmod  13979  modsubdir  13981  ltexp2a  14206  leexp2  14211  ltexp2r  14213  exple1  14216  expnlbnd2  14273  mulsubdivbinom2  14301  hashtpg  14524  ccatass  14626  ccatopth  14754  pfxccatin12lem2a  14765  pfxccat3  14772  cshinj  14849  2cshw  14851  s2f1o  14955  limsupgre  15517  addcn2  15630  mulcn2  15632  binomrisefac  16078  bpolydif  16091  dvdsmodexp  16298  modmulconst  16325  dvdsexp2im  16364  dvdsmod  16366  sadass  16508  gcdass  16584  rplpwr  16595  rpmulgcd2  16693  rpdvds  16697  rpexp  16759  prmdiveq  16823  hashgcdlem  16825  coprimeprodsq  16846  coprimeprodsq2  16847  pythagtriplem3  16856  pcdvdsb  16907  pcgcd1  16915  dvdsprmpweq  16922  pcbc  16938  0ram  17058  ramz2  17062  ramub1lem1  17064  mremre  17647  mrieqv2d  17682  lubun  18560  isnsgrp  18736  issubmnd  18774  frmdss2  18876  submefmnd  18908  sgrp2rid2ex  18940  mulgnn0p1  19103  mulgnnsubcl  19104  mulgneg  19110  mulgdirlem  19123  nmzsubg  19183  ghmmulg  19246  pmtrfv  19470  pmtrmvd  19474  pmtrfb  19483  odmodnn0  19558  oddvdsnn0  19562  odnncl  19563  odmod  19564  oddvds  19565  odeq  19568  odmulgid  19572  odmulg  19574  odmulgeq  19575  odbezout  19576  odf1o1  19590  odf1o2  19591  odngen  19595  odcau  19622  pgpssslw  19632  fislw  19643  lsmless1x  19662  lsmless2x  19663  lsmsubm  19671  lsmmod  19693  lsmmod2  19694  efgsfo  19757  cntzcmn  19858  odadd1  19866  odadd2  19867  odadd  19868  lsmcomx  19874  prdscmnd  19879  gsumconst  19952  ring1eq0  20295  cntzsubrng  20567  cntzsubr  20606  isabvd  20813  rmodislmod  20928  lspss  20982  0lmhm  21039  reslmhm2  21052  pwssplit0  21057  pwssplit1  21058  lbspss  21081  lspfixed  21130  lsmcv  21143  lspsnat  21147  2idlcpblrng  21281  cnfldfunALT  21379  cnfldfunALTOLD  21392  xrsdsreclblem  21430  obselocv  21748  frlmsplit2  21793  frlmsslss2  21795  frlmup4  21821  lindff1  21840  lsslindf  21850  lsslinds  21851  islindf4  21858  issubassa  21887  aspss  21897  coe1subfv  22269  coe1tm  22276  mpomatmul  22452  mamutpos  22464  submaval  22587  mdetdiag  22605  mdetunilem1  22618  mdetunilem3  22620  mdetunilem9  22626  mdetmul  22629  maducoeval2  22646  madurid  22650  minmar1val  22654  cramer  22697  cpmatel2  22719  m2cpm  22747  decpmatmul  22778  pmatcollpw1lem2  22781  pmatcollpw1  22782  pmatcollpw2lem  22783  pm2mpcl  22803  mply1topmatcl  22811  mp2pm2mplem2  22813  mp2pm2mplem4  22815  pm2mpghmlem2  22818  pm2mpghmlem1  22819  cayhamlem2  22890  neiint  23112  topssnei  23132  cnrest2  23294  cnprest2  23298  cnt0  23354  cnt1  23358  cnhaus  23362  cncmp  23400  fiuncmp  23412  sscmp  23413  hauscmp  23415  cnconn  23430  unconn  23437  comppfsc  23540  kgen2ss  23563  ptpjopn  23620  ptrescn  23647  qtopss  23723  kqfvima  23738  r0cld  23746  cmphaushmeo  23808  fbssint  23846  fbasrn  23892  filuni  23893  ufilmax  23915  fin1aufil  23940  fmf  23953  fmss  23954  rnelfmlem  23960  rnelfm  23961  fmufil  23967  fmco  23969  flimss2  23980  flimss1  23981  flimrest  23991  cnpflf2  24008  cnpflf  24009  flfcnp  24012  lmflf  24013  supnfcls  24028  fclsss1  24030  fclsss2  24031  cnpfcfi  24048  subgntr  24115  opnsubg  24116  cldsubg  24119  ustuqtop1  24250  ucncn  24294  bldisj  24408  blgt0  24409  bl2in  24410  blss2ps  24413  blss2  24414  xbln0  24424  blssps  24434  blss  24435  lpbl  24516  blcld  24518  blcls  24519  stdbdmopn  24531  metcnp2  24555  txmetcnp  24560  blval2  24575  restmetu  24583  nmoix  24750  nmoi2  24751  nmoeq0  24757  nmotri  24760  metdsge  24871  metds0  24872  metdseq0  24876  icoopnst  24969  iccpnfhmeo  24976  xrhmeo  24977  nmhmcn  25153  cphsqrtcl2  25220  cphsqrtcl3  25221  fmcfil  25306  bcthlem5  25362  cmetcusp1  25387  cssbn  25409  pjth  25473  ovolunnul  25535  volun  25580  voliunlem2  25586  itg2const  25775  iblconst  25853  itgconst  25854  limcvallem  25906  dvcnp2  25955  dvcnp2OLD  25956  dvcn  25957  deg1mul3le  26156  deg1tmle  26157  idomrootle  26212  ig1pdvds  26219  coe11  26292  dgrmulc  26311  dvply1  26325  aaliou2  26382  efcvx  26493  tanord  26580  logdivlti  26662  logccv  26705  recxpcl  26717  cxplea  26738  cxple2a  26741  ang180  26857  isosctrlem2  26862  cxp2lim  27020  amgm  27034  muval1  27176  dvdssqf  27181  mumullem2  27223  bcmono  27321  lgsneg  27365  lgsmod  27367  lgsdirprm  27375  lgsdir  27376  lgsdi  27378  sltres  27707  nolt02olem  27739  nolt02o  27740  nogt01o  27741  nosupbnd1lem1  27753  nosupbnd1lem4  27756  nosupbnd1lem5  27757  nosupbnd1lem6  27758  noinfbnd1lem1  27768  noinfbnd1lem4  27771  noinfbnd1lem6  27773  noinfbnd2  27776  noetainflem3  27784  sltlpss  27945  cofsslt  27952  coinitsslt  27953  cofcutrtime  27961  addsass  28038  addsdi  28181  mulsass  28192  sltmul2  28197  norecdiv  28216  brbtwn2  28920  colinearalglem1  28921  colinearalg  28925  axcgrtr  28930  axcontlem2  28980  upgrewlkle2  29624  wlksoneq1eq2  29682  crctcshwlkn0lem5  29834  wspthsnwspthsnon  29936  lppthon  30170  upgriseupth  30226  4cyclusnfrgr  30311  numclwwlk1lem2foa  30373  numclwwlk5  30407  nvmul0or  30669  shless  31378  shlej1  31379  pjspansn  31596  kbmul  31974  homco2  31996  kbass2  32136  fnpreimac  32681  padct  32731  eliccelico  32779  elicoelioo  32780  iocinioc2  32781  difioo  32784  nexple  32833  swrdrn2  32939  swrdrn3  32940  xrge0npcan  33025  isarchi2  33192  archiabl  33205  pidlnz  33404  lindssn  33406  ssmxidl  33502  mdetlap1  33825  zarclsiin  33870  pstmfval  33895  fmcncfil  33930  zrhnm  33968  qqhnm  33991  volfiniune  34231  omsmeas  34325  eulerpartlemb  34370  probinc  34423  cndprob01  34437  signswmnd  34572  cvmsss2  35279  funsseq  35768  cgrtriv  36003  5segofs  36007  btwntriv2  36013  btwnxfr  36057  segcon2  36106  brsegle2  36110  seglelin  36117  outsideofeu  36132  weiunpo  36466  weiunfr  36468  weiunse  36469  lindsenlbs  37622  mblfinlem2  37665  blbnd  37794  rrndstprj2  37838  zerdivemp1x  37954  lsmsat  39009  lsatfixedN  39010  lssat  39017  lkrlsp  39103  lshpkrlem4  39114  cvrcon3b  39278  leat3  39296  atlen0  39311  atnle  39318  atlatmstc  39320  atlatle  39321  cvlcvr1  39340  cvlsupr2  39344  hlsupr2  39389  hlrelat2  39405  cvrexchlem  39421  cvratlem  39423  lnnat  39429  atexchcvrN  39442  1cvratlt  39476  1cvrjat  39477  3atlem3  39487  3atlem7  39491  llni2  39514  atcvrlln2  39521  llnexatN  39523  llncmp  39524  2llnmat  39526  2at0mat0  39527  2atnelpln  39546  llncvrlpln2  39559  2lplnmN  39561  2llnmj  39562  lplncmp  39564  lplnexatN  39565  2llnjaN  39568  lvoli3  39579  islvol2aN  39594  4atlem3a  39599  4atlem4a  39601  4atlem4b  39602  4atlem11  39611  4atlem12  39614  lplncvrlvol2  39617  lvolcmp  39619  2lplnmj  39624  islinei  39742  linepmap  39777  lneq2at  39780  2llnma3r  39790  elpaddn0  39802  elpaddatriN  39805  elpaddat  39806  paddcom  39815  paddss1  39819  paddss2  39820  paddasslem6  39827  paddasslem7  39828  paddasslem10  39831  paddasslem15  39836  pmodlem2  39849  pmodl42N  39853  pmapjoin  39854  atmod1i1m  39860  llnmod1i2  39862  llnexchb2lem  39870  polcon2bN  39922  pclfinclN  39952  poml4N  39955  poml6N  39957  osumcllem11N  39968  osumclN  39969  pmapojoinN  39970  pexmidlem2N  39973  pexmidlem3N  39974  pexmidlem4N  39975  pexmidlem6N  39977  pexmidlem7N  39978  pl42lem2N  39982  pl42lem3N  39983  pl42lem4N  39984  pl42N  39985  lhpexle3lem  40013  lhpmcvr3  40027  lhp2at0nle  40037  lhprelat3N  40042  lauteq  40097  lautco  40099  ltrncoidN  40130  ltrneq2  40150  ltrnnidn  40176  ltrnideq  40177  trlnle  40188  cdlemc  40199  cdlemd4  40203  cdlemd5  40204  cdlemd9  40208  cdlemd  40209  ltrneq3  40210  cdlemefrs29pre00  40397  cdlemefrs29cpre1  40400  cdlemefrs29clN  40401  cdlemefrs32fva  40402  cdlemefr29exN  40404  cdlemefr27cl  40405  cdlemefs27cl  40415  cdlemefs32sn1aw  40416  cdleme32fva  40439  cdleme32d  40446  cdleme32f  40448  cdleme32le  40449  cdleme40n  40470  cdleme41snaw  40478  cdleme17d3  40498  cdleme48fvg  40502  cdlemeg46fvcl  40508  cdlemeg46fgN  40536  cdleme48fgv  40540  ltrniotavalbN  40586  cdlemb3  40608  cdlemg15  40658  cdlemg17dN  40665  trlco  40729  cdlemg44b  40734  ltrncom  40740  trljco  40742  tendococl  40774  tendoplcl  40783  tendoplcom  40784  tendotr  40832  cdlemk36  40915  cdlemk35s-id  40940  cdlemk39s-id  40942  cdlemk19x  40945  cdlemk53b  40958  cdlemk55  40963  cdlemk35u  40966  cdlemk55u  40968  cdlemk39u  40970  cdlemk19u  40972  cdlemk56  40973  tendoex  40977  cdleml5N  40982  dihord2pre  41227  dihord6apre  41258  dihord5b  41261  dihord5apre  41264  dihord  41266  dihmeetlem1N  41292  dihmeetlem2N  41301  dihglbcpreN  41302  dihmeetbN  41305  dihmeetlem4preN  41308  dihmeetlem5  41310  dihmeetlem6  41311  dihmeetlem7N  41312  dihmeetlem10N  41318  dihmeetlem11N  41319  dihmeetlem12N  41320  dihmeetlem13N  41321  dihmeetlem15N  41323  dihmeetlem17N  41325  dihmeetlem18N  41326  dihmeetlem19N  41327  dihmeetALTN  41329  dih1dimatlem0  41330  dihlspsnssN  41334  dvh3dim2  41450  sticksstones1  42147  sticksstones2  42148  sticksstones12  42159  aks6d1c6isolem1  42175  dvdsexpnn  42368  resubcan2  42418  mzpsubst  42759  diophrw  42770  eldioph2lem1  42771  rencldnfi  42832  pellexlem2  42841  pellqrexplicit  42888  infmrgelbi  42889  rmxycomplete  42929  congadd  42978  acongeq  42995  jm2.19  43005  jm2.22  43007  jm2.20nn  43009  jm2.25lem1  43010  jm2.27  43020  jm3.1  43032  lmhmlnmsplit  43099  pwssplit4  43101  hbtlem2  43136  dgraa0p  43161  proot1hash  43207  iocunico  43223  cantnf2  43338  dflim5  43342  omcl2  43346  tfsconcatrn  43355  nadd2rabex  43399  relexpxpmin  43730  brtrclfv2  43740  ntrclsk3  44083  grur1cld  44251  ismnu  44280  suprnmpt  45179  wessf1ornlem  45190  choicefi  45205  supxrgere  45344  supxrgelem  45348  supxrge  45349  infleinflem2  45382  snunioo1  45525  iccintsng  45536  fmul01  45595  lptre2pt  45655  0ellimcdiv  45664  fnlimfvre  45689  limsupmnfuzlem  45741  climisp  45761  limsupgtlem  45792  ibliccsinexp  45966  iblioosinexp  45968  volioc  45987  iblspltprt  45988  stoweidlem20  46035  stoweidlem22  46037  stoweidlem34  46049  stoweidlem44  46059  stoweidlem60  46075  wallispilem3  46082  fourierdlem42  46164  fourierdlem51  46172  fourierdlem54  46175  fourierdlem87  46208  fourierdlem97  46218  ioorrnopnlem  46319  sge0seq  46461  hoicvr  46563  fsupdm  46857  finfdm  46861  3f1oss1  47087  funfocofob  47090  imasetpreimafvbijlemfv  47389  uhgrimisgrgric  47899  uhgrimgrlim  47954  fprmappr  48261  lincresunit3lem3  48391  lindssnlvec  48403  rrx2linesl  48664  line2  48673  itsclc0lem3  48679  itsclc0yqsollem1  48683  itscnhlc0xyqsol  48686  itschlc0xyqsol1  48687  itsclc0  48692  itscnhlinecirc02plem2  48704  itscnhlinecirc02plem3  48705