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  7453  endjudisj  7566  djuassen  7573  xpdjuen  7574  mulcanenq  7752  ltanqg  7767  addnnnq0  7816  nnanq0  7825  prltlu  7854  distrprg  7955  ltexprlemm  7967  recexprlem1ssl  8000  recexprlem1ssu  8001  addsrpr  8112  mulsrpr  8113  mulasssrg  8125  recexgt0sr  8140  ltpsrprg  8170  axmulass  8240  axpre-ltadd  8253  ltxrlt  8391  subadd2  8530  addsubass  8536  nppcan  8548  nppcan3  8550  subcan2  8551  subsub2  8554  subsub4  8559  pnpcan  8565  pnncan  8567  subcan  8581  subdi  8712  ltadd1  8757  leadd1  8758  leadd2  8759  ltsubadd  8760  ltsubadd2  8761  lesubadd  8762  lesubadd2  8763  ltaddsub  8764  leaddsub  8766  lesub1  8784  lesub2  8785  ltsub1  8786  ltsub2  8787  ltaddsublt  8899  gt0add  8901  reapadd1  8924  remulext1  8927  remulext2  8928  apadd2  8937  mulext2  8941  mulap0r  8943  leltap  8953  ltap  8961  apsub1  8970  divap0b  9013  divmulasscomap  9026  divcanap5  9044  dmdcanap  9052  redivclap  9061  div2negap  9065  lt2msq1  9215  ltdiv2  9217  ofnegsub  9292  indfval  9299  ind1  9300  nndivtr  9346  difgtsumgt  9714  zfidc  9723  gtndiv  9741  eluzsub  9952  nn01to3  10017  qdivcl  10043  irrmul  10047  rpgecl  10083  divge1  10124  xaddass  10271  xltadd1  10278  ubioog  10316  ubioc1  10331  lbico1  10332  iccleub  10333  lbicc2  10386  ubicc2  10387  icoshftf1o  10393  fzen  10447  elfz1b  10497  uznfz  10510  elfzo0  10593  elfzo0z  10596  ubmelfzo  10618  fzonn0p1p1  10631  ubmelm1fzo  10644  zsupssdc  10673  qbtwnre  10691  flqwordi  10723  flltdivnn0lt  10739  ceiqle  10750  modqval  10761  modqvalr  10762  modqcl  10763  flqpmodeq  10764  modq0  10766  mulqmod0  10767  negqmod0  10768  modqge0  10769  modqlt  10770  modqdiffl  10772  modqdifz  10773  modqmulnn  10779  modqvalp1  10780  modqabs2  10795  modqmuladdnn0  10805  qnegmod  10806  addmodid  10809  modqeqmodmin  10831  modfzo0difsn  10832  addmodlteq  10835  frec2uzf1od  10843  expnegap0  10984  expgt1  11014  exprecap  11017  expaddzaplem  11019  expaddzap  11020  expmulzap  11022  mulbinom2  11093  expnbnd  11101  fihashss  11257  fimaxq  11270  seq3coll  11294  ccatw2s1leng  11406  ccat2s1fvwd  11415  swrdval  11420  swrdnd  11431  swrdlen2  11434  pfxn0  11460  ccatopth2  11489  s3cl  11558  s3fv0g  11563  s3fv1g  11564  s3fv2g  11565  shftfibg  11585  redivap  11639  imdivap  11646  cjdivap  11675  maxleast  11979  lemininf  12000  ltmininf  12001  bdtrilem  12005  bdtri  12006  xrmaxaddlem  12026  xrmaxadd  12027  xrmineqinf  12035  xrltmininf  12036  xrminltinf  12038  xrminadd  12041  climuni  12059  reccn2ap  12079  isumz  12156  fsumsplitsnun  12186  geoisum1c  12287  prodfap0  12312  prod1dc  12353  fprodabs  12383  cos12dec  12535  summodnegmod  12589  dvdsmultr2  12600  mulmoddvds  12630  divalglemeuneg  12690  gcdaddm  12761  gcdass  12792  mulgcd  12793  gcddiv  12796  nnminle  12812  lcmass  12863  mulgcddvds  12872  qredeq  12874  congr  12878  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  prmexpb  12929  rpexp  12931  pythagtriplem1  13044  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem12  13054  pythagtriplem13  13055  pythagtriplem15  13057  pythagtriplem19  13061  pcdiv  13081  dvdsprmpweqle  13116  sumhashdc  13126  pcbc  13130  4sqlem12  13181  4sqlem18  13187  ballotfilemsgt1  13254  ballotfilemfrcn0  13273  unennn  13288  nninfdc  13344  fvsetsid  13386  ressressg  13429  rngmulrg  13492  imasaddvallemg  13636  qusaddvallemg  13654  mgmsscl  13681  plusfvalg  13683  ress0g  13756  imasmnd2  13759  imasmnd  13760  grpasscan2  13869  grpidrcan  13870  grpidlcan  13871  grpinvadd  13883  grppncan  13896  dfgrp3me  13905  grpsubpropd2  13910  imasgrp2  13913  imasgrp  13914  mhmmnd  13919  mulgnnsubcl  13937  mulgnn0subcl  13938  mulgsubcl  13939  mulgaddcomlem  13948  mulgaddcom  13949  mulgpropdg  13967  submmulg  13969  subgcl  13987  subgsubcl  13988  subgsub  13989  subgmulg  13991  nsgconj  14009  ghmsub  14054  ghmnsgima  14071  ghmeqker  14074  f1ghm0to0  14075  ablinvadd  14114  ablpncan2  14120  subgabl  14136  gsumsncmn  14156  gsumconstcmn  14166  pwsinvg  14215  rngcl  14243  imasrng  14255  rng1zrlem  14258  srgcl  14274  ringcl  14317  crngcom  14318  ringidss  14334  ringcom  14336  mulgass2  14363  imasring  14369  opprringbg  14385  unitmulcl  14420  unitmulclb  14421  dvrcl  14442  unitdvcl  14443  dvrcan1  14447  dvrcan3  14448  rhmmul  14471  subrngmcl  14517  subrgmcl  14541  subrgdv  14546  domneq0  14581  islmod  14627  scafvalg  14644  lmodcom  14670  lmodprop2d  14685  rmodislmodlem  14687  rmodislmod  14688  lsselg  14698  lssvnegcl  14713  lspss  14736  lspun  14739  lspsnvsi  14755  lsslsp  14766  sralmod  14787  lidlnegcl  14822  rspssp  14831  rnglidlrng  14835  qus2idrng  14862  zndvds  14984  aspss  15019  asclmul1  15029  asclmul2  15030  ascldimul  15031  asclinvg  15032  asclmulg  15044  psrbagaddclfi  15061  psrbagcon  15062  basgen  15181  2basgeng  15183  ntrss  15220  neiss  15251  opnneiss  15259  restco  15275  restabs  15276  cnprcl2k  15307  cnpf2  15308  lmconst  15317  cnpnei  15320  cnptoprest  15340  cnmpt2t  15394  psmetsym  15430  psmetge0  15432  xmetge0  15466  xmetsym  15469  blvalps  15489  blval  15490  ssblps  15526  ssbl  15527  blpnfctr  15540  xmssym  15570  bdxmet  15602  metcnp3  15612  dvfvalap  15782  dvid  15796  dvidre  15798  dvcnp2cntop  15800  elplyr  15841  ply1term  15844  plypow  15845  ptolemy  15925  logfac  15995  rpcxpadd  16007  rpcxpsub  16010  rpmulcxp  16011  cxpmul  16014  rpcxple2  16020  rpcxplt2  16021  cxpcom  16040  rplogbval  16047  rplogbcl  16048  rplogbchbase  16052  rplogbreexp  16055  relogbexpap  16060  logbleb  16063  logblt  16064  rplogbcxp  16065  rpcxplogb  16066  relogbcxpbap  16067  sgmppw  16106  lgslem1  16119  lgsfvalg  16124  lgsval4  16139  lgsneg  16143  lgsne0  16157  lgsdinn0  16167  lgsquad  16199  funvtxvalg  16277  funiedgvalg  16278  upgrex  16344  uhgr2edg  16447  usgr2v1e2w  16487  subumgredg2en  16512  iedginwlk  16598  upgrwlkedg  16602  clwwlkccat  16642  clwwlknonex2  16680  eulerpathprum  16721  dichmul0or  16760  repiecele0  17075  repiecege0  17076