Theorem simp3 1023

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 1020	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )
2	1	simprd 114	1 |- ( ( ph /\ ps /\ ch ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simpl3  1026  simpr3  1029  simp3i  1032  simp3d  1035  simp13  1053  simp23  1056  simp33  1059  3anibar  1189  3ianorr  1343  intn3an3d  1392  stoic4a  1474  stoic4b  1475  mob2  2983  sotri2  5126  sotri3  5127  feq123  5465  resasplitss  5507  sefvex  5650  ftpg  5827  fsnunf  5843  fnfvima  5878  cocan1  5917  cocan2  5918  f1oiso2  5957  riotass  5990  moriotass  5991  ovmpox  6139  ovmpoga  6140  fvmpopr2d  6147  caovimo  6205  ofrval  6235  dfsmo2  6439  tfr1onlembfn  6496  tfrcllembfn  6509  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecrdg  6560  nnsucsssuc  6646  f1oen2g  6914  f1dom2g  6915  xpdom3m  7001  mapxpen  7017  diffifi  7064  unfidisj  7095  undifdc  7097  ssfidc  7110  sbthlemi9  7143  ctssdc  7291  endjudisj  7403  djuassen  7410  xpdjuen  7411  mulcanenq  7583  ltanqg  7598  addnnnq0  7647  nnanq0  7656  prltlu  7685  distrprg  7786  ltexprlemm  7798  recexprlem1ssl  7831  recexprlem1ssu  7832  addsrpr  7943  mulsrpr  7944  mulasssrg  7956  recexgt0sr  7971  ltpsrprg  8001  axmulass  8071  axpre-ltadd  8084  ltxrlt  8223  subadd2  8361  addsubass  8367  nppcan  8379  nppcan3  8381  subcan2  8382  subsub2  8385  subsub4  8390  pnpcan  8396  pnncan  8398  subcan  8412  subdi  8542  ltadd1  8587  leadd1  8588  leadd2  8589  ltsubadd  8590  ltsubadd2  8591  lesubadd  8592  lesubadd2  8593  ltaddsub  8594  leaddsub  8596  lesub1  8614  lesub2  8615  ltsub1  8616  ltsub2  8617  ltaddsublt  8729  gt0add  8731  reapadd1  8754  remulext1  8757  remulext2  8758  apadd2  8767  mulext2  8771  mulap0r  8773  leltap  8783  ltap  8791  apsub1  8800  divap0b  8841  divmulasscomap  8854  divcanap5  8872  dmdcanap  8880  redivclap  8889  div2negap  8893  lt2msq1  9043  ltdiv2  9045  ofnegsub  9120  nndivtr  9163  difgtsumgt  9527  gtndiv  9553  eluzsub  9764  nn01to3  9824  qdivcl  9850  irrmul  9854  rpgecl  9890  divge1  9931  xaddass  10077  xltadd1  10084  ubioog  10122  ubioc1  10137  lbico1  10138  iccleub  10139  lbicc2  10192  ubicc2  10193  icoshftf1o  10199  fzen  10251  elfz1b  10298  uznfz  10311  elfzo0  10394  elfzo0z  10396  ubmelfzo  10418  fzonn0p1p1  10431  ubmelm1fzo  10444  zsupssdc  10470  qbtwnre  10488  flqwordi  10520  flltdivnn0lt  10536  ceiqle  10547  modqval  10558  modqvalr  10559  modqcl  10560  flqpmodeq  10561  modq0  10563  mulqmod0  10564  negqmod0  10565  modqge0  10566  modqlt  10567  modqdiffl  10569  modqdifz  10570  modqmulnn  10576  modqvalp1  10577  modqabs2  10592  modqmuladdnn0  10602  qnegmod  10603  addmodid  10606  modqeqmodmin  10628  modfzo0difsn  10629  addmodlteq  10632  frec2uzf1od  10640  expnegap0  10781  expgt1  10811  exprecap  10814  expaddzaplem  10816  expaddzap  10817  expmulzap  10819  mulbinom2  10890  expnbnd  10897  fihashss  11051  fimaxq  11062  seq3coll  11077  swrdval  11195  swrdnd  11206  swrdlen2  11209  pfxn0  11235  ccatopth2  11264  s3cl  11333  s3fv0g  11338  s3fv1g  11339  shftfibg  11346  redivap  11400  imdivap  11407  cjdivap  11435  maxleast  11739  lemininf  11760  ltmininf  11761  bdtrilem  11765  bdtri  11766  xrmaxaddlem  11786  xrmaxadd  11787  xrmineqinf  11795  xrltmininf  11796  xrminltinf  11798  xrminadd  11801  climuni  11819  reccn2ap  11839  isumz  11915  fsumsplitsnun  11945  geoisum1c  12046  prodfap0  12071  prod1dc  12112  fprodabs  12142  cos12dec  12294  summodnegmod  12348  dvdsmultr2  12359  mulmoddvds  12389  divalglemeuneg  12449  gcdaddm  12520  gcdass  12551  mulgcd  12552  gcddiv  12555  nnminle  12571  lcmass  12622  mulgcddvds  12631  qredeq  12633  congr  12637  divgcdcoprmex  12639  cncongr1  12640  cncongr2  12641  prmexpb  12688  rpexp  12690  pythagtriplem1  12803  pythagtriplem6  12808  pythagtriplem7  12809  pythagtriplem12  12813  pythagtriplem13  12814  pythagtriplem15  12816  pythagtriplem19  12820  pcdiv  12840  dvdsprmpweqle  12875  sumhashdc  12885  pcbc  12889  4sqlem12  12940  4sqlem18  12946  unennn  12983  nninfdc  13039  fvsetsid  13081  ressressg  13123  rngmulrg  13186  imasaddvallemg  13363  qusaddvallemg  13381  mgmsscl  13409  plusfvalg  13411  ress0g  13491  imasmnd2  13500  imasmnd  13501  gsumfzz  13543  grpasscan2  13612  grpidrcan  13613  grpidlcan  13614  grpinvadd  13626  grppncan  13639  dfgrp3me  13648  grpsubpropd2  13653  pwsinvg  13660  imasgrp2  13662  imasgrp  13663  mhmmnd  13668  mulgnnsubcl  13686  mulgnn0subcl  13687  mulgsubcl  13688  mulgaddcomlem  13697  mulgaddcom  13698  mulgpropdg  13716  submmulg  13718  subgcl  13736  subgsubcl  13737  subgsub  13738  subgmulg  13740  nsgconj  13758  ghmsub  13803  ghmnsgima  13820  ghmeqker  13823  f1ghm0to0  13824  ablinvadd  13862  ablpncan2  13868  subgabl  13884  rngcl  13922  imasrng  13934  srgcl  13948  ringcl  13991  crngcom  13992  ringidss  14007  ringcom  14009  mulgass2  14036  imasring  14042  opprringbg  14058  unitmulcl  14092  unitmulclb  14093  dvrcl  14114  unitdvcl  14115  dvrcan1  14119  dvrcan3  14120  rhmmul  14143  subrngmcl  14188  subrgmcl  14212  subrgdv  14217  domneq0  14251  islmod  14270  scafvalg  14286  lmodcom  14312  lmodprop2d  14327  rmodislmodlem  14329  rmodislmod  14330  lsselg  14340  lssvnegcl  14355  lspss  14378  lspun  14381  lspsnvsi  14397  lsslsp  14408  sralmod  14429  lidlnegcl  14464  rspssp  14473  rnglidlrng  14477  qus2idrng  14504  zndvds  14628  basgen  14769  2basgeng  14771  ntrss  14808  neiss  14839  opnneiss  14847  restco  14863  restabs  14864  cnprcl2k  14895  cnpf2  14896  lmconst  14905  cnpnei  14908  cnptoprest  14928  cnmpt2t  14982  psmetsym  15018  psmetge0  15020  xmetge0  15054  xmetsym  15057  blvalps  15077  blval  15078  ssblps  15114  ssbl  15115  blpnfctr  15128  xmssym  15158  bdxmet  15190  metcnp3  15200  dvfvalap  15370  dvid  15384  dvidre  15386  dvcnp2cntop  15388  elplyr  15429  ply1term  15432  plypow  15433  ptolemy  15513  rpcxpadd  15594  rpcxpsub  15597  rpmulcxp  15598  cxpmul  15601  rpcxple2  15607  rpcxplt2  15608  cxpcom  15627  rplogbval  15634  rplogbcl  15635  rplogbchbase  15639  rplogbreexp  15642  relogbexpap  15647  logbleb  15650  logblt  15651  rplogbcxp  15652  rpcxplogb  15653  relogbcxpbap  15654  sgmppw  15681  lgslem1  15694  lgsfvalg  15699  lgsval4  15714  lgsneg  15718  lgsne0  15732  lgsdinn0  15742  lgsquad  15774  funvtxvalg  15852  funiedgvalg  15853  upgrex  15918  uhgr2edg  16019  iedginwlk  16098  upgrwlkedg  16102  clwwlkccat  16138