Theorem simp3 999

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Proof of Theorem simp3

Step	Hyp	Ref	Expression
1		3simpc 996	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	simprd 114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  simpl3  1002  simpr3  1005  simp3i  1008  simp3d  1011  simp13  1029  simp23  1032  simp33  1035  3anibar  1165  3ianorr  1309  stoic4a  1432  stoic4b  1433  mob2  2919  sotri2  5028  sotri3  5029  feq123  5359  resasplitss  5397  sefvex  5538  ftpg  5703  fsnunf  5719  fnfvima  5754  cocan1  5791  cocan2  5792  f1oiso2  5831  riotass  5861  moriotass  5862  ovmpox  6006  ovmpoga  6007  caovimo  6071  ofrval  6096  dfsmo2  6291  tfr1onlembfn  6348  tfrcllembfn  6361  freccllem  6406  frecfcllem  6408  frecsuclem  6410  frecrdg  6412  nnsucsssuc  6496  f1oen2g  6758  f1dom2g  6759  xpdom3m  6837  mapxpen  6851  diffifi  6897  unfidisj  6924  undifdc  6926  ssfidc  6937  sbthlemi9  6967  ctssdc  7115  endjudisj  7212  djuassen  7219  xpdjuen  7220  mulcanenq  7387  ltanqg  7402  addnnnq0  7451  nnanq0  7460  prltlu  7489  distrprg  7590  ltexprlemm  7602  recexprlem1ssl  7635  recexprlem1ssu  7636  addsrpr  7747  mulsrpr  7748  mulasssrg  7760  recexgt0sr  7775  ltpsrprg  7805  axmulass  7875  axpre-ltadd  7888  ltxrlt  8026  subadd2  8164  addsubass  8170  nppcan  8182  nppcan3  8184  subcan2  8185  subsub2  8188  subsub4  8193  pnpcan  8199  pnncan  8201  subcan  8215  subdi  8345  ltadd1  8389  leadd1  8390  leadd2  8391  ltsubadd  8392  ltsubadd2  8393  lesubadd  8394  lesubadd2  8395  ltaddsub  8396  leaddsub  8398  lesub1  8416  lesub2  8417  ltsub1  8418  ltsub2  8419  ltaddsublt  8531  gt0add  8533  reapadd1  8556  remulext1  8559  remulext2  8560  apadd2  8569  mulext2  8573  mulap0r  8575  leltap  8585  ltap  8593  apsub1  8602  divap0b  8643  divmulasscomap  8656  divcanap5  8674  dmdcanap  8682  redivclap  8691  div2negap  8695  lt2msq1  8845  ltdiv2  8847  nndivtr  8964  difgtsumgt  9325  gtndiv  9351  eluzsub  9560  nn01to3  9620  qdivcl  9646  irrmul  9650  rpgecl  9685  divge1  9726  xaddass  9872  xltadd1  9879  ubioog  9917  ubioc1  9932  lbico1  9933  iccleub  9934  lbicc2  9987  ubicc2  9988  icoshftf1o  9994  fzen  10046  elfz1b  10093  uznfz  10106  elfzo0  10185  elfzo0z  10187  ubmelfzo  10203  fzonn0p1p1  10216  ubmelm1fzo  10229  qbtwnre  10260  flqwordi  10291  flltdivnn0lt  10307  ceiqle  10316  modqval  10327  modqvalr  10328  modqcl  10329  flqpmodeq  10330  modq0  10332  mulqmod0  10333  negqmod0  10334  modqge0  10335  modqlt  10336  modqdiffl  10338  modqdifz  10339  modqmulnn  10345  modqvalp1  10346  modqabs2  10361  modqmuladdnn0  10371  qnegmod  10372  addmodid  10375  modqeqmodmin  10397  modfzo0difsn  10398  addmodlteq  10401  frec2uzf1od  10409  expnegap0  10531  expgt1  10561  exprecap  10564  expaddzaplem  10566  expaddzap  10567  expmulzap  10569  mulbinom2  10640  expnbnd  10647  fihashss  10799  fimaxq  10810  seq3coll  10825  shftfibg  10832  redivap  10886  imdivap  10893  cjdivap  10921  maxleast  11225  lemininf  11245  ltmininf  11246  bdtrilem  11250  bdtri  11251  xrmaxaddlem  11271  xrmaxadd  11272  xrmineqinf  11280  xrltmininf  11281  xrminltinf  11283  xrminadd  11286  climuni  11304  reccn2ap  11324  isumz  11400  fsumsplitsnun  11430  geoisum1c  11531  prodfap0  11556  prod1dc  11597  fprodabs  11627  cos12dec  11778  summodnegmod  11832  dvdsmultr2  11843  mulmoddvds  11872  divalglemeuneg  11931  zsupssdc  11958  gcdaddm  11988  gcdass  12019  mulgcd  12020  gcddiv  12023  nnminle  12039  lcmass  12088  mulgcddvds  12097  qredeq  12099  congr  12103  divgcdcoprmex  12105  cncongr1  12106  cncongr2  12107  prmexpb  12154  rpexp  12156  pythagtriplem1  12268  pythagtriplem6  12273  pythagtriplem7  12274  pythagtriplem12  12278  pythagtriplem13  12279  pythagtriplem15  12281  pythagtriplem19  12285  pcdiv  12305  dvdsprmpweqle  12339  sumhashdc  12348  pcbc  12352  unennn  12401  nninfdc  12457  fvsetsid  12499  ressressg  12537  rngmulrg  12599  imasaddvallemg  12742  qusaddvallemg  12758  mgmsscl  12786  plusfvalg  12788  ress0g  12850  grpasscan2  12940  grpidrcan  12941  grpidlcan  12942  grpinvadd  12954  grppncan  12967  dfgrp3me  12976  grpsubpropd2  12981  mhmmnd  12986  mulgnnsubcl  13001  mulgnn0subcl  13002  mulgsubcl  13003  mulgaddcomlem  13012  mulgaddcom  13013  mulgpropdg  13031  subgcl  13050  subgsubcl  13051  subgsub  13052  subgmulg  13054  nsgconj  13072  ablinvadd  13119  ablpncan2  13125  srgcl  13159  ringcl  13202  crngcom  13203  ringidss  13218  ringcom  13220  mulgass2  13241  opprringbg  13256  unitmulcl  13288  unitmulclb  13289  dvrcl  13310  unitdvcl  13311  dvrcan1  13315  dvrcan3  13316  subrgmcl  13360  subrgdv  13365  islmod  13387  scafvalg  13403  lmodcom  13429  lmodprop2d  13444  rmodislmodlem  13446  rmodislmod  13447  lsselg  13454  lssvnegcl  13469  lspss  13491  lspun  13494  lspsnvsi  13510  lsslsp  13521  sralmod  13542  lidlnegcl  13570  rspssp  13578  basgen  13720  2basgeng  13722  ntrss  13759  neiss  13790  opnneiss  13798  restco  13814  restabs  13815  cnprcl2k  13846  cnpf2  13847  lmconst  13856  cnpnei  13859  cnptoprest  13879  cnmpt2t  13933  psmetsym  13969  psmetge0  13971  xmetge0  14005  xmetsym  14008  blvalps  14028  blval  14029  ssblps  14065  ssbl  14066  blpnfctr  14079  xmssym  14109  bdxmet  14141  metcnp3  14151  dvfvalap  14290  dvid  14302  dvcnp2cntop  14303  ptolemy  14385  rpcxpadd  14466  rpcxpsub  14469  rpmulcxp  14470  cxpmul  14473  rpcxple2  14478  rpcxplt2  14479  cxpcom  14497  rplogbval  14503  rplogbcl  14504  rplogbchbase  14508  rplogbreexp  14511  relogbexpap  14516  logbleb  14519  logblt  14520  rplogbcxp  14521  rpcxplogb  14522  relogbcxpbap  14523  lgslem1  14541  lgsfvalg  14546  lgsval4  14561  lgsneg  14565  lgsne0  14579  lgsdinn0  14589