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  2984  sotri2  5132  sotri3  5133  feq123  5471  resasplitss  5513  sefvex  5656  ftpg  5833  fsnunf  5849  fnfvima  5884  cocan1  5923  cocan2  5924  f1oiso2  5963  riotass  5996  moriotass  5997  ovmpox  6145  ovmpoga  6146  fvmpopr2d  6153  caovimo  6211  ofrval  6241  dfsmo2  6448  tfr1onlembfn  6505  tfrcllembfn  6518  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecrdg  6569  nnsucsssuc  6655  f1oen2g  6923  f1dom2g  6924  xpdom3m  7013  mapxpen  7029  diffifi  7076  unfidisj  7107  undifdc  7109  ssfidc  7122  sbthlemi9  7155  ctssdc  7303  endjudisj  7415  djuassen  7422  xpdjuen  7423  mulcanenq  7595  ltanqg  7610  addnnnq0  7659  nnanq0  7668  prltlu  7697  distrprg  7798  ltexprlemm  7810  recexprlem1ssl  7843  recexprlem1ssu  7844  addsrpr  7955  mulsrpr  7956  mulasssrg  7968  recexgt0sr  7983  ltpsrprg  8013  axmulass  8083  axpre-ltadd  8096  ltxrlt  8235  subadd2  8373  addsubass  8379  nppcan  8391  nppcan3  8393  subcan2  8394  subsub2  8397  subsub4  8402  pnpcan  8408  pnncan  8410  subcan  8424  subdi  8554  ltadd1  8599  leadd1  8600  leadd2  8601  ltsubadd  8602  ltsubadd2  8603  lesubadd  8604  lesubadd2  8605  ltaddsub  8606  leaddsub  8608  lesub1  8626  lesub2  8627  ltsub1  8628  ltsub2  8629  ltaddsublt  8741  gt0add  8743  reapadd1  8766  remulext1  8769  remulext2  8770  apadd2  8779  mulext2  8783  mulap0r  8785  leltap  8795  ltap  8803  apsub1  8812  divap0b  8853  divmulasscomap  8866  divcanap5  8884  dmdcanap  8892  redivclap  8901  div2negap  8905  lt2msq1  9055  ltdiv2  9057  ofnegsub  9132  nndivtr  9175  difgtsumgt  9539  gtndiv  9565  eluzsub  9776  nn01to3  9841  qdivcl  9867  irrmul  9871  rpgecl  9907  divge1  9948  xaddass  10094  xltadd1  10101  ubioog  10139  ubioc1  10154  lbico1  10155  iccleub  10156  lbicc2  10209  ubicc2  10210  icoshftf1o  10216  fzen  10268  elfz1b  10315  uznfz  10328  elfzo0  10411  elfzo0z  10413  ubmelfzo  10435  fzonn0p1p1  10448  ubmelm1fzo  10461  zsupssdc  10488  qbtwnre  10506  flqwordi  10538  flltdivnn0lt  10554  ceiqle  10565  modqval  10576  modqvalr  10577  modqcl  10578  flqpmodeq  10579  modq0  10581  mulqmod0  10582  negqmod0  10583  modqge0  10584  modqlt  10585  modqdiffl  10587  modqdifz  10588  modqmulnn  10594  modqvalp1  10595  modqabs2  10610  modqmuladdnn0  10620  qnegmod  10621  addmodid  10624  modqeqmodmin  10646  modfzo0difsn  10647  addmodlteq  10650  frec2uzf1od  10658  expnegap0  10799  expgt1  10829  exprecap  10832  expaddzaplem  10834  expaddzap  10835  expmulzap  10837  mulbinom2  10908  expnbnd  10915  fihashss  11070  fimaxq  11081  seq3coll  11096  ccatw2s1leng  11205  ccat2s1fvwd  11214  swrdval  11219  swrdnd  11230  swrdlen2  11233  pfxn0  11259  ccatopth2  11288  s3cl  11357  s3fv0g  11362  s3fv1g  11363  s3fv2g  11364  shftfibg  11371  redivap  11425  imdivap  11432  cjdivap  11460  maxleast  11764  lemininf  11785  ltmininf  11786  bdtrilem  11790  bdtri  11791  xrmaxaddlem  11811  xrmaxadd  11812  xrmineqinf  11820  xrltmininf  11821  xrminltinf  11823  xrminadd  11826  climuni  11844  reccn2ap  11864  isumz  11940  fsumsplitsnun  11970  geoisum1c  12071  prodfap0  12096  prod1dc  12137  fprodabs  12167  cos12dec  12319  summodnegmod  12373  dvdsmultr2  12384  mulmoddvds  12414  divalglemeuneg  12474  gcdaddm  12545  gcdass  12576  mulgcd  12577  gcddiv  12580  nnminle  12596  lcmass  12647  mulgcddvds  12656  qredeq  12658  congr  12662  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  prmexpb  12713  rpexp  12715  pythagtriplem1  12828  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem12  12838  pythagtriplem13  12839  pythagtriplem15  12841  pythagtriplem19  12845  pcdiv  12865  dvdsprmpweqle  12900  sumhashdc  12910  pcbc  12914  4sqlem12  12965  4sqlem18  12971  unennn  13008  nninfdc  13064  fvsetsid  13106  ressressg  13148  rngmulrg  13211  imasaddvallemg  13388  qusaddvallemg  13406  mgmsscl  13434  plusfvalg  13436  ress0g  13516  imasmnd2  13525  imasmnd  13526  gsumfzz  13568  grpasscan2  13637  grpidrcan  13638  grpidlcan  13639  grpinvadd  13651  grppncan  13664  dfgrp3me  13673  grpsubpropd2  13678  pwsinvg  13685  imasgrp2  13687  imasgrp  13688  mhmmnd  13693  mulgnnsubcl  13711  mulgnn0subcl  13712  mulgsubcl  13713  mulgaddcomlem  13722  mulgaddcom  13723  mulgpropdg  13741  submmulg  13743  subgcl  13761  subgsubcl  13762  subgsub  13763  subgmulg  13765  nsgconj  13783  ghmsub  13828  ghmnsgima  13845  ghmeqker  13848  f1ghm0to0  13849  ablinvadd  13887  ablpncan2  13893  subgabl  13909  rngcl  13947  imasrng  13959  srgcl  13973  ringcl  14016  crngcom  14017  ringidss  14032  ringcom  14034  mulgass2  14061  imasring  14067  opprringbg  14083  unitmulcl  14117  unitmulclb  14118  dvrcl  14139  unitdvcl  14140  dvrcan1  14144  dvrcan3  14145  rhmmul  14168  subrngmcl  14213  subrgmcl  14237  subrgdv  14242  domneq0  14276  islmod  14295  scafvalg  14311  lmodcom  14337  lmodprop2d  14352  rmodislmodlem  14354  rmodislmod  14355  lsselg  14365  lssvnegcl  14380  lspss  14403  lspun  14406  lspsnvsi  14422  lsslsp  14433  sralmod  14454  lidlnegcl  14489  rspssp  14498  rnglidlrng  14502  qus2idrng  14529  zndvds  14653  basgen  14794  2basgeng  14796  ntrss  14833  neiss  14864  opnneiss  14872  restco  14888  restabs  14889  cnprcl2k  14920  cnpf2  14921  lmconst  14930  cnpnei  14933  cnptoprest  14953  cnmpt2t  15007  psmetsym  15043  psmetge0  15045  xmetge0  15079  xmetsym  15082  blvalps  15102  blval  15103  ssblps  15139  ssbl  15140  blpnfctr  15153  xmssym  15183  bdxmet  15215  metcnp3  15225  dvfvalap  15395  dvid  15409  dvidre  15411  dvcnp2cntop  15413  elplyr  15454  ply1term  15457  plypow  15458  ptolemy  15538  rpcxpadd  15619  rpcxpsub  15622  rpmulcxp  15623  cxpmul  15626  rpcxple2  15632  rpcxplt2  15633  cxpcom  15652  rplogbval  15659  rplogbcl  15660  rplogbchbase  15664  rplogbreexp  15667  relogbexpap  15672  logbleb  15675  logblt  15676  rplogbcxp  15677  rpcxplogb  15678  relogbcxpbap  15679  sgmppw  15706  lgslem1  15719  lgsfvalg  15724  lgsval4  15739  lgsneg  15743  lgsne0  15757  lgsdinn0  15767  lgsquad  15799  funvtxvalg  15877  funiedgvalg  15878  upgrex  15944  uhgr2edg  16045  usgr2v1e2w  16085  iedginwlk  16154  upgrwlkedg  16158  clwwlkccat  16196  clwwlknonex2  16234