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  8531  addsubass  8537  nppcan  8549  nppcan3  8551  subcan2  8552  subsub2  8555  subsub4  8560  pnpcan  8566  pnncan  8568  subcan  8582  subdi  8713  ltadd1  8758  leadd1  8759  leadd2  8760  ltsubadd  8761  ltsubadd2  8762  lesubadd  8763  lesubadd2  8764  ltaddsub  8765  leaddsub  8767  lesub1  8785  lesub2  8786  ltsub1  8787  ltsub2  8788  ltaddsublt  8901  gt0add  8903  reapadd1  8926  remulext1  8929  remulext2  8930  apadd2  8939  mulext2  8943  mulap0r  8945  leltap  8955  ltap  8963  apsub1  8972  divap0b  9015  divmulasscomap  9028  divcanap5  9046  dmdcanap  9054  redivclap  9063  div2negap  9067  lt2msq1  9217  ltdiv2  9219  ofnegsub  9294  indfval  9301  ind1  9302  nndivtr  9348  difgtsumgt  9718  zfidc  9727  gtndiv  9745  eluzsub  9961  nn01to3  10026  qdivcl  10052  irrmul  10057  rpgecl  10093  divge1  10134  xaddass  10281  xltadd1  10288  ubioog  10326  ubioc1  10341  lbico1  10342  iccleub  10343  lbicc2  10396  ubicc2  10397  icoshftf1o  10403  fzen  10457  elfz1b  10507  uznfz  10520  elfzo0  10603  elfzo0z  10606  ubmelfzo  10628  fzonn0p1p1  10641  ubmelm1fzo  10654  zsupssdc  10683  qbtwnre  10701  flqwordi  10736  flltdivnn0lt  10752  ceiqle  10763  modqval  10774  modqvalr  10775  modqcl  10776  flqpmodeq  10777  modq0  10779  mulqmod0  10780  negqmod0  10781  modqge0  10782  modqlt  10783  modqdiffl  10785  modqdifz  10786  modqmulnn  10792  modqvalp1  10793  modqabs2  10808  modqmuladdnn0  10818  qnegmod  10819  addmodid  10822  modqeqmodmin  10844  modfzo0difsn  10845  addmodlteq  10848  frec2uzf1od  10856  expnegap0  10997  expgt1  11027  exprecap  11030  expaddzaplem  11032  expaddzap  11033  expmulzap  11035  mulbinom2  11106  expnbnd  11114  fihashss  11271  fimaxq  11284  seq3coll  11308  ccatw2s1leng  11420  ccat2s1fvwd  11429  swrdval  11434  swrdnd  11445  swrdlen2  11448  pfxn0  11474  ccatopth2  11503  s3cl  11572  s3fv0g  11577  s3fv1g  11578  s3fv2g  11579  shftfibg  11599  redivap  11653  imdivap  11660  cjdivap  11689  maxleast  11994  lemininf  12015  ltmininf  12016  bdtrilem  12021  bdtri  12022  xrmaxaddlem  12042  xrmaxadd  12043  xrmineqinf  12051  xrltmininf  12052  xrminltinf  12054  xrminadd  12057  climuni  12075  reccn2ap  12095  isumz  12172  fsumsplitsnun  12202  geoisum1c  12303  prodfap0  12328  prod1dc  12369  fprodabs  12399  cos12dec  12551  summodnegmod  12605  dvdsmultr2  12616  mulmoddvds  12646  divalglemeuneg  12706  gcdaddm  12777  gcdass  12808  mulgcd  12809  gcddiv  12812  nnminle  12828  lcmass  12879  mulgcddvds  12888  qredeq  12890  congr  12894  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  prmexpb  12946  rpexp  12948  pythagtriplem1  13064  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem12  13074  pythagtriplem13  13075  pythagtriplem15  13077  pythagtriplem19  13081  pcdiv  13101  dvdsprmpweqle  13136  sumhashdc  13146  pcbc  13150  4sqlem12  13201  4sqlem18  13207  ballotfilemsgt1  13303  ballotfilemfrcn0  13322  unennn  13337  nninfdc  13393  fvsetsid  13435  ressressg  13478  rngmulrg  13541  imasaddvallemg  13685  qusaddvallemg  13703  mgmsscl  13730  plusfvalg  13732  ress0g  13805  imasmnd2  13808  imasmnd  13809  grpasscan2  13918  grpidrcan  13919  grpidlcan  13920  grpinvadd  13932  grppncan  13945  dfgrp3me  13954  grpsubpropd2  13959  imasgrp2  13962  imasgrp  13963  mhmmnd  13968  mulgnnsubcl  13986  mulgnn0subcl  13987  mulgsubcl  13988  mulgaddcomlem  13997  mulgaddcom  13998  mulgpropdg  14016  submmulg  14018  subgcl  14036  subgsubcl  14037  subgsub  14038  subgmulg  14040  nsgconj  14058  ghmsub  14103  ghmnsgima  14120  ghmeqker  14123  f1ghm0to0  14124  ablinvadd  14163  ablpncan2  14169  subgabl  14185  gsumsncmn  14205  gsumconstcmn  14215  pwsinvg  14264  rngcl  14292  imasrng  14304  rng1zrlem  14307  srgcl  14323  ringcl  14366  crngcom  14367  ringidss  14383  ringcom  14385  mulgass2  14412  imasring  14418  opprringbg  14434  unitmulcl  14469  unitmulclb  14470  dvrcl  14491  unitdvcl  14492  dvrcan1  14496  dvrcan3  14497  rhmmul  14520  subrngmcl  14566  subrgmcl  14590  subrgdv  14595  domneq0  14630  islmod  14676  scafvalg  14693  lmodcom  14719  lmodprop2d  14734  rmodislmodlem  14736  rmodislmod  14737  lsselg  14747  lssvnegcl  14762  lspss  14785  lspun  14788  lspsnvsi  14804  lsslsp  14815  sralmod  14836  lidlnegcl  14871  rspssp  14880  rnglidlrng  14884  qus2idrng  14911  zndvds  15033  aspss  15068  asclmul1  15078  asclmul2  15079  ascldimul  15080  asclinvg  15081  asclmulg  15093  psrbagaddclfi  15110  psrbagcon  15111  basgen  15230  2basgeng  15232  ntrss  15269  neiss  15300  opnneiss  15308  restco  15324  restabs  15325  cnprcl2k  15356  cnpf2  15357  lmconst  15366  cnpnei  15369  cnptoprest  15389  cnmpt2t  15443  psmetsym  15479  psmetge0  15481  xmetge0  15515  xmetsym  15518  blvalps  15538  blval  15539  ssblps  15575  ssbl  15576  blpnfctr  15589  xmssym  15619  bdxmet  15651  metcnp3  15661  dvfvalap  15831  dvid  15845  dvidre  15847  dvcnp2cntop  15849  elplyr  15890  ply1term  15893  plypow  15894  ptolemy  15975  logfac  16048  rpcxpadd  16060  rpcxpsub  16063  rpmulcxp  16064  cxpmul  16067  rpcxple2  16073  rpcxplt2  16074  cxpcom  16093  rplogbval  16100  rplogbcl  16101  rplogbchbase  16105  rplogbreexp  16108  relogbexpap  16113  logbleb  16116  logblt  16117  rplogbcxp  16118  rpcxplogb  16119  relogbcxpbap  16120  ppiqwordi  16174  sgmppw  16187  bcmono  16202  prmefexple  16206  lgslem1  16217  lgsfvalg  16222  lgsval4  16237  lgsneg  16241  lgsne0  16255  lgsdinn0  16265  lgsquad  16297  funvtxvalg  16375  funiedgvalg  16376  upgrex  16442  uhgr2edg  16545  usgr2v1e2w  16585  subumgredg2en  16610  iedginwlk  16696  upgrwlkedg  16700  clwwlkccat  16740  clwwlknonex2  16778  eulerpathprum  16819  dichmul0or  16858  repiecele0  17173  repiecege0  17174