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  2917  sotri2  5026  sotri3  5027  feq123  5357  resasplitss  5395  sefvex  5536  ftpg  5700  fsnunf  5716  fnfvima  5751  cocan1  5787  cocan2  5788  f1oiso2  5827  riotass  5857  moriotass  5858  ovmpox  6002  ovmpoga  6003  caovimo  6067  ofrval  6092  dfsmo2  6287  tfr1onlembfn  6344  tfrcllembfn  6357  freccllem  6402  frecfcllem  6404  frecsuclem  6406  frecrdg  6408  nnsucsssuc  6492  f1oen2g  6754  f1dom2g  6755  xpdom3m  6833  mapxpen  6847  diffifi  6893  unfidisj  6920  undifdc  6922  ssfidc  6933  sbthlemi9  6963  ctssdc  7111  endjudisj  7208  djuassen  7215  xpdjuen  7216  mulcanenq  7383  ltanqg  7398  addnnnq0  7447  nnanq0  7456  prltlu  7485  distrprg  7586  ltexprlemm  7598  recexprlem1ssl  7631  recexprlem1ssu  7632  addsrpr  7743  mulsrpr  7744  mulasssrg  7756  recexgt0sr  7771  ltpsrprg  7801  axmulass  7871  axpre-ltadd  7884  ltxrlt  8022  subadd2  8160  addsubass  8166  nppcan  8178  nppcan3  8180  subcan2  8181  subsub2  8184  subsub4  8189  pnpcan  8195  pnncan  8197  subcan  8211  subdi  8341  ltadd1  8385  leadd1  8386  leadd2  8387  ltsubadd  8388  ltsubadd2  8389  lesubadd  8390  lesubadd2  8391  ltaddsub  8392  leaddsub  8394  lesub1  8412  lesub2  8413  ltsub1  8414  ltsub2  8415  ltaddsublt  8527  gt0add  8529  reapadd1  8552  remulext1  8555  remulext2  8556  apadd2  8565  mulext2  8569  mulap0r  8571  leltap  8581  ltap  8589  apsub1  8598  divap0b  8639  divmulasscomap  8652  divcanap5  8670  dmdcanap  8678  redivclap  8687  div2negap  8691  lt2msq1  8841  ltdiv2  8843  nndivtr  8960  difgtsumgt  9321  gtndiv  9347  eluzsub  9556  nn01to3  9616  qdivcl  9642  irrmul  9646  rpgecl  9681  divge1  9722  xaddass  9868  xltadd1  9875  ubioog  9913  ubioc1  9928  lbico1  9929  iccleub  9930  lbicc2  9983  ubicc2  9984  icoshftf1o  9990  fzen  10042  elfz1b  10089  uznfz  10102  elfzo0  10181  elfzo0z  10183  ubmelfzo  10199  fzonn0p1p1  10212  ubmelm1fzo  10225  qbtwnre  10256  flqwordi  10287  flltdivnn0lt  10303  ceiqle  10312  modqval  10323  modqvalr  10324  modqcl  10325  flqpmodeq  10326  modq0  10328  mulqmod0  10329  negqmod0  10330  modqge0  10331  modqlt  10332  modqdiffl  10334  modqdifz  10335  modqmulnn  10341  modqvalp1  10342  modqabs2  10357  modqmuladdnn0  10367  qnegmod  10368  addmodid  10371  modqeqmodmin  10393  modfzo0difsn  10394  addmodlteq  10397  frec2uzf1od  10405  expnegap0  10527  expgt1  10557  exprecap  10560  expaddzaplem  10562  expaddzap  10563  expmulzap  10565  mulbinom2  10636  expnbnd  10643  fihashss  10795  fimaxq  10806  seq3coll  10821  shftfibg  10828  redivap  10882  imdivap  10889  cjdivap  10917  maxleast  11221  lemininf  11241  ltmininf  11242  bdtrilem  11246  bdtri  11247  xrmaxaddlem  11267  xrmaxadd  11268  xrmineqinf  11276  xrltmininf  11277  xrminltinf  11279  xrminadd  11282  climuni  11300  reccn2ap  11320  isumz  11396  fsumsplitsnun  11426  geoisum1c  11527  prodfap0  11552  prod1dc  11593  fprodabs  11623  cos12dec  11774  summodnegmod  11828  dvdsmultr2  11839  mulmoddvds  11868  divalglemeuneg  11927  zsupssdc  11954  gcdaddm  11984  gcdass  12015  mulgcd  12016  gcddiv  12019  nnminle  12035  lcmass  12084  mulgcddvds  12093  qredeq  12095  congr  12099  divgcdcoprmex  12101  cncongr1  12102  cncongr2  12103  prmexpb  12150  rpexp  12152  pythagtriplem1  12264  pythagtriplem6  12269  pythagtriplem7  12270  pythagtriplem12  12274  pythagtriplem13  12275  pythagtriplem15  12277  pythagtriplem19  12281  pcdiv  12301  dvdsprmpweqle  12335  sumhashdc  12344  pcbc  12348  unennn  12397  nninfdc  12453  fvsetsid  12495  ressressg  12533  rngmulrg  12595  imasaddvallemg  12735  qusaddvallemg  12751  mgmsscl  12779  plusfvalg  12781  ress0g  12843  grpasscan2  12933  grpidrcan  12934  grpidlcan  12935  grpinvadd  12947  grppncan  12960  dfgrp3me  12969  grpsubpropd2  12974  mhmmnd  12979  mulgnnsubcl  12994  mulgnn0subcl  12995  mulgsubcl  12996  mulgaddcomlem  13004  mulgaddcom  13005  mulgpropdg  13023  subgcl  13042  subgsubcl  13043  subgsub  13044  subgmulg  13046  nsgconj  13064  ablinvadd  13111  ablpncan2  13117  srgcl  13151  ringcl  13194  crngcom  13195  ringidss  13210  ringcom  13212  mulgass2  13233  opprringbg  13248  unitmulcl  13280  unitmulclb  13281  dvrcl  13302  unitdvcl  13303  dvrcan1  13307  dvrcan3  13308  subrgmcl  13352  subrgdv  13357  islmod  13379  scafvalg  13395  basgen  13550  2basgeng  13552  ntrss  13589  neiss  13620  opnneiss  13628  restco  13644  restabs  13645  cnprcl2k  13676  cnpf2  13677  lmconst  13686  cnpnei  13689  cnptoprest  13709  cnmpt2t  13763  psmetsym  13799  psmetge0  13801  xmetge0  13835  xmetsym  13838  blvalps  13858  blval  13859  ssblps  13895  ssbl  13896  blpnfctr  13909  xmssym  13939  bdxmet  13971  metcnp3  13981  dvfvalap  14120  dvid  14132  dvcnp2cntop  14133  ptolemy  14215  rpcxpadd  14296  rpcxpsub  14299  rpmulcxp  14300  cxpmul  14303  rpcxple2  14308  rpcxplt2  14309  cxpcom  14327  rplogbval  14333  rplogbcl  14334  rplogbchbase  14338  rplogbreexp  14341  relogbexpap  14346  logbleb  14349  logblt  14350  rplogbcxp  14351  rpcxplogb  14352  relogbcxpbap  14353  lgslem1  14371  lgsfvalg  14376  lgsval4  14391  lgsneg  14395  lgsne0  14409  lgsdinn0  14419