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 )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used 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  ifprdc  3819  sotri2  5185  sotri3  5186  feq123  5525  resasplitss  5569  fresaunres2disj  5570  sefvex  5716  ftpg  5899  fsnunf  5915  fnfvima  5953  cocan1  5993  cocan2  5994  f1oiso2  6033  riotass  6068  moriotass  6069  ovmpox  6217  ovmpoga  6218  fvmpopr2d  6225  caovimo  6283  ofrval  6313  suppvalfn  6481  fvn0elsuppb  6492  dfsmo2  6558  tfr1onlembfn  6615  tfrcllembfn  6628  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecrdg  6679  nnsucsssuc  6765  f1oen2g  7041  f1dom2g  7042  xpdom3m  7132  mapxpen  7148  diffifi  7198  unfidisj  7229  undifdc  7231  imaf1fi  7240  ssfidc  7245  sbthlemi9  7282  fdcf1  7316  ctssdc  7454  endjudisj  7567  djuassen  7574  xpdjuen  7575  mulcanenq  7753  ltanqg  7768  addnnnq0  7817  nnanq0  7826  prltlu  7855  distrprg  7956  ltexprlemm  7968  recexprlem1ssl  8001  recexprlem1ssu  8002  addsrpr  8113  mulsrpr  8114  mulasssrg  8126  recexgt0sr  8141  ltpsrprg  8171  axmulass  8241  axpre-ltadd  8254  ltxrlt  8392  subadd2  8532  addsubass  8538  nppcan  8550  nppcan3  8552  subcan2  8553  subsub2  8556  subsub4  8561  pnpcan  8567  pnncan  8569  subcan  8583  subdi  8714  ltadd1  8759  leadd1  8760  leadd2  8761  ltsubadd  8762  ltsubadd2  8763  lesubadd  8764  lesubadd2  8765  ltaddsub  8766  leaddsub  8768  lesub1  8786  lesub2  8787  ltsub1  8788  ltsub2  8789  ltaddsublt  8902  gt0add  8904  reapadd1  8927  remulext1  8930  remulext2  8931  apadd2  8940  mulext2  8944  mulap0r  8946  leltap  8956  ltap  8964  apsub1  8973  divap0b  9016  divmulasscomap  9029  divcanap5  9047  dmdcanap  9055  redivclap  9064  div2negap  9068  lt2msq1  9218  ltdiv2  9220  ofnegsub  9295  indfval  9302  ind1  9303  nndivtr  9349  difgtsumgt  9719  zfidc  9728  gtndiv  9746  eluzsub  9962  nn01to3  10027  qdivcl  10053  irrmul  10058  rpgecl  10094  divge1  10135  xaddass  10282  xltadd1  10289  ubioog  10327  ubioc1  10342  lbico1  10343  iccleub  10344  lbicc2  10397  ubicc2  10398  icoshftf1o  10404  fzen  10458  elfz1b  10508  uznfz  10521  elfzo0  10604  elfzo0z  10607  ubmelfzo  10629  fzonn0p1p1  10642  ubmelm1fzo  10655  zsupssdc  10684  qbtwnre  10702  flqwordi  10738  flltdivnn0lt  10754  ceiqle  10765  modqval  10776  modqvalr  10777  modqcl  10778  flqpmodeq  10779  modq0  10781  mulqmod0  10782  negqmod0  10783  modqge0  10784  modqlt  10785  modqdiffl  10787  modqdifz  10788  modqmulnn  10794  modqvalp1  10795  modqabs2  10810  modqmuladdnn0  10820  qnegmod  10821  addmodid  10824  modqeqmodmin  10846  modfzo0difsn  10847  addmodlteq  10850  frec2uzf1od  10858  expnegap0  10999  expgt1  11029  exprecap  11032  expaddzaplem  11034  expaddzap  11035  expmulzap  11037  mulbinom2  11108  expnbnd  11116  fihashss  11273  fimaxq  11286  seq3coll  11310  ccatw2s1leng  11422  ccat2s1fvwd  11431  swrdval  11436  swrdnd  11447  swrdlen2  11450  pfxn0  11476  ccatopth2  11505  s3cl  11574  s3fv0g  11579  s3fv1g  11580  s3fv2g  11581  shftfibg  11601  redivap  11655  imdivap  11662  cjdivap  11691  maxleast  11996  lemininf  12018  ltmininf  12019  bdtrilem  12024  bdtri  12025  xrmaxaddlem  12045  xrmaxadd  12046  xrmineqinf  12054  xrltmininf  12055  xrminltinf  12057  xrminadd  12060  climuni  12078  reccn2ap  12098  isumz  12175  fsumsplitsnun  12205  geoisum1c  12306  prodfap0  12331  prod1dc  12372  fprodabs  12402  cos12dec  12554  summodnegmod  12608  dvdsmultr2  12619  mulmoddvds  12649  divalglemeuneg  12709  gcdaddm  12780  gcdass  12811  mulgcd  12812  gcddiv  12815  nnminle  12831  lcmass  12882  mulgcddvds  12891  qredeq  12893  congr  12897  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  prmexpb  12949  rpexp  12951  pythagtriplem1  13067  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem12  13077  pythagtriplem13  13078  pythagtriplem15  13080  pythagtriplem19  13084  pcdiv  13104  dvdsprmpweqle  13139  sumhashdc  13149  pcbc  13153  4sqlem12  13204  4sqlem18  13210  ballotfilemsgt1  13306  ballotfilemfrcn0  13325  unennn  13340  nninfdc  13396  fvsetsid  13438  ressressg  13482  rngmulrg  13545  imasaddvallemg  13689  qusaddvallemg  13707  mgmsscl  13734  plusfvalg  13736  ress0g  13809  imasmnd2  13812  imasmnd  13813  grpasscan2  13922  grpidrcan  13923  grpidlcan  13924  grpinvadd  13936  grppncan  13949  dfgrp3me  13958  grpsubpropd2  13963  imasgrp2  13966  imasgrp  13967  mhmmnd  13972  mulgnnsubcl  13990  mulgnn0subcl  13991  mulgsubcl  13992  mulgaddcomlem  14001  mulgaddcom  14002  mulgpropdg  14020  submmulg  14022  subgcl  14040  subgsubcl  14041  subgsub  14042  subgmulg  14044  nsgconj  14062  ghmsub  14107  ghmnsgima  14124  ghmeqker  14127  f1ghm0to0  14128  ablinvadd  14198  ablpncan2  14204  subgabl  14220  gsumsncmn  14240  gsumconstcmn  14250  pwsinvg  14299  rngcl  14327  imasrng  14339  rng1zrlem  14342  srgcl  14358  ringcl  14401  crngcom  14402  ringidss  14418  ringcom  14420  mulgass2  14447  imasring  14453  opprringbg  14469  unitmulcl  14504  unitmulclb  14505  dvrcl  14526  unitdvcl  14527  dvrcan1  14531  dvrcan3  14532  rhmmul  14555  subrngmcl  14601  subrgmcl  14625  subrgdv  14630  domneq0  14665  islmod  14711  scafvalg  14728  lmodcom  14754  lmodprop2d  14769  rmodislmodlem  14771  rmodislmod  14772  lsselg  14782  lssvnegcl  14797  lspss  14820  lspun  14823  lspsnvsi  14839  lsslsp  14850  sralmod  14871  lidlnegcl  14906  rspssp  14915  rnglidlrng  14919  qus2idrng  14946  zndvds  15068  aspss  15103  asclmul1  15113  asclmul2  15114  ascldimul  15115  asclinvg  15116  asclmulg  15128  psrbagaddclfi  15145  psrbagcon  15146  basgen  15272  2basgeng  15274  ntrss  15311  neiss  15342  opnneiss  15350  restco  15366  restabs  15367  cnprcl2k  15398  cnpf2  15399  lmconst  15408  cnpnei  15411  cnptoprest  15431  cnmpt2t  15485  psmetsym  15521  psmetge0  15523  xmetge0  15557  xmetsym  15560  blvalps  15580  blval  15581  ssblps  15617  ssbl  15618  blpnfctr  15631  xmssym  15661  bdxmet  15693  metcnp3  15703  dvfvalap  15873  dvid  15887  dvidre  15889  dvcnp2cntop  15891  elplyr  15932  ply1term  15935  plypow  15936  ptolemy  16017  logfac  16090  rpcxpadd  16102  rpcxpsub  16105  rpmulcxp  16106  cxpmul  16109  rpcxple2  16115  rpcxplt2  16116  cxpcom  16135  rplogbval  16142  rplogbcl  16143  rplogbchbase  16147  rplogbreexp  16150  relogbexpap  16155  logbleb  16158  logblt  16159  rplogbcxp  16160  rpcxplogb  16161  relogbcxpbap  16162  chtqwordi  16224  ppiqwordi  16229  sgmppw  16247  bcmono  16265  prmefexple  16269  lgslem1  16285  lgsfvalg  16290  lgsval4  16305  lgsneg  16309  lgsne0  16323  lgsdinn0  16333  lgsquad  16365  funvtxvalg  16443  funiedgvalg  16444  upgrex  16510  uhgr2edg  16613  usgr2v1e2w  16653  subumgredg2en  16678  iedginwlk  16764  upgrwlkedg  16768  clwwlkccat  16808  clwwlknonex2  16846  eulerpathprum  16887  dichmul0or  16926  repiecele0  17241  repiecege0  17242