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  6563  tfr1onlembfn  6620  tfrcllembfn  6633  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecrdg  6684  nnsucsssuc  6770  mapm  6975  f1oen2g  7047  f1dom2g  7048  xpdom3m  7138  mapxpen  7154  diffifi  7204  unfidisj  7235  undifdc  7237  imaf1fi  7246  ssfidc  7251  sbthlemi9  7289  snopfsupp  7306  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  9723  zfidc  9732  gtndiv  9751  eluzsub  9967  nn01to3  10032  qdivcl  10058  irrmul  10063  rpgecl  10099  divge1  10140  xaddass  10287  xltadd1  10294  ubioog  10332  ubioc1  10347  lbico1  10348  iccleub  10349  lbicc2  10402  ubicc2  10403  icoshftf1o  10409  fzen  10463  elfz1b  10513  uznfz  10526  elfzo0  10609  elfzo0z  10612  ubmelfzo  10634  fzonn0p1p1  10647  ubmelm1fzo  10660  zsupssdc  10689  qbtwnre  10707  flqwordi  10743  flltdivnn0lt  10759  ceiqle  10770  modqval  10781  modqvalr  10782  modqcl  10783  flqpmodeq  10784  modq0  10786  mulqmod0  10787  negqmod0  10788  modqge0  10789  modqlt  10790  modqdiffl  10792  modqdifz  10793  modqmulnn  10799  modqvalp1  10800  modqabs2  10815  modqmuladdnn0  10825  qnegmod  10826  addmodid  10829  modqeqmodmin  10851  modfzo0difsn  10852  addmodlteq  10855  frec2uzf1od  10863  expnegap0  11004  expgt1  11034  exprecap  11037  expaddzaplem  11039  expaddzap  11040  expmulzap  11042  mulbinom2  11113  expnbnd  11121  fihashss  11278  fimaxq  11291  seq3coll  11315  ccatw2s1leng  11427  ccat2s1fvwd  11436  swrdval  11441  swrdnd  11452  swrdlen2  11455  pfxn0  11481  ccatopth2  11510  s3cl  11579  s3fv0g  11584  s3fv1g  11585  s3fv2g  11586  shftfibg  11606  redivap  11660  imdivap  11667  cjdivap  11696  maxleast  12001  lemininf  12023  ltmininf  12024  bdtrilem  12029  bdtri  12030  xrmaxaddlem  12050  xrmaxadd  12051  xrmineqinf  12059  xrltmininf  12060  xrminltinf  12062  xrminadd  12065  climuni  12083  reccn2ap  12103  isumz  12180  fsumsplitsnun  12210  geoisum1c  12311  prodfap0  12336  prod1dc  12377  fprodabs  12407  cos12dec  12559  summodnegmod  12613  dvdsmultr2  12624  mulmoddvds  12654  divalglemeuneg  12714  gcdaddm  12785  gcdass  12816  mulgcd  12817  gcddiv  12820  nnminle  12836  lcmass  12887  mulgcddvds  12896  qredeq  12898  congr  12902  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  prmexpb  12954  rpexp  12956  pythagtriplem1  13072  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem12  13082  pythagtriplem13  13083  pythagtriplem15  13085  pythagtriplem19  13089  pcdiv  13109  dvdsprmpweqle  13144  sumhashdc  13154  pcbc  13158  4sqlem12  13209  4sqlem18  13215  ballotfilemsgt1  13311  ballotfilemfrcn0  13330  unennn  13345  nninfdc  13401  fvsetsid  13443  ressressg  13487  rngmulrg  13550  imasaddvallemg  13694  qusaddvallemg  13712  mgmsscl  13739  plusfvalg  13741  ress0g  13814  imasmnd2  13817  imasmnd  13818  grpasscan2  13927  grpidrcan  13928  grpidlcan  13929  grpinvadd  13941  grppncan  13954  dfgrp3me  13963  grpsubpropd2  13968  imasgrp2  13971  imasgrp  13972  mhmmnd  13977  mulgnnsubcl  13995  mulgnn0subcl  13996  mulgsubcl  13997  mulgaddcomlem  14006  mulgaddcom  14007  mulgpropdg  14025  submmulg  14027  subgcl  14045  subgsubcl  14046  subgsub  14047  subgmulg  14049  nsgconj  14067  ghmsub  14112  ghmnsgima  14129  ghmeqker  14132  f1ghm0to0  14133  ablinvadd  14203  ablpncan2  14209  subgabl  14225  gsumsncmn  14245  gsumconstcmn  14265  pwsinvg  14321  rngcl  14349  imasrng  14361  rng1zrlem  14364  srgcl  14380  ringcl  14423  crngcom  14424  ringidss  14440  ringcom  14442  mulgass2  14469  imasring  14477  opprringbg  14493  unitmulcl  14528  unitmulclb  14529  dvrcl  14550  unitdvcl  14551  dvrcan1  14555  dvrcan3  14556  rhmmul  14579  subrngmcl  14625  subrgmcl  14649  subrgdv  14654  domneq0  14689  islmod  14735  scafvalg  14752  lmodcom  14778  lmodprop2d  14793  rmodislmodlem  14795  rmodislmod  14796  lsselg  14806  lssvnegcl  14821  lspss  14844  lspun  14847  lspsnvsi  14863  lsslsp  14874  sralmod  14895  lidlnegcl  14930  rspssp  14939  rnglidlrng  14943  qus2idrng  14970  zndvds  15092  aspss  15127  asclmul1  15137  asclmul2  15138  ascldimul  15139  asclinvg  15140  asclmulg  15152  psrbagdceq  15167  psrbagaddclfi  15173  psrbagcon  15174  psrringfi  15213  mvrf1fi  15219  basgen  15323  2basgeng  15325  ntrss  15362  neiss  15393  opnneiss  15401  restco  15417  restabs  15418  cnprcl2k  15449  cnpf2  15450  lmconst  15459  cnpnei  15462  cnptoprest  15482  cnmpt2t  15536  psmetsym  15572  psmetge0  15574  xmetge0  15608  xmetsym  15611  blvalps  15631  blval  15632  ssblps  15668  ssbl  15669  blpnfctr  15682  xmssym  15712  bdxmet  15744  metcnp3  15754  dvfvalap  15924  dvid  15938  dvidre  15940  dvcnp2cntop  15942  elplyr  15983  ply1term  15986  plypow  15987  ptolemy  16068  logfac  16143  rpcxpadd  16155  rpcxpsub  16158  rpmulcxp  16159  cxpmul  16162  rpcxple2  16170  rpcxplt2  16171  cxpcom  16190  efnthr  16193  rplogbval  16198  rplogbcl  16199  rplogbchbase  16203  rplogbreexp  16206  relogbexpap  16211  logbleb  16214  logblt  16215  rplogbcxp  16216  rpcxplogb  16217  relogbcxpbap  16218  chtqwordi  16280  ppiqwordi  16285  sgmppw  16303  bcmono  16321  prmefexple  16325  lgslem1  16341  lgsfvalg  16346  lgsval4  16361  lgsneg  16365  lgsne0  16379  lgsdinn0  16389  lgsquad  16421  funvtxvalg  16499  funiedgvalg  16500  upgrex  16566  uhgr2edg  16669  usgr2v1e2w  16709  subumgredg2en  16734  iedginwlk  16820  upgrwlkedg  16824  clwwlkccat  16864  clwwlknonex2  16902  eulerpathprum  16943  dichmul0or  16982  repiecele0  17298  repiecege0  17299