Theorem simp3 948

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

Syntax hints:   → wi 4   ∧ w3a 927

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

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

This theorem is referenced by:  simpl3  951  simpr3  954  simp3i  957  simp3d  960  simp13  978  simp23  981  simp33  984  3anibar  1114  3ianorr  1252  stoic4a  1373  stoic4b  1374  mob2  2809  sotri2  4862  sotri3  4863  feq123  5187  resasplitss  5225  sefvex  5361  ftpg  5520  fsnunf  5536  fnfvima  5568  cocan1  5604  cocan2  5605  f1oiso2  5644  riotass  5673  moriotass  5674  ovmpt2x  5811  ovmpt2ga  5812  caovimo  5876  ofrval  5904  dfsmo2  6090  tfr1onlembfn  6147  tfrcllembfn  6160  freccllem  6205  frecfcllem  6207  frecsuclem  6209  frecrdg  6211  nnsucsssuc  6293  f1oen2g  6552  f1dom2g  6553  xpdom3m  6630  mapxpen  6644  diffifi  6690  unfidisj  6712  undifdc  6714  ssfidc  6724  sbthlemi9  6754  mulcanenq  7041  ltanqg  7056  addnnnq0  7105  nnanq0  7114  prltlu  7143  distrprg  7244  ltexprlemm  7256  recexprlem1ssl  7289  recexprlem1ssu  7290  addsrpr  7388  mulsrpr  7389  mulasssrg  7401  recexgt0sr  7416  axmulass  7505  axpre-ltadd  7518  ltxrlt  7649  subadd2  7783  addsubass  7789  nppcan  7801  nppcan3  7803  subcan2  7804  subsub2  7807  subsub4  7812  pnpcan  7818  pnncan  7820  subcan  7834  subdi  7960  ltadd1  8004  leadd1  8005  leadd2  8006  ltsubadd  8007  ltsubadd2  8008  lesubadd  8009  lesubadd2  8010  ltaddsub  8011  leaddsub  8013  lesub1  8031  lesub2  8032  ltsub1  8033  ltsub2  8034  ltaddsublt  8145  gt0add  8147  reapadd1  8170  remulext1  8173  remulext2  8174  apadd2  8183  mulext2  8187  mulap0r  8189  leltap  8198  ltap  8205  apsub1  8214  divap0b  8247  divmulasscomap  8260  divcanap5  8278  dmdcanap  8286  redivclap  8295  div2negap  8299  lt2msq1  8443  ltdiv2  8445  nndivtr  8562  gtndiv  8940  eluzsub  9147  nn01to3  9201  qdivcl  9227  irrmul  9231  rpgecl  9261  divge1  9299  xaddass  9435  xltadd1  9442  ubioog  9480  ubioc1  9495  lbico1  9496  iccleub  9497  lbicc2  9550  ubicc2  9551  icoshftf1o  9557  fzen  9606  elfz1b  9653  uznfz  9666  elfzo0  9742  elfzo0z  9744  ubmelfzo  9760  fzonn0p1p1  9773  ubmelm1fzo  9786  qbtwnre  9817  flqwordi  9844  flltdivnn0lt  9860  ceiqle  9869  modqval  9880  modqvalr  9881  modqcl  9882  flqpmodeq  9883  modq0  9885  mulqmod0  9886  negqmod0  9887  modqge0  9888  modqlt  9889  modqdiffl  9891  modqdifz  9892  modqmulnn  9898  modqvalp1  9899  modqabs2  9914  modqmuladdnn0  9924  qnegmod  9925  addmodid  9928  modqeqmodmin  9950  modfzo0difsn  9951  addmodlteq  9954  frec2uzf1od  9962  expnegap0  10078  expgt1  10108  exprecap  10111  expaddzaplem  10113  expaddzap  10114  expmulzap  10116  mulbinom2  10185  expnbnd  10192  fihashss  10339  fimaxq  10350  seq3coll  10362  shftfibg  10369  redivap  10423  imdivap  10430  cjdivap  10458  maxleast  10761  lemininf  10780  ltmininf  10781  bdtrilem  10785  bdtri  10786  xrmaxaddlem  10803  xrmaxadd  10804  xrmineqinf  10812  xrltmininf  10813  xrminltinf  10815  xrminadd  10818  climuni  10836  reccn2ap  10856  isumz  10932  fsumsplitsnun  10962  geoisum1c  11063  summodnegmod  11254  dvdsmultr2  11263  mulmoddvds  11291  divalglemeuneg  11350  gcdaddm  11402  gcdass  11431  mulgcd  11432  gcddiv  11435  lcmass  11494  mulgcddvds  11503  qredeq  11505  congr  11509  divgcdcoprmex  11511  cncongr1  11512  cncongr2  11513  prmexpb  11557  rpexp  11559  unennn  11637  fvsetsid  11677  ressid2  11702  ressval2  11703  rngmulrg  11761  basgen  11932  2basgeng  11934  ntrss  11971  neiss  12002  opnneiss  12010  restco  12026  restabs  12027  cnprcl2k  12057  cnpf2  12058  lmconst  12067  cnpnei  12070  cnptoprest  12090  psmetsym  12115  psmetge0  12117  xmetge0  12151  xmetsym  12154  blvalps  12174  blval  12175  ssblps  12211  ssbl  12212  blpnfctr  12225  xmssym  12255  bdxmet  12287  metcnp3  12293