Theorem simp3 1002

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 999	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	simprd 114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  simpl3  1005  simpr3  1008  simp3i  1011  simp3d  1014  simp13  1032  simp23  1035  simp33  1038  3anibar  1168  3ianorr  1322  intn3an3d  1370  stoic4a  1452  stoic4b  1453  mob2  2954  sotri2  5085  sotri3  5086  feq123  5423  resasplitss  5462  sefvex  5604  ftpg  5775  fsnunf  5791  fnfvima  5826  cocan1  5863  cocan2  5864  f1oiso2  5903  riotass  5934  moriotass  5935  ovmpox  6081  ovmpoga  6082  fvmpopr2d  6089  caovimo  6147  ofrval  6176  dfsmo2  6380  tfr1onlembfn  6437  tfrcllembfn  6450  freccllem  6495  frecfcllem  6497  frecsuclem  6499  frecrdg  6501  nnsucsssuc  6585  f1oen2g  6853  f1dom2g  6854  xpdom3m  6936  mapxpen  6952  diffifi  6998  unfidisj  7026  undifdc  7028  ssfidc  7041  sbthlemi9  7074  ctssdc  7222  endjudisj  7329  djuassen  7336  xpdjuen  7337  mulcanenq  7505  ltanqg  7520  addnnnq0  7569  nnanq0  7578  prltlu  7607  distrprg  7708  ltexprlemm  7720  recexprlem1ssl  7753  recexprlem1ssu  7754  addsrpr  7865  mulsrpr  7866  mulasssrg  7878  recexgt0sr  7893  ltpsrprg  7923  axmulass  7993  axpre-ltadd  8006  ltxrlt  8145  subadd2  8283  addsubass  8289  nppcan  8301  nppcan3  8303  subcan2  8304  subsub2  8307  subsub4  8312  pnpcan  8318  pnncan  8320  subcan  8334  subdi  8464  ltadd1  8509  leadd1  8510  leadd2  8511  ltsubadd  8512  ltsubadd2  8513  lesubadd  8514  lesubadd2  8515  ltaddsub  8516  leaddsub  8518  lesub1  8536  lesub2  8537  ltsub1  8538  ltsub2  8539  ltaddsublt  8651  gt0add  8653  reapadd1  8676  remulext1  8679  remulext2  8680  apadd2  8689  mulext2  8693  mulap0r  8695  leltap  8705  ltap  8713  apsub1  8722  divap0b  8763  divmulasscomap  8776  divcanap5  8794  dmdcanap  8802  redivclap  8811  div2negap  8815  lt2msq1  8965  ltdiv2  8967  ofnegsub  9042  nndivtr  9085  difgtsumgt  9449  gtndiv  9475  eluzsub  9685  nn01to3  9745  qdivcl  9771  irrmul  9775  rpgecl  9811  divge1  9852  xaddass  9998  xltadd1  10005  ubioog  10043  ubioc1  10058  lbico1  10059  iccleub  10060  lbicc2  10113  ubicc2  10114  icoshftf1o  10120  fzen  10172  elfz1b  10219  uznfz  10232  elfzo0  10313  elfzo0z  10315  ubmelfzo  10336  fzonn0p1p1  10349  ubmelm1fzo  10362  zsupssdc  10388  qbtwnre  10406  flqwordi  10438  flltdivnn0lt  10454  ceiqle  10465  modqval  10476  modqvalr  10477  modqcl  10478  flqpmodeq  10479  modq0  10481  mulqmod0  10482  negqmod0  10483  modqge0  10484  modqlt  10485  modqdiffl  10487  modqdifz  10488  modqmulnn  10494  modqvalp1  10495  modqabs2  10510  modqmuladdnn0  10520  qnegmod  10521  addmodid  10524  modqeqmodmin  10546  modfzo0difsn  10547  addmodlteq  10550  frec2uzf1od  10558  expnegap0  10699  expgt1  10729  exprecap  10732  expaddzaplem  10734  expaddzap  10735  expmulzap  10737  mulbinom2  10808  expnbnd  10815  fihashss  10968  fimaxq  10979  seq3coll  10994  swrdval  11109  swrdnd  11120  swrdlen2  11123  pfxn0  11147  shftfibg  11175  redivap  11229  imdivap  11236  cjdivap  11264  maxleast  11568  lemininf  11589  ltmininf  11590  bdtrilem  11594  bdtri  11595  xrmaxaddlem  11615  xrmaxadd  11616  xrmineqinf  11624  xrltmininf  11625  xrminltinf  11627  xrminadd  11630  climuni  11648  reccn2ap  11668  isumz  11744  fsumsplitsnun  11774  geoisum1c  11875  prodfap0  11900  prod1dc  11941  fprodabs  11971  cos12dec  12123  summodnegmod  12177  dvdsmultr2  12188  mulmoddvds  12218  divalglemeuneg  12278  gcdaddm  12349  gcdass  12380  mulgcd  12381  gcddiv  12384  nnminle  12400  lcmass  12451  mulgcddvds  12460  qredeq  12462  congr  12466  divgcdcoprmex  12468  cncongr1  12469  cncongr2  12470  prmexpb  12517  rpexp  12519  pythagtriplem1  12632  pythagtriplem6  12637  pythagtriplem7  12638  pythagtriplem12  12642  pythagtriplem13  12643  pythagtriplem15  12645  pythagtriplem19  12649  pcdiv  12669  dvdsprmpweqle  12704  sumhashdc  12714  pcbc  12718  4sqlem12  12769  4sqlem18  12775  unennn  12812  nninfdc  12868  fvsetsid  12910  ressressg  12951  rngmulrg  13014  imasaddvallemg  13191  qusaddvallemg  13209  mgmsscl  13237  plusfvalg  13239  ress0g  13319  imasmnd2  13328  imasmnd  13329  gsumfzz  13371  grpasscan2  13440  grpidrcan  13441  grpidlcan  13442  grpinvadd  13454  grppncan  13467  dfgrp3me  13476  grpsubpropd2  13481  pwsinvg  13488  imasgrp2  13490  imasgrp  13491  mhmmnd  13496  mulgnnsubcl  13514  mulgnn0subcl  13515  mulgsubcl  13516  mulgaddcomlem  13525  mulgaddcom  13526  mulgpropdg  13544  submmulg  13546  subgcl  13564  subgsubcl  13565  subgsub  13566  subgmulg  13568  nsgconj  13586  ghmsub  13631  ghmnsgima  13648  ghmeqker  13651  f1ghm0to0  13652  ablinvadd  13690  ablpncan2  13696  subgabl  13712  rngcl  13750  imasrng  13762  srgcl  13776  ringcl  13819  crngcom  13820  ringidss  13835  ringcom  13837  mulgass2  13864  imasring  13870  opprringbg  13886  unitmulcl  13919  unitmulclb  13920  dvrcl  13941  unitdvcl  13942  dvrcan1  13946  dvrcan3  13947  rhmmul  13970  subrngmcl  14015  subrgmcl  14039  subrgdv  14044  domneq0  14078  islmod  14097  scafvalg  14113  lmodcom  14139  lmodprop2d  14154  rmodislmodlem  14156  rmodislmod  14157  lsselg  14167  lssvnegcl  14182  lspss  14205  lspun  14208  lspsnvsi  14224  lsslsp  14235  sralmod  14256  lidlnegcl  14291  rspssp  14300  rnglidlrng  14304  qus2idrng  14331  zndvds  14455  basgen  14596  2basgeng  14598  ntrss  14635  neiss  14666  opnneiss  14674  restco  14690  restabs  14691  cnprcl2k  14722  cnpf2  14723  lmconst  14732  cnpnei  14735  cnptoprest  14755  cnmpt2t  14809  psmetsym  14845  psmetge0  14847  xmetge0  14881  xmetsym  14884  blvalps  14904  blval  14905  ssblps  14941  ssbl  14942  blpnfctr  14955  xmssym  14985  bdxmet  15017  metcnp3  15027  dvfvalap  15197  dvid  15211  dvidre  15213  dvcnp2cntop  15215  elplyr  15256  ply1term  15259  plypow  15260  ptolemy  15340  rpcxpadd  15421  rpcxpsub  15424  rpmulcxp  15425  cxpmul  15428  rpcxple2  15434  rpcxplt2  15435  cxpcom  15454  rplogbval  15461  rplogbcl  15462  rplogbchbase  15466  rplogbreexp  15469  relogbexpap  15474  logbleb  15477  logblt  15478  rplogbcxp  15479  rpcxplogb  15480  relogbcxpbap  15481  sgmppw  15508  lgslem1  15521  lgsfvalg  15526  lgsval4  15541  lgsneg  15545  lgsne0  15559  lgsdinn0  15569  lgsquad  15601  funvtxvalg  15679  funiedgvalg  15680