Theorem simp3 1025

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  simpl3  1028  simpr3  1031  simp3i  1034  simp3d  1037  simp13  1055  simp23  1058  simp33  1061  3anibar  1191  3ianorr  1345  intn3an3d  1394  stoic4a  1476  stoic4b  1477  mob2  2986  sotri2  5134  sotri3  5135  feq123  5474  resasplitss  5516  sefvex  5660  ftpg  5837  fsnunf  5853  fnfvima  5888  cocan1  5927  cocan2  5928  f1oiso2  5967  riotass  6000  moriotass  6001  ovmpox  6149  ovmpoga  6150  fvmpopr2d  6157  caovimo  6215  ofrval  6245  dfsmo2  6452  tfr1onlembfn  6509  tfrcllembfn  6522  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecrdg  6573  nnsucsssuc  6659  f1oen2g  6927  f1dom2g  6928  xpdom3m  7017  mapxpen  7033  diffifi  7082  unfidisj  7113  undifdc  7115  imaf1fi  7124  ssfidc  7129  sbthlemi9  7163  ctssdc  7311  endjudisj  7424  djuassen  7431  xpdjuen  7432  mulcanenq  7604  ltanqg  7619  addnnnq0  7668  nnanq0  7677  prltlu  7706  distrprg  7807  ltexprlemm  7819  recexprlem1ssl  7852  recexprlem1ssu  7853  addsrpr  7964  mulsrpr  7965  mulasssrg  7977  recexgt0sr  7992  ltpsrprg  8022  axmulass  8092  axpre-ltadd  8105  ltxrlt  8244  subadd2  8382  addsubass  8388  nppcan  8400  nppcan3  8402  subcan2  8403  subsub2  8406  subsub4  8411  pnpcan  8417  pnncan  8419  subcan  8433  subdi  8563  ltadd1  8608  leadd1  8609  leadd2  8610  ltsubadd  8611  ltsubadd2  8612  lesubadd  8613  lesubadd2  8614  ltaddsub  8615  leaddsub  8617  lesub1  8635  lesub2  8636  ltsub1  8637  ltsub2  8638  ltaddsublt  8750  gt0add  8752  reapadd1  8775  remulext1  8778  remulext2  8779  apadd2  8788  mulext2  8792  mulap0r  8794  leltap  8804  ltap  8812  apsub1  8821  divap0b  8862  divmulasscomap  8875  divcanap5  8893  dmdcanap  8901  redivclap  8910  div2negap  8914  lt2msq1  9064  ltdiv2  9066  ofnegsub  9141  nndivtr  9184  difgtsumgt  9548  gtndiv  9574  eluzsub  9785  nn01to3  9850  qdivcl  9876  irrmul  9880  rpgecl  9916  divge1  9957  xaddass  10103  xltadd1  10110  ubioog  10148  ubioc1  10163  lbico1  10164  iccleub  10165  lbicc2  10218  ubicc2  10219  icoshftf1o  10225  fzen  10277  elfz1b  10324  uznfz  10337  elfzo0  10420  elfzo0z  10422  ubmelfzo  10444  fzonn0p1p1  10457  ubmelm1fzo  10470  zsupssdc  10497  qbtwnre  10515  flqwordi  10547  flltdivnn0lt  10563  ceiqle  10574  modqval  10585  modqvalr  10586  modqcl  10587  flqpmodeq  10588  modq0  10590  mulqmod0  10591  negqmod0  10592  modqge0  10593  modqlt  10594  modqdiffl  10596  modqdifz  10597  modqmulnn  10603  modqvalp1  10604  modqabs2  10619  modqmuladdnn0  10629  qnegmod  10630  addmodid  10633  modqeqmodmin  10655  modfzo0difsn  10656  addmodlteq  10659  frec2uzf1od  10667  expnegap0  10808  expgt1  10838  exprecap  10841  expaddzaplem  10843  expaddzap  10844  expmulzap  10846  mulbinom2  10917  expnbnd  10924  fihashss  11079  fimaxq  11090  seq3coll  11105  ccatw2s1leng  11214  ccat2s1fvwd  11223  swrdval  11228  swrdnd  11239  swrdlen2  11242  pfxn0  11268  ccatopth2  11297  s3cl  11366  s3fv0g  11371  s3fv1g  11372  s3fv2g  11373  shftfibg  11380  redivap  11434  imdivap  11441  cjdivap  11469  maxleast  11773  lemininf  11794  ltmininf  11795  bdtrilem  11799  bdtri  11800  xrmaxaddlem  11820  xrmaxadd  11821  xrmineqinf  11829  xrltmininf  11830  xrminltinf  11832  xrminadd  11835  climuni  11853  reccn2ap  11873  isumz  11949  fsumsplitsnun  11979  geoisum1c  12080  prodfap0  12105  prod1dc  12146  fprodabs  12176  cos12dec  12328  summodnegmod  12382  dvdsmultr2  12393  mulmoddvds  12423  divalglemeuneg  12483  gcdaddm  12554  gcdass  12585  mulgcd  12586  gcddiv  12589  nnminle  12605  lcmass  12656  mulgcddvds  12665  qredeq  12667  congr  12671  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  prmexpb  12722  rpexp  12724  pythagtriplem1  12837  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem12  12847  pythagtriplem13  12848  pythagtriplem15  12850  pythagtriplem19  12854  pcdiv  12874  dvdsprmpweqle  12909  sumhashdc  12919  pcbc  12923  4sqlem12  12974  4sqlem18  12980  unennn  13017  nninfdc  13073  fvsetsid  13115  ressressg  13157  rngmulrg  13220  imasaddvallemg  13397  qusaddvallemg  13415  mgmsscl  13443  plusfvalg  13445  ress0g  13525  imasmnd2  13534  imasmnd  13535  gsumfzz  13577  grpasscan2  13646  grpidrcan  13647  grpidlcan  13648  grpinvadd  13660  grppncan  13673  dfgrp3me  13682  grpsubpropd2  13687  pwsinvg  13694  imasgrp2  13696  imasgrp  13697  mhmmnd  13702  mulgnnsubcl  13720  mulgnn0subcl  13721  mulgsubcl  13722  mulgaddcomlem  13731  mulgaddcom  13732  mulgpropdg  13750  submmulg  13752  subgcl  13770  subgsubcl  13771  subgsub  13772  subgmulg  13774  nsgconj  13792  ghmsub  13837  ghmnsgima  13854  ghmeqker  13857  f1ghm0to0  13858  ablinvadd  13896  ablpncan2  13902  subgabl  13918  rngcl  13956  imasrng  13968  srgcl  13982  ringcl  14025  crngcom  14026  ringidss  14041  ringcom  14043  mulgass2  14070  imasring  14076  opprringbg  14092  unitmulcl  14126  unitmulclb  14127  dvrcl  14148  unitdvcl  14149  dvrcan1  14153  dvrcan3  14154  rhmmul  14177  subrngmcl  14222  subrgmcl  14246  subrgdv  14251  domneq0  14285  islmod  14304  scafvalg  14320  lmodcom  14346  lmodprop2d  14361  rmodislmodlem  14363  rmodislmod  14364  lsselg  14374  lssvnegcl  14389  lspss  14412  lspun  14415  lspsnvsi  14431  lsslsp  14442  sralmod  14463  lidlnegcl  14498  rspssp  14507  rnglidlrng  14511  qus2idrng  14538  zndvds  14662  basgen  14803  2basgeng  14805  ntrss  14842  neiss  14873  opnneiss  14881  restco  14897  restabs  14898  cnprcl2k  14929  cnpf2  14930  lmconst  14939  cnpnei  14942  cnptoprest  14962  cnmpt2t  15016  psmetsym  15052  psmetge0  15054  xmetge0  15088  xmetsym  15091  blvalps  15111  blval  15112  ssblps  15148  ssbl  15149  blpnfctr  15162  xmssym  15192  bdxmet  15224  metcnp3  15234  dvfvalap  15404  dvid  15418  dvidre  15420  dvcnp2cntop  15422  elplyr  15463  ply1term  15466  plypow  15467  ptolemy  15547  rpcxpadd  15628  rpcxpsub  15631  rpmulcxp  15632  cxpmul  15635  rpcxple2  15641  rpcxplt2  15642  cxpcom  15661  rplogbval  15668  rplogbcl  15669  rplogbchbase  15673  rplogbreexp  15676  relogbexpap  15681  logbleb  15684  logblt  15685  rplogbcxp  15686  rpcxplogb  15687  relogbcxpbap  15688  sgmppw  15715  lgslem1  15728  lgsfvalg  15733  lgsval4  15748  lgsneg  15752  lgsne0  15766  lgsdinn0  15776  lgsquad  15808  funvtxvalg  15886  funiedgvalg  15887  upgrex  15953  uhgr2edg  16056  usgr2v1e2w  16096  subumgredg2en  16121  iedginwlk  16207  upgrwlkedg  16211  clwwlkccat  16251  clwwlknonex2  16289