Theorem simpl3 1059

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpl3	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simpl3

Step	Hyp	Ref	Expression
1		simp3 1056	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	adantr 480	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simpll3  1095  simprl3  1101  simp1l3  1149  simp2l3  1155  simp3l3  1161  3anandirs  1427  f1prex  6439  fcofo  6443  soisores  6477  weniso  6504  knatar  6507  ofmpteq  6814  smorndom  7352  nnmord  7599  nnmword  7600  difsnen  7927  mapunen  8014  ac6sfi  8089  fipreima  8155  wemaplem2  8335  wemapso2lem  8340  en2eqpr  8713  indcardi  8747  acndom  8757  fodomfi2  8766  infmap2  8923  cflim2  8968  coftr  8978  infpssrlem4  9011  fin23lem11  9022  fincssdom  9028  isf32lem9  9066  fin1a2lem9  9113  gchpwdom  9371  gruima  9503  prpssnq  9691  distrlem4pr  9727  dedekind  10079  addcan  10099  addcan2  10100  divmulass  10587  supmul1  10869  uzsupss  11656  xaddass  11951  xleadd1a  11955  xlesubadd  11965  xmulasslem3  11988  xmulass  11989  xadddilem  11996  xadddi  11997  ixxun  12062  icoshftf1o  12166  snunioc  12171  difelfzle  12321  fzo1fzo0n0  12386  ssfzoulel  12428  modmuladd  12574  modifeq2int  12594  modaddmulmod  12599  modsubdir  12601  ltexp2a  12774  leexp2  12777  ltexp2r  12779  exple1  12782  expnlbnd2  12857  mulsubdivbinom2  12908  hashtpg  13121  ccatass  13224  ccatopth  13322  swrdccatin12lem2a  13336  swrdccat3  13343  cshinj  13408  s2f1o  13511  limsupgre  14060  addcn2  14172  mulcn2  14174  binomrisefac  14612  bpolydif  14625  modmulconst  14851  dvdsmod  14888  sadass  15031  gcdass  15102  rplpwr  15114  rppwr  15115  rpmulgcd2  15208  rpdvds  15212  rpexp  15270  prmdiveq  15329  hashgcdlem  15331  coprimeprodsq  15351  coprimeprodsq2  15352  pythagtriplem3  15361  pcdvdsb  15411  pcgcd1  15419  dvdsprmpweq  15426  pcbc  15442  0ram  15562  ramz2  15566  ramub1lem1  15568  setsstruct  15727  mremre  16087  mrieqv2d  16122  lubun  16946  isnsgrp  17111  issubmnd  17141  gsumccat  17201  frmdss2  17223  sgrp2rid2ex  17237  mulgnn0p1  17375  mulgnnsubcl  17376  mulgneg  17383  mulgdirlem  17395  nmzsubg  17458  ghmmulg  17495  pmtrfv  17695  pmtrmvd  17699  pmtrfb  17708  odmodnn0  17782  oddvdsnn0  17786  odnncl  17787  odmod  17788  oddvds  17789  odeq  17792  odmulgid  17794  odmulg  17796  odmulgeq  17797  odbezout  17798  odf1o1  17810  odf1o2  17811  odngen  17815  odcau  17842  pgpssslw  17852  fislw  17863  lsmless1x  17882  lsmless2x  17883  lsmsubm  17891  lsmmod  17911  lsmmod2  17912  efgsfo  17975  cntzcmn  18068  odadd1  18074  odadd2  18075  odadd  18076  lsmcomx  18082  prdscmnd  18087  gsumconst  18157  ring1eq0  18413  cntzsubr  18635  isabvd  18643  lspss  18805  0lmhm  18861  reslmhm2  18874  pwssplit0  18879  pwssplit1  18880  lbspss  18903  lspfixed  18949  lsmcv  18962  lspsnat  18966  issubassa  19145  aspss  19153  coe1subfv  19457  coe1tm  19464  xrsdsreclblem  19611  obselocv  19891  frlmsplit2  19931  frlmsslss2  19933  frlmup4  19959  lindff1  19978  lsslindf  19988  lsslinds  19989  islindf4  19996  mpt2matmul  20071  mamutpos  20083  submaval  20206  mdetdiag  20224  mdetunilem1  20237  mdetunilem3  20239  mdetunilem9  20245  mdetmul  20248  maducoeval2  20265  madurid  20269  minmar1val  20273  cramer  20316  cpmatel2  20337  m2cpm  20365  decpmatmul  20396  pmatcollpw1lem2  20399  pmatcollpw1  20400  pmatcollpw2lem  20401  pm2mpcl  20421  mply1topmatcl  20429  mp2pm2mplem2  20431  mp2pm2mplem4  20433  pm2mpghmlem2  20436  pm2mpghmlem1  20437  cayhamlem2  20508  neiint  20718  topssnei  20738  cnrest2  20900  cnprest2  20904  cnt0  20960  cnt1  20964  cnhaus  20968  cncmp  21005  fiuncmp  21017  sscmp  21018  hauscmp  21020  cnconn  21035  uncon  21042  comppfsc  21145  kgen2ss  21168  ptpjopn  21225  ptrescn  21252  qtopss  21328  kqfvima  21343  r0cld  21351  cmphaushmeo  21413  fbssint  21452  fbasrn  21498  filuni  21499  ufilmax  21521  fin1aufil  21546  fmf  21559  fmss  21560  rnelfmlem  21566  rnelfm  21567  fmufil  21573  fmco  21575  flimss2  21586  flimss1  21587  flimrest  21597  cnpflf2  21614  cnpflf  21615  flfcnp  21618  lmflf  21619  supnfcls  21634  fclsss1  21636  fclsss2  21637  cnpfcfi  21654  subgntr  21720  opnsubg  21721  cldsubg  21724  ustuqtop1  21855  ucncn  21899  bldisj  22013  blgt0  22014  bl2in  22015  blss2ps  22018  blss2  22019  xbln0  22029  blssps  22039  blss  22040  lpbl  22118  blcld  22120  blcls  22121  stdbdmopn  22133  metcnp2  22157  txmetcnp  22162  blval2  22177  restmetu  22185  nmoix  22343  nmoi2  22344  nmoeq0  22350  nmotri  22353  metdsge  22460  metds0  22461  metdseq0  22465  icoopnst  22546  iccpnfhmeo  22552  xrhmeo  22553  nmhmcn  22728  cphsqrtcl2  22794  cphsqrtcl3  22795  fmcfil  22878  bcthlem5  22933  cmetcusp1  22957  pjth  23018  ovolunnul  23075  volun  23120  voliunlem2  23126  itg2const  23313  iblconst  23390  itgconst  23391  limcvallem  23441  dvcnp2  23489  dvcn  23490  deg1mul3le  23680  deg1tmle  23681  ig1pdvds  23740  coe11  23813  dgrmulc  23831  dvply1  23843  aaliou2  23899  efcvx  24007  tanord  24088  logdivlti  24170  logccv  24209  recxpcl  24221  cxplea  24242  cxple2a  24245  ang180  24344  isosctrlem2  24349  cxp2lim  24503  amgm  24517  muval1  24659  dvdssqf  24664  mumullem2  24706  bcmono  24802  lgsneg  24846  lgsmod  24848  lgsdirprm  24856  lgsdir  24857  lgsdi  24859  brbtwn2  25585  colinearalglem1  25586  colinearalg  25590  axcgrtr  25595  axcontlem2  25645  cyclispthon  26161  clwwlknprop  26300  clwwlknimp  26304  vdgrfif  26426  4cyclusnfrgra  26546  nvmul0or  26889  shless  27602  shlej1  27603  pjspansn  27820  kbmul  28198  homco2  28220  kbass2  28360  padct  28885  eliccelico  28929  elicoelioo  28930  iocinioc2  28931  difioo  28934  xrge0npcan  29025  isarchi2  29070  archiabl  29083  mdetlap1  29220  pstmfval  29267  fmcncfil  29305  zrhnm  29341  qqhnm  29362  nexple  29399  volfiniune  29620  omsmeas  29712  eulerpartlemb  29757  probinc  29810  cndprob01  29824  signswmnd  29960  cvmsss2  30510  dvdspw  30889  funsseq  30912  sltres  31061  cgrtriv  31279  5segofs  31283  btwntriv2  31289  btwnxfr  31333  segcon2  31382  brsegle2  31386  seglelin  31393  outsideofeu  31408  lindsenlbs  32574  mblfinlem2  32617  blbnd  32756  rrndstprj2  32800  zerdivemp1x  32916  lsmsat  33313  lsatfixedN  33314  lssat  33321  lkrlsp  33407  lshpkrlem4  33418  cvrcon3b  33582  leat3  33600  atlen0  33615  atnle  33622  atlatmstc  33624  atlatle  33625  cvlcvr1  33644  cvlsupr2  33648  hlsupr2  33691  hlrelat2  33707  cvrexchlem  33723  cvratlem  33725  lnnat  33731  atexchcvrN  33744  1cvratlt  33778  1cvrjat  33779  3atlem3  33789  3atlem7  33793  llni2  33816  atcvrlln2  33823  llnexatN  33825  llncmp  33826  2llnmat  33828  2at0mat0  33829  2atnelpln  33848  llncvrlpln2  33861  2lplnmN  33863  2llnmj  33864  lplncmp  33866  lplnexatN  33867  2llnjaN  33870  lvoli3  33881  islvol2aN  33896  4atlem3a  33901  4atlem4a  33903  4atlem4b  33904  4atlem11  33913  4atlem12  33916  lplncvrlvol2  33919  lvolcmp  33921  2lplnmj  33926  islinei  34044  linepmap  34079  lneq2at  34082  2llnma3r  34092  elpaddn0  34104  elpaddatriN  34107  elpaddat  34108  paddcom  34117  paddss1  34121  paddss2  34122  paddasslem6  34129  paddasslem7  34130  paddasslem10  34133  paddasslem15  34138  pmodlem2  34151  pmodl42N  34155  pmapjoin  34156  atmod1i1m  34162  llnmod1i2  34164  llnexchb2lem  34172  polcon2bN  34224  pclfinclN  34254  poml4N  34257  poml6N  34259  osumcllem11N  34270  osumclN  34271  pmapojoinN  34272  pexmidlem2N  34275  pexmidlem3N  34276  pexmidlem4N  34277  pexmidlem6N  34279  pexmidlem7N  34280  pl42lem2N  34284  pl42lem3N  34285  pl42lem4N  34286  pl42N  34287  lhpexle3lem  34315  lhpmcvr3  34329  lhp2at0nle  34339  lhprelat3N  34344  lauteq  34399  lautco  34401  ltrncoidN  34432  ltrneq2  34452  ltrnnidn  34479  ltrnideq  34480  trlnle  34491  cdlemc  34502  cdlemd4  34506  cdlemd5  34507  cdlemd9  34511  cdlemd  34512  ltrneq3  34513  cdlemefrs29pre00  34701  cdlemefrs29cpre1  34704  cdlemefrs29clN  34705  cdlemefrs32fva  34706  cdlemefr29exN  34708  cdlemefr27cl  34709  cdlemefs27cl  34719  cdlemefs32sn1aw  34720  cdleme32fva  34743  cdleme32d  34750  cdleme32f  34752  cdleme32le  34753  cdleme40n  34774  cdleme41snaw  34782  cdleme17d3  34802  cdleme48fvg  34806  cdlemeg46fvcl  34812  cdlemeg46fgN  34840  cdleme48fgv  34844  ltrniotavalbN  34890  cdlemb3  34912  cdlemg15  34962  cdlemg17dN  34969  trlco  35033  cdlemg44b  35038  ltrncom  35044  trljco  35046  tendococl  35078  tendoplcl  35087  tendoplcom  35088  tendotr  35136  cdlemk36  35219  cdlemk35s-id  35244  cdlemk39s-id  35246  cdlemk19x  35249  cdlemk53b  35262  cdlemk55  35267  cdlemk35u  35270  cdlemk55u  35272  cdlemk39u  35274  cdlemk19u  35276  cdlemk56  35277  tendoex  35281  cdleml5N  35286  dihord2pre  35532  dihord6apre  35563  dihord5b  35566  dihord5apre  35569  dihord  35571  dihmeetlem1N  35597  dihmeetlem2N  35606  dihglbcpreN  35607  dihmeetbN  35610  dihmeetlem4preN  35613  dihmeetlem5  35615  dihmeetlem6  35616  dihmeetlem7N  35617  dihmeetlem10N  35623  dihmeetlem11N  35624  dihmeetlem12N  35625  dihmeetlem13N  35626  dihmeetlem15N  35628  dihmeetlem17N  35630  dihmeetlem18N  35631  dihmeetlem19N  35632  dihmeetALTN  35634  dih1dimatlem0  35635  dihlspsnssN  35639  dvh3dim2  35755  mzpsubst  36329  diophrw  36340  eldioph2lem1  36341  rencldnfi  36403  pellexlem2  36412  pellqrexplicit  36459  infmrgelbi  36460  rmxycomplete  36500  congadd  36551  acongeq  36568  jm2.19  36578  jm2.22  36580  jm2.20nn  36582  jm2.25lem1  36583  jm2.27  36593  jm3.1  36605  lmhmlnmsplit  36675  pwssplit4  36677  hbtlem2  36713  dgraa0p  36738  idomrootle  36792  proot1hash  36797  iocunico  36815  relexpxpmin  37028  brtrclfv2  37038  ntrclsk3  37388  suprnmpt  38350  wessf1ornlem  38366  choicefi  38387  supxrgere  38490  supxrgelem  38494  supxrge  38495  infleinflem2  38528  snunioo1  38585  iccintsng  38596  fmul01  38647  lptre2pt  38707  0ellimcdiv  38716  fnlimfvre  38741  ibliccsinexp  38842  iblioosinexp  38844  volioc  38864  iblspltprt  38865  stoweidlem20  38913  stoweidlem22  38915  stoweidlem34  38927  stoweidlem44  38937  stoweidlem60  38953  wallispilem3  38960  fourierdlem42  39042  fourierdlem51  39050  fourierdlem54  39053  fourierdlem87  39086  fourierdlem97  39096  ioorrnopnlem  39200  sge0seq  39339  hoicvr  39438  ccatpfx  40272  pfxccat3  40289  upgrewlkle2  40808  wlksoneq1eq2  40872  usgr2trlncl  40966  crctcsh1wlkn0lem5  41017  1wlkiswwlks1  41064  wspthsnwspthsnon  41122  lppthon  41318  upgriseupth  41375  4cyclusnfrgr  41462  av-numclwwlk5  41542  lincresunit3lem3  42057  lindssnlvec  42069