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  5188  sotri3  5189  feq123  5528  resasplitss  5572  fresaunres2disj  5573  sefvex  5719  ftpg  5902  fsnunf  5918  fnfvima  5956  cocan1  5996  cocan2  5997  f1oiso2  6036  riotass  6071  moriotass  6072  ovmpox  6220  ovmpoga  6221  fvmpopr2d  6228  caovimo  6286  ofrval  6317  suppvalfn  6485  fvn0elsuppb  6496  dfsmo2  6562  tfr1onlembfn  6619  tfrcllembfn  6632  freccllem  6677  frecfcllem  6679  frecsuclem  6681  frecrdg  6683  nnsucsssuc  6769  f1oen2g  7045  f1dom2g  7046  xpdom3m  7136  mapxpen  7152  diffifi  7202  unfidisj  7233  undifdc  7235  imaf1fi  7244  ssfidc  7249  sbthlemi9  7287  fdcf1  7321  ctssdc  7459  endjudisj  7572  djuassen  7579  xpdjuen  7580  mulcanenq  7758  ltanqg  7773  addnnnq0  7822  nnanq0  7831  prltlu  7860  distrprg  7961  ltexprlemm  7973  recexprlem1ssl  8006  recexprlem1ssu  8007  addsrpr  8118  mulsrpr  8119  mulasssrg  8131  recexgt0sr  8146  ltpsrprg  8176  axmulass  8246  axpre-ltadd  8259  ltxrlt  8397  subadd2  8537  addsubass  8543  nppcan  8555  nppcan3  8557  subcan2  8558  subsub2  8561  subsub4  8566  pnpcan  8572  pnncan  8574  subcan  8588  subdi  8719  ltadd1  8764  leadd1  8765  leadd2  8766  ltsubadd  8767  ltsubadd2  8768  lesubadd  8769  lesubadd2  8770  ltaddsub  8771  leaddsub  8773  lesub1  8791  lesub2  8792  ltsub1  8793  ltsub2  8794  ltaddsublt  8907  gt0add  8909  reapadd1  8932  remulext1  8935  remulext2  8936  apadd2  8945  mulext2  8949  mulap0r  8951  leltap  8961  ltap  8969  apsub1  8978  divap0b  9021  divmulasscomap  9034  divcanap5  9052  dmdcanap  9060  redivclap  9069  div2negap  9073  lt2msq1  9223  ltdiv2  9225  ofsubeq0  9300  ofnegsub  9301  indfval  9308  ind1  9309  nndivtr  9355  difgtsumgt  9725  zfidc  9734  gtndiv  9752  eluzsub  9968  nn01to3  10033  qdivcl  10059  irrmul  10064  rpgecl  10100  divge1  10141  xaddass  10288  xltadd1  10295  ubioog  10333  ubioc1  10348  lbico1  10349  iccleub  10350  lbicc2  10403  ubicc2  10404  icoshftf1o  10410  fzen  10464  elfz1b  10514  uznfz  10527  elfzo0  10610  elfzo0z  10613  ubmelfzo  10635  fzonn0p1p1  10648  ubmelm1fzo  10661  zsupssdc  10690  qbtwnre  10708  flqwordi  10744  flltdivnn0lt  10760  ceiqle  10771  modqval  10782  modqvalr  10783  modqcl  10784  flqpmodeq  10785  modq0  10787  mulqmod0  10788  negqmod0  10789  modqge0  10790  modqlt  10791  modqdiffl  10793  modqdifz  10794  modqmulnn  10800  modqvalp1  10801  modqabs2  10816  modqmuladdnn0  10826  qnegmod  10827  addmodid  10830  modqeqmodmin  10852  modfzo0difsn  10853  addmodlteq  10856  frec2uzf1od  10864  expnegap0  11005  expgt1  11035  exprecap  11038  expaddzaplem  11040  expaddzap  11041  expmulzap  11043  mulbinom2  11114  expnbnd  11122  fihashss  11279  fimaxq  11292  seq3coll  11316  ccatw2s1leng  11428  ccat2s1fvwd  11437  swrdval  11442  swrdnd  11453  swrdlen2  11456  pfxn0  11482  ccatopth2  11511  s3cl  11580  s3fv0g  11585  s3fv1g  11586  s3fv2g  11587  shftfibg  11607  redivap  11661  imdivap  11668  cjdivap  11697  maxleast  12002  lemininf  12024  ltmininf  12025  bdtrilem  12030  bdtri  12031  xrmaxaddlem  12051  xrmaxadd  12052  xrmineqinf  12060  xrltmininf  12061  xrminltinf  12063  xrminadd  12066  climuni  12084  reccn2ap  12104  isumz  12181  fsumsplitsnun  12211  geoisum1c  12312  prodfap0  12337  prod1dc  12378  fprodabs  12408  cos12dec  12560  summodnegmod  12614  dvdsmultr2  12625  mulmoddvds  12655  divalglemeuneg  12715  gcdaddm  12786  gcdass  12817  mulgcd  12818  gcddiv  12821  nnminle  12837  lcmass  12888  mulgcddvds  12897  qredeq  12899  congr  12903  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  prmexpb  12955  rpexp  12957  pythagtriplem1  13073  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem12  13083  pythagtriplem13  13084  pythagtriplem15  13086  pythagtriplem19  13090  pcdiv  13110  dvdsprmpweqle  13145  sumhashdc  13155  pcbc  13159  4sqlem12  13210  4sqlem18  13216  ballotfilemsgt1  13312  ballotfilemfrcn0  13331  unennn  13346  nninfdc  13402  fvsetsid  13444  ressressg  13488  rngmulrg  13551  imasaddvallemg  13695  qusaddvallemg  13713  mgmsscl  13740  plusfvalg  13742  ress0g  13815  imasmnd2  13818  imasmnd  13819  grpasscan2  13928  grpidrcan  13929  grpidlcan  13930  grpinvadd  13942  grppncan  13955  dfgrp3me  13964  grpsubpropd2  13969  imasgrp2  13972  imasgrp  13973  mhmmnd  13978  mulgnnsubcl  13996  mulgnn0subcl  13997  mulgsubcl  13998  mulgaddcomlem  14007  mulgaddcom  14008  mulgpropdg  14026  submmulg  14028  subgcl  14046  subgsubcl  14047  subgsub  14048  subgmulg  14050  nsgconj  14068  ghmsub  14113  ghmnsgima  14130  ghmeqker  14133  f1ghm0to0  14134  ablinvadd  14204  ablpncan2  14210  subgabl  14226  gsumsncmn  14246  gsumconstcmn  14266  pwsinvg  14322  rngcl  14350  imasrng  14362  rng1zrlem  14365  srgcl  14381  ringcl  14424  crngcom  14425  ringidss  14441  ringcom  14443  mulgass2  14470  imasring  14478  opprringbg  14494  unitmulcl  14529  unitmulclb  14530  dvrcl  14551  unitdvcl  14552  dvrcan1  14556  dvrcan3  14557  rhmmul  14580  subrngmcl  14626  subrgmcl  14650  subrgdv  14655  domneq0  14690  islmod  14736  scafvalg  14753  lmodcom  14779  lmodprop2d  14794  rmodislmodlem  14796  rmodislmod  14797  lsselg  14807  lssvnegcl  14822  lspss  14845  lspun  14848  lspsnvsi  14864  lsslsp  14875  sralmod  14896  lidlnegcl  14931  rspssp  14940  rnglidlrng  14944  qus2idrng  14971  zndvds  15093  aspss  15128  asclmul1  15138  asclmul2  15139  ascldimul  15140  asclinvg  15141  asclmulg  15153  psrbagaddclfi  15170  psrbagcon  15171  psrringfi  15204  basgen  15306  2basgeng  15308  ntrss  15345  neiss  15376  opnneiss  15384  restco  15400  restabs  15401  cnprcl2k  15432  cnpf2  15433  lmconst  15442  cnpnei  15445  cnptoprest  15465  cnmpt2t  15519  psmetsym  15555  psmetge0  15557  xmetge0  15591  xmetsym  15594  blvalps  15614  blval  15615  ssblps  15651  ssbl  15652  blpnfctr  15665  xmssym  15695  bdxmet  15727  metcnp3  15737  dvfvalap  15907  dvid  15921  dvidre  15923  dvcnp2cntop  15925  elplyr  15966  ply1term  15969  plypow  15970  ptolemy  16051  logfac  16126  rpcxpadd  16138  rpcxpsub  16141  rpmulcxp  16142  cxpmul  16145  rpcxple2  16153  rpcxplt2  16154  cxpcom  16173  efnthr  16176  rplogbval  16181  rplogbcl  16182  rplogbchbase  16186  rplogbreexp  16189  relogbexpap  16194  logbleb  16197  logblt  16198  rplogbcxp  16199  rpcxplogb  16200  relogbcxpbap  16201  chtqwordi  16263  ppiqwordi  16268  sgmppw  16286  bcmono  16304  prmefexple  16308  lgslem1  16324  lgsfvalg  16329  lgsval4  16344  lgsneg  16348  lgsne0  16362  lgsdinn0  16372  lgsquad  16404  funvtxvalg  16482  funiedgvalg  16483  upgrex  16549  uhgr2edg  16652  usgr2v1e2w  16692  subumgredg2en  16717  iedginwlk  16803  upgrwlkedg  16807  clwwlkccat  16847  clwwlknonex2  16885  eulerpathprum  16926  dichmul0or  16965  repiecele0  17281  repiecege0  17282