Theorem simp3 1026

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simpl3  1029  simpr3  1032  simp3i  1035  simp3d  1038  simp13  1056  simp23  1059  simp33  1062  3anibar  1192  3ianorr  1346  intn3an3d  1395  stoic4a  1477  stoic4b  1478  mob2  2987  sotri2  5141  sotri3  5142  feq123  5481  resasplitss  5524  sefvex  5669  ftpg  5846  fsnunf  5862  fnfvima  5899  cocan1  5938  cocan2  5939  f1oiso2  5978  riotass  6011  moriotass  6012  ovmpox  6160  ovmpoga  6161  fvmpopr2d  6168  caovimo  6226  ofrval  6255  suppvalfn  6419  fvn0elsuppb  6430  dfsmo2  6496  tfr1onlembfn  6553  tfrcllembfn  6566  freccllem  6611  frecfcllem  6613  frecsuclem  6615  frecrdg  6617  nnsucsssuc  6703  f1oen2g  6971  f1dom2g  6972  xpdom3m  7061  mapxpen  7077  diffifi  7126  unfidisj  7157  undifdc  7159  imaf1fi  7168  ssfidc  7173  sbthlemi9  7207  ctssdc  7355  endjudisj  7468  djuassen  7475  xpdjuen  7476  mulcanenq  7648  ltanqg  7663  addnnnq0  7712  nnanq0  7721  prltlu  7750  distrprg  7851  ltexprlemm  7863  recexprlem1ssl  7896  recexprlem1ssu  7897  addsrpr  8008  mulsrpr  8009  mulasssrg  8021  recexgt0sr  8036  ltpsrprg  8066  axmulass  8136  axpre-ltadd  8149  ltxrlt  8287  subadd2  8425  addsubass  8431  nppcan  8443  nppcan3  8445  subcan2  8446  subsub2  8449  subsub4  8454  pnpcan  8460  pnncan  8462  subcan  8476  subdi  8606  ltadd1  8651  leadd1  8652  leadd2  8653  ltsubadd  8654  ltsubadd2  8655  lesubadd  8656  lesubadd2  8657  ltaddsub  8658  leaddsub  8660  lesub1  8678  lesub2  8679  ltsub1  8680  ltsub2  8681  ltaddsublt  8793  gt0add  8795  reapadd1  8818  remulext1  8821  remulext2  8822  apadd2  8831  mulext2  8835  mulap0r  8837  leltap  8847  ltap  8855  apsub1  8864  divap0b  8905  divmulasscomap  8918  divcanap5  8936  dmdcanap  8944  redivclap  8953  div2negap  8957  lt2msq1  9107  ltdiv2  9109  ofnegsub  9184  nndivtr  9227  difgtsumgt  9593  gtndiv  9619  eluzsub  9830  nn01to3  9895  qdivcl  9921  irrmul  9925  rpgecl  9961  divge1  10002  xaddass  10148  xltadd1  10155  ubioog  10193  ubioc1  10208  lbico1  10209  iccleub  10210  lbicc2  10263  ubicc2  10264  icoshftf1o  10270  fzen  10323  elfz1b  10370  uznfz  10383  elfzo0  10466  elfzo0z  10469  ubmelfzo  10491  fzonn0p1p1  10504  ubmelm1fzo  10517  zsupssdc  10544  qbtwnre  10562  flqwordi  10594  flltdivnn0lt  10610  ceiqle  10621  modqval  10632  modqvalr  10633  modqcl  10634  flqpmodeq  10635  modq0  10637  mulqmod0  10638  negqmod0  10639  modqge0  10640  modqlt  10641  modqdiffl  10643  modqdifz  10644  modqmulnn  10650  modqvalp1  10651  modqabs2  10666  modqmuladdnn0  10676  qnegmod  10677  addmodid  10680  modqeqmodmin  10702  modfzo0difsn  10703  addmodlteq  10706  frec2uzf1od  10714  expnegap0  10855  expgt1  10885  exprecap  10888  expaddzaplem  10890  expaddzap  10891  expmulzap  10893  mulbinom2  10964  expnbnd  10971  fihashss  11126  fimaxq  11137  seq3coll  11152  ccatw2s1leng  11264  ccat2s1fvwd  11273  swrdval  11278  swrdnd  11289  swrdlen2  11292  pfxn0  11318  ccatopth2  11347  s3cl  11416  s3fv0g  11421  s3fv1g  11422  s3fv2g  11423  shftfibg  11443  redivap  11497  imdivap  11504  cjdivap  11532  maxleast  11836  lemininf  11857  ltmininf  11858  bdtrilem  11862  bdtri  11863  xrmaxaddlem  11883  xrmaxadd  11884  xrmineqinf  11892  xrltmininf  11893  xrminltinf  11895  xrminadd  11898  climuni  11916  reccn2ap  11936  isumz  12013  fsumsplitsnun  12043  geoisum1c  12144  prodfap0  12169  prod1dc  12210  fprodabs  12240  cos12dec  12392  summodnegmod  12446  dvdsmultr2  12457  mulmoddvds  12487  divalglemeuneg  12547  gcdaddm  12618  gcdass  12649  mulgcd  12650  gcddiv  12653  nnminle  12669  lcmass  12720  mulgcddvds  12729  qredeq  12731  congr  12735  divgcdcoprmex  12737  cncongr1  12738  cncongr2  12739  prmexpb  12786  rpexp  12788  pythagtriplem1  12901  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem12  12911  pythagtriplem13  12912  pythagtriplem15  12914  pythagtriplem19  12918  pcdiv  12938  dvdsprmpweqle  12973  sumhashdc  12983  pcbc  12987  4sqlem12  13038  4sqlem18  13044  unennn  13081  nninfdc  13137  fvsetsid  13179  ressressg  13221  rngmulrg  13284  imasaddvallemg  13461  qusaddvallemg  13479  mgmsscl  13507  plusfvalg  13509  ress0g  13589  imasmnd2  13598  imasmnd  13599  gsumfzz  13641  grpasscan2  13710  grpidrcan  13711  grpidlcan  13712  grpinvadd  13724  grppncan  13737  dfgrp3me  13746  grpsubpropd2  13751  pwsinvg  13758  imasgrp2  13760  imasgrp  13761  mhmmnd  13766  mulgnnsubcl  13784  mulgnn0subcl  13785  mulgsubcl  13786  mulgaddcomlem  13795  mulgaddcom  13796  mulgpropdg  13814  submmulg  13816  subgcl  13834  subgsubcl  13835  subgsub  13836  subgmulg  13838  nsgconj  13856  ghmsub  13901  ghmnsgima  13918  ghmeqker  13921  f1ghm0to0  13922  ablinvadd  13960  ablpncan2  13966  subgabl  13982  rngcl  14021  imasrng  14033  srgcl  14047  ringcl  14090  crngcom  14091  ringidss  14106  ringcom  14108  mulgass2  14135  imasring  14141  opprringbg  14157  unitmulcl  14191  unitmulclb  14192  dvrcl  14213  unitdvcl  14214  dvrcan1  14218  dvrcan3  14219  rhmmul  14242  subrngmcl  14287  subrgmcl  14311  subrgdv  14316  domneq0  14351  islmod  14370  scafvalg  14386  lmodcom  14412  lmodprop2d  14427  rmodislmodlem  14429  rmodislmod  14430  lsselg  14440  lssvnegcl  14455  lspss  14478  lspun  14481  lspsnvsi  14497  lsslsp  14508  sralmod  14529  lidlnegcl  14564  rspssp  14573  rnglidlrng  14577  qus2idrng  14604  zndvds  14728  psrbagcon  14755  basgen  14874  2basgeng  14876  ntrss  14913  neiss  14944  opnneiss  14952  restco  14968  restabs  14969  cnprcl2k  15000  cnpf2  15001  lmconst  15010  cnpnei  15013  cnptoprest  15033  cnmpt2t  15087  psmetsym  15123  psmetge0  15125  xmetge0  15159  xmetsym  15162  blvalps  15182  blval  15183  ssblps  15219  ssbl  15220  blpnfctr  15233  xmssym  15263  bdxmet  15295  metcnp3  15305  dvfvalap  15475  dvid  15489  dvidre  15491  dvcnp2cntop  15493  elplyr  15534  ply1term  15537  plypow  15538  ptolemy  15618  rpcxpadd  15699  rpcxpsub  15702  rpmulcxp  15703  cxpmul  15706  rpcxple2  15712  rpcxplt2  15713  cxpcom  15732  rplogbval  15739  rplogbcl  15740  rplogbchbase  15744  rplogbreexp  15747  relogbexpap  15752  logbleb  15755  logblt  15756  rplogbcxp  15757  rpcxplogb  15758  relogbcxpbap  15759  sgmppw  15789  lgslem1  15802  lgsfvalg  15807  lgsval4  15822  lgsneg  15826  lgsne0  15840  lgsdinn0  15850  lgsquad  15882  funvtxvalg  15960  funiedgvalg  15961  upgrex  16027  uhgr2edg  16130  usgr2v1e2w  16170  subumgredg2en  16195  iedginwlk  16281  upgrwlkedg  16285  clwwlkccat  16325  clwwlknonex2  16363  eulerpathprum  16404  repiecele0  16741  repiecege0  16742  gfsumsn  16797