Theorem simp3 1030

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

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced by:  simpl3  1033  simpr3  1036  simp3i  1039  simp3d  1042  simp13  1060  simp23  1063  simp33  1066  3anibar  1196  3ianorr  1350  intn3an3d  1399  stoic4a  1481  stoic4b  1482  mob2  3006  sotri2  5180  sotri3  5181  feq123  5520  resasplitss  5564  fresaunres2disj  5565  sefvex  5711  ftpg  5890  fsnunf  5906  fnfvima  5943  cocan1  5983  cocan2  5984  f1oiso2  6023  riotass  6058  moriotass  6059  ovmpox  6207  ovmpoga  6208  fvmpopr2d  6215  caovimo  6273  ofrval  6303  suppvalfn  6471  fvn0elsuppb  6482  dfsmo2  6548  tfr1onlembfn  6605  tfrcllembfn  6618  freccllem  6663  frecfcllem  6665  frecsuclem  6667  frecrdg  6669  nnsucsssuc  6755  f1oen2g  7031  f1dom2g  7032  xpdom3m  7122  mapxpen  7138  diffifi  7188  unfidisj  7219  undifdc  7221  imaf1fi  7230  ssfidc  7235  sbthlemi9  7272  fdcf1  7306  ctssdc  7443  endjudisj  7556  djuassen  7563  xpdjuen  7564  mulcanenq  7742  ltanqg  7757  addnnnq0  7806  nnanq0  7815  prltlu  7844  distrprg  7945  ltexprlemm  7957  recexprlem1ssl  7990  recexprlem1ssu  7991  addsrpr  8102  mulsrpr  8103  mulasssrg  8115  recexgt0sr  8130  ltpsrprg  8160  axmulass  8230  axpre-ltadd  8243  ltxrlt  8381  subadd2  8520  addsubass  8526  nppcan  8538  nppcan3  8540  subcan2  8541  subsub2  8544  subsub4  8549  pnpcan  8555  pnncan  8557  subcan  8571  subdi  8702  ltadd1  8747  leadd1  8748  leadd2  8749  ltsubadd  8750  ltsubadd2  8751  lesubadd  8752  lesubadd2  8753  ltaddsub  8754  leaddsub  8756  lesub1  8774  lesub2  8775  ltsub1  8776  ltsub2  8777  ltaddsublt  8889  gt0add  8891  reapadd1  8914  remulext1  8917  remulext2  8918  apadd2  8927  mulext2  8931  mulap0r  8933  leltap  8943  ltap  8951  apsub1  8960  divap0b  9003  divmulasscomap  9016  divcanap5  9034  dmdcanap  9042  redivclap  9051  div2negap  9055  lt2msq1  9205  ltdiv2  9207  ofnegsub  9282  nndivtr  9325  difgtsumgt  9693  zfidc  9702  gtndiv  9720  eluzsub  9931  nn01to3  9996  qdivcl  10022  irrmul  10026  rpgecl  10062  divge1  10103  xaddass  10250  xltadd1  10257  ubioog  10295  ubioc1  10310  lbico1  10311  iccleub  10312  lbicc2  10365  ubicc2  10366  icoshftf1o  10372  fzen  10426  elfz1b  10475  uznfz  10488  elfzo0  10571  elfzo0z  10574  ubmelfzo  10596  fzonn0p1p1  10609  ubmelm1fzo  10622  zsupssdc  10651  qbtwnre  10669  flqwordi  10701  flltdivnn0lt  10717  ceiqle  10728  modqval  10739  modqvalr  10740  modqcl  10741  flqpmodeq  10742  modq0  10744  mulqmod0  10745  negqmod0  10746  modqge0  10747  modqlt  10748  modqdiffl  10750  modqdifz  10751  modqmulnn  10757  modqvalp1  10758  modqabs2  10773  modqmuladdnn0  10783  qnegmod  10784  addmodid  10787  modqeqmodmin  10809  modfzo0difsn  10810  addmodlteq  10813  frec2uzf1od  10821  expnegap0  10962  expgt1  10992  exprecap  10995  expaddzaplem  10997  expaddzap  10998  expmulzap  11000  mulbinom2  11071  expnbnd  11079  fihashss  11235  fimaxq  11248  seq3coll  11272  ccatw2s1leng  11384  ccat2s1fvwd  11393  swrdval  11398  swrdnd  11409  swrdlen2  11412  pfxn0  11438  ccatopth2  11467  s3cl  11536  s3fv0g  11541  s3fv1g  11542  s3fv2g  11543  shftfibg  11563  redivap  11617  imdivap  11624  cjdivap  11653  maxleast  11957  lemininf  11978  ltmininf  11979  bdtrilem  11983  bdtri  11984  xrmaxaddlem  12004  xrmaxadd  12005  xrmineqinf  12013  xrltmininf  12014  xrminltinf  12016  xrminadd  12019  climuni  12037  reccn2ap  12057  isumz  12134  fsumsplitsnun  12164  geoisum1c  12265  prodfap0  12290  prod1dc  12331  fprodabs  12361  cos12dec  12513  summodnegmod  12567  dvdsmultr2  12578  mulmoddvds  12608  divalglemeuneg  12668  gcdaddm  12739  gcdass  12770  mulgcd  12771  gcddiv  12774  nnminle  12790  lcmass  12841  mulgcddvds  12850  qredeq  12852  congr  12856  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  prmexpb  12907  rpexp  12909  pythagtriplem1  13022  pythagtriplem6  13027  pythagtriplem7  13028  pythagtriplem12  13032  pythagtriplem13  13033  pythagtriplem15  13035  pythagtriplem19  13039  pcdiv  13059  dvdsprmpweqle  13094  sumhashdc  13104  pcbc  13108  4sqlem12  13159  4sqlem18  13165  ballotfilemsgt1  13232  ballotfilemfrcn0  13251  unennn  13266  nninfdc  13322  fvsetsid  13364  ressressg  13406  rngmulrg  13469  imasaddvallemg  13613  qusaddvallemg  13631  mgmsscl  13658  plusfvalg  13660  ress0g  13733  imasmnd2  13736  imasmnd  13737  grpasscan2  13846  grpidrcan  13847  grpidlcan  13848  grpinvadd  13860  grppncan  13873  dfgrp3me  13882  grpsubpropd2  13887  imasgrp2  13890  imasgrp  13891  mhmmnd  13896  mulgnnsubcl  13914  mulgnn0subcl  13915  mulgsubcl  13916  mulgaddcomlem  13925  mulgaddcom  13926  mulgpropdg  13944  submmulg  13946  subgcl  13964  subgsubcl  13965  subgsub  13966  subgmulg  13968  nsgconj  13986  ghmsub  14031  ghmnsgima  14048  ghmeqker  14051  f1ghm0to0  14052  ablinvadd  14091  ablpncan2  14097  subgabl  14113  gsumsncmn  14133  gsumconstcmn  14143  pwsinvg  14192  rngcl  14218  imasrng  14230  rng1zrlem  14233  srgcl  14248  ringcl  14291  crngcom  14292  ringidss  14307  ringcom  14309  mulgass2  14336  imasring  14342  opprringbg  14358  unitmulcl  14393  unitmulclb  14394  dvrcl  14415  unitdvcl  14416  dvrcan1  14420  dvrcan3  14421  rhmmul  14444  subrngmcl  14490  subrgmcl  14514  subrgdv  14519  domneq0  14554  islmod  14600  scafvalg  14616  lmodcom  14642  lmodprop2d  14657  rmodislmodlem  14659  rmodislmod  14660  lsselg  14670  lssvnegcl  14685  lspss  14708  lspun  14711  lspsnvsi  14727  lsslsp  14738  sralmod  14759  lidlnegcl  14794  rspssp  14803  rnglidlrng  14807  qus2idrng  14834  zndvds  14956  psrbagaddclfi  14984  psrbagcon  14985  basgen  15104  2basgeng  15106  ntrss  15143  neiss  15174  opnneiss  15182  restco  15198  restabs  15199  cnprcl2k  15230  cnpf2  15231  lmconst  15240  cnpnei  15243  cnptoprest  15263  cnmpt2t  15317  psmetsym  15353  psmetge0  15355  xmetge0  15389  xmetsym  15392  blvalps  15412  blval  15413  ssblps  15449  ssbl  15450  blpnfctr  15463  xmssym  15493  bdxmet  15525  metcnp3  15535  dvfvalap  15705  dvid  15719  dvidre  15721  dvcnp2cntop  15723  elplyr  15764  ply1term  15767  plypow  15768  ptolemy  15848  logfac  15918  rpcxpadd  15930  rpcxpsub  15933  rpmulcxp  15934  cxpmul  15937  rpcxple2  15943  rpcxplt2  15944  cxpcom  15963  rplogbval  15970  rplogbcl  15971  rplogbchbase  15975  rplogbreexp  15978  relogbexpap  15983  logbleb  15986  logblt  15987  rplogbcxp  15988  rpcxplogb  15989  relogbcxpbap  15990  sgmppw  16020  lgslem1  16033  lgsfvalg  16038  lgsval4  16053  lgsneg  16057  lgsne0  16071  lgsdinn0  16081  lgsquad  16113  funvtxvalg  16191  funiedgvalg  16192  upgrex  16258  uhgr2edg  16361  usgr2v1e2w  16401  subumgredg2en  16426  iedginwlk  16512  upgrwlkedg  16516  clwwlkccat  16556  clwwlknonex2  16594  eulerpathprum  16635  dichmul0or  16674  repiecele0  16980  repiecege0  16981