Theorem simp3 1001

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

Assertion

Ref	Expression
simp3	|- ( ( ph /\ ps /\ ch ) -> ch )

Proof of Theorem simp3

Step	Hyp	Ref	Expression
1		3simpc 998	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )
2	1	simprd 114	1 |- ( ( ph /\ ps /\ ch ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  simpl3  1004  simpr3  1007  simp3i  1010  simp3d  1013  simp13  1031  simp23  1034  simp33  1037  3anibar  1167  3ianorr  1320  stoic4a  1443  stoic4b  1444  mob2  2944  sotri2  5068  sotri3  5069  feq123  5400  resasplitss  5438  sefvex  5580  ftpg  5747  fsnunf  5763  fnfvima  5798  cocan1  5835  cocan2  5836  f1oiso2  5875  riotass  5906  moriotass  5907  ovmpox  6052  ovmpoga  6053  fvmpopr2d  6060  caovimo  6118  ofrval  6147  dfsmo2  6346  tfr1onlembfn  6403  tfrcllembfn  6416  freccllem  6461  frecfcllem  6463  frecsuclem  6465  frecrdg  6467  nnsucsssuc  6551  f1oen2g  6815  f1dom2g  6816  xpdom3m  6894  mapxpen  6910  diffifi  6956  unfidisj  6984  undifdc  6986  ssfidc  6999  sbthlemi9  7032  ctssdc  7180  endjudisj  7279  djuassen  7286  xpdjuen  7287  mulcanenq  7454  ltanqg  7469  addnnnq0  7518  nnanq0  7527  prltlu  7556  distrprg  7657  ltexprlemm  7669  recexprlem1ssl  7702  recexprlem1ssu  7703  addsrpr  7814  mulsrpr  7815  mulasssrg  7827  recexgt0sr  7842  ltpsrprg  7872  axmulass  7942  axpre-ltadd  7955  ltxrlt  8094  subadd2  8232  addsubass  8238  nppcan  8250  nppcan3  8252  subcan2  8253  subsub2  8256  subsub4  8261  pnpcan  8267  pnncan  8269  subcan  8283  subdi  8413  ltadd1  8458  leadd1  8459  leadd2  8460  ltsubadd  8461  ltsubadd2  8462  lesubadd  8463  lesubadd2  8464  ltaddsub  8465  leaddsub  8467  lesub1  8485  lesub2  8486  ltsub1  8487  ltsub2  8488  ltaddsublt  8600  gt0add  8602  reapadd1  8625  remulext1  8628  remulext2  8629  apadd2  8638  mulext2  8642  mulap0r  8644  leltap  8654  ltap  8662  apsub1  8671  divap0b  8712  divmulasscomap  8725  divcanap5  8743  dmdcanap  8751  redivclap  8760  div2negap  8764  lt2msq1  8914  ltdiv2  8916  ofnegsub  8991  nndivtr  9034  difgtsumgt  9397  gtndiv  9423  eluzsub  9633  nn01to3  9693  qdivcl  9719  irrmul  9723  rpgecl  9759  divge1  9800  xaddass  9946  xltadd1  9953  ubioog  9991  ubioc1  10006  lbico1  10007  iccleub  10008  lbicc2  10061  ubicc2  10062  icoshftf1o  10068  fzen  10120  elfz1b  10167  uznfz  10180  elfzo0  10260  elfzo0z  10262  ubmelfzo  10278  fzonn0p1p1  10291  ubmelm1fzo  10304  zsupssdc  10330  qbtwnre  10348  flqwordi  10380  flltdivnn0lt  10396  ceiqle  10407  modqval  10418  modqvalr  10419  modqcl  10420  flqpmodeq  10421  modq0  10423  mulqmod0  10424  negqmod0  10425  modqge0  10426  modqlt  10427  modqdiffl  10429  modqdifz  10430  modqmulnn  10436  modqvalp1  10437  modqabs2  10452  modqmuladdnn0  10462  qnegmod  10463  addmodid  10466  modqeqmodmin  10488  modfzo0difsn  10489  addmodlteq  10492  frec2uzf1od  10500  expnegap0  10641  expgt1  10671  exprecap  10674  expaddzaplem  10676  expaddzap  10677  expmulzap  10679  mulbinom2  10750  expnbnd  10757  fihashss  10910  fimaxq  10921  seq3coll  10936  shftfibg  10987  redivap  11041  imdivap  11048  cjdivap  11076  maxleast  11380  lemininf  11401  ltmininf  11402  bdtrilem  11406  bdtri  11407  xrmaxaddlem  11427  xrmaxadd  11428  xrmineqinf  11436  xrltmininf  11437  xrminltinf  11439  xrminadd  11442  climuni  11460  reccn2ap  11480  isumz  11556  fsumsplitsnun  11586  geoisum1c  11687  prodfap0  11712  prod1dc  11753  fprodabs  11783  cos12dec  11935  summodnegmod  11989  dvdsmultr2  12000  mulmoddvds  12030  divalglemeuneg  12090  gcdaddm  12161  gcdass  12192  mulgcd  12193  gcddiv  12196  nnminle  12212  lcmass  12263  mulgcddvds  12272  qredeq  12274  congr  12278  divgcdcoprmex  12280  cncongr1  12281  cncongr2  12282  prmexpb  12329  rpexp  12331  pythagtriplem1  12444  pythagtriplem6  12449  pythagtriplem7  12450  pythagtriplem12  12454  pythagtriplem13  12455  pythagtriplem15  12457  pythagtriplem19  12461  pcdiv  12481  dvdsprmpweqle  12516  sumhashdc  12526  pcbc  12530  4sqlem12  12581  4sqlem18  12587  unennn  12624  nninfdc  12680  fvsetsid  12722  ressressg  12763  rngmulrg  12825  imasaddvallemg  12968  qusaddvallemg  12986  mgmsscl  13014  plusfvalg  13016  ress0g  13094  gsumfzz  13137  grpasscan2  13206  grpidrcan  13207  grpidlcan  13208  grpinvadd  13220  grppncan  13233  dfgrp3me  13242  grpsubpropd2  13247  imasgrp2  13250  imasgrp  13251  mhmmnd  13256  mulgnnsubcl  13274  mulgnn0subcl  13275  mulgsubcl  13276  mulgaddcomlem  13285  mulgaddcom  13286  mulgpropdg  13304  submmulg  13306  subgcl  13324  subgsubcl  13325  subgsub  13326  subgmulg  13328  nsgconj  13346  ghmsub  13391  ghmnsgima  13408  ghmeqker  13411  f1ghm0to0  13412  ablinvadd  13450  ablpncan2  13456  subgabl  13472  rngcl  13510  imasrng  13522  srgcl  13536  ringcl  13579  crngcom  13580  ringidss  13595  ringcom  13597  mulgass2  13624  imasring  13630  opprringbg  13646  unitmulcl  13679  unitmulclb  13680  dvrcl  13701  unitdvcl  13702  dvrcan1  13706  dvrcan3  13707  rhmmul  13730  subrngmcl  13775  subrgmcl  13799  subrgdv  13804  domneq0  13838  islmod  13857  scafvalg  13873  lmodcom  13899  lmodprop2d  13914  rmodislmodlem  13916  rmodislmod  13917  lsselg  13927  lssvnegcl  13942  lspss  13965  lspun  13968  lspsnvsi  13984  lsslsp  13995  sralmod  14016  lidlnegcl  14051  rspssp  14060  rnglidlrng  14064  qus2idrng  14091  zndvds  14215  basgen  14326  2basgeng  14328  ntrss  14365  neiss  14396  opnneiss  14404  restco  14420  restabs  14421  cnprcl2k  14452  cnpf2  14453  lmconst  14462  cnpnei  14465  cnptoprest  14485  cnmpt2t  14539  psmetsym  14575  psmetge0  14577  xmetge0  14611  xmetsym  14614  blvalps  14634  blval  14635  ssblps  14671  ssbl  14672  blpnfctr  14685  xmssym  14715  bdxmet  14747  metcnp3  14757  dvfvalap  14927  dvid  14941  dvidre  14943  dvcnp2cntop  14945  elplyr  14986  ply1term  14989  plypow  14990  ptolemy  15070  rpcxpadd  15151  rpcxpsub  15154  rpmulcxp  15155  cxpmul  15158  rpcxple2  15164  rpcxplt2  15165  cxpcom  15184  rplogbval  15191  rplogbcl  15192  rplogbchbase  15196  rplogbreexp  15199  relogbexpap  15204  logbleb  15207  logblt  15208  rplogbcxp  15209  rpcxplogb  15210  relogbcxpbap  15211  sgmppw  15238  lgslem1  15251  lgsfvalg  15256  lgsval4  15271  lgsneg  15275  lgsne0  15289  lgsdinn0  15299  lgsquad  15331