Theorem simp3 984

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

Syntax hints:   → wi 4   ∧ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  simpl3  987  simpr3  990  simp3i  993  simp3d  996  simp13  1014  simp23  1017  simp33  1020  3anibar  1150  3ianorr  1288  stoic4a  1409  stoic4b  1410  mob2  2868  sotri2  4944  sotri3  4945  feq123  5272  resasplitss  5310  sefvex  5450  ftpg  5612  fsnunf  5628  fnfvima  5660  cocan1  5696  cocan2  5697  f1oiso2  5736  riotass  5765  moriotass  5766  ovmpox  5907  ovmpoga  5908  caovimo  5972  ofrval  6000  dfsmo2  6192  tfr1onlembfn  6249  tfrcllembfn  6262  freccllem  6307  frecfcllem  6309  frecsuclem  6311  frecrdg  6313  nnsucsssuc  6396  f1oen2g  6657  f1dom2g  6658  xpdom3m  6736  mapxpen  6750  diffifi  6796  unfidisj  6818  undifdc  6820  ssfidc  6831  sbthlemi9  6861  ctssdc  7006  endjudisj  7083  djuassen  7090  xpdjuen  7091  mulcanenq  7217  ltanqg  7232  addnnnq0  7281  nnanq0  7290  prltlu  7319  distrprg  7420  ltexprlemm  7432  recexprlem1ssl  7465  recexprlem1ssu  7466  addsrpr  7577  mulsrpr  7578  mulasssrg  7590  recexgt0sr  7605  ltpsrprg  7635  axmulass  7705  axpre-ltadd  7718  ltxrlt  7854  subadd2  7990  addsubass  7996  nppcan  8008  nppcan3  8010  subcan2  8011  subsub2  8014  subsub4  8019  pnpcan  8025  pnncan  8027  subcan  8041  subdi  8171  ltadd1  8215  leadd1  8216  leadd2  8217  ltsubadd  8218  ltsubadd2  8219  lesubadd  8220  lesubadd2  8221  ltaddsub  8222  leaddsub  8224  lesub1  8242  lesub2  8243  ltsub1  8244  ltsub2  8245  ltaddsublt  8357  gt0add  8359  reapadd1  8382  remulext1  8385  remulext2  8386  apadd2  8395  mulext2  8399  mulap0r  8401  leltap  8411  ltap  8419  apsub1  8428  divap0b  8467  divmulasscomap  8480  divcanap5  8498  dmdcanap  8506  redivclap  8515  div2negap  8519  lt2msq1  8667  ltdiv2  8669  nndivtr  8786  gtndiv  9170  eluzsub  9379  nn01to3  9436  qdivcl  9462  irrmul  9466  rpgecl  9499  divge1  9540  xaddass  9682  xltadd1  9689  ubioog  9727  ubioc1  9742  lbico1  9743  iccleub  9744  lbicc2  9797  ubicc2  9798  icoshftf1o  9804  fzen  9854  elfz1b  9901  uznfz  9914  elfzo0  9990  elfzo0z  9992  ubmelfzo  10008  fzonn0p1p1  10021  ubmelm1fzo  10034  qbtwnre  10065  flqwordi  10092  flltdivnn0lt  10108  ceiqle  10117  modqval  10128  modqvalr  10129  modqcl  10130  flqpmodeq  10131  modq0  10133  mulqmod0  10134  negqmod0  10135  modqge0  10136  modqlt  10137  modqdiffl  10139  modqdifz  10140  modqmulnn  10146  modqvalp1  10147  modqabs2  10162  modqmuladdnn0  10172  qnegmod  10173  addmodid  10176  modqeqmodmin  10198  modfzo0difsn  10199  addmodlteq  10202  frec2uzf1od  10210  expnegap0  10332  expgt1  10362  exprecap  10365  expaddzaplem  10367  expaddzap  10368  expmulzap  10370  mulbinom2  10439  expnbnd  10446  fihashss  10594  fimaxq  10605  seq3coll  10617  shftfibg  10624  redivap  10678  imdivap  10685  cjdivap  10713  maxleast  11017  lemininf  11037  ltmininf  11038  bdtrilem  11042  bdtri  11043  xrmaxaddlem  11061  xrmaxadd  11062  xrmineqinf  11070  xrltmininf  11071  xrminltinf  11073  xrminadd  11076  climuni  11094  reccn2ap  11114  isumz  11190  fsumsplitsnun  11220  geoisum1c  11321  prodfap0  11346  cos12dec  11510  summodnegmod  11560  dvdsmultr2  11569  mulmoddvds  11597  divalglemeuneg  11656  gcdaddm  11708  gcdass  11739  mulgcd  11740  gcddiv  11743  lcmass  11802  mulgcddvds  11811  qredeq  11813  congr  11817  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  prmexpb  11865  rpexp  11867  unennn  11946  fvsetsid  12032  ressid2  12057  ressval2  12058  rngmulrg  12116  basgen  12288  2basgeng  12290  ntrss  12327  neiss  12358  opnneiss  12366  restco  12382  restabs  12383  cnprcl2k  12414  cnpf2  12415  lmconst  12424  cnpnei  12427  cnptoprest  12447  cnmpt2t  12501  psmetsym  12537  psmetge0  12539  xmetge0  12573  xmetsym  12576  blvalps  12596  blval  12597  ssblps  12633  ssbl  12634  blpnfctr  12647  xmssym  12677  bdxmet  12709  metcnp3  12719  dvfvalap  12858  dvid  12870  dvcnp2cntop  12871  ptolemy  12953  rpcxpadd  13034  rpcxpsub  13037  rpmulcxp  13038  cxpmul  13041  rpcxple2  13046  rpcxplt2  13047  cxpcom  13065  rplogbval  13070  rplogbcl  13071  rplogbchbase  13075  rplogbreexp  13078  relogbexpap  13083  logbleb  13086  logblt  13087  rplogbcxp  13088  rpcxplogb  13089  relogbcxpbap  13090