Theorem simp2 1029

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp2	|- ( ( ph /\ ps /\ ch ) -> ps )

Proof of Theorem simp2

Step	Hyp	Ref	Expression
1		3simpa 1025	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
2	1	simprd 114	1 |- ( ( ph /\ ps /\ ch ) -> ps )

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

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl2  1032  simpr2  1035  simp2i  1038  simp2d  1041  simp12  1059  simp22  1062  simp32  1065  syld3an3  1323  3ianorr  1350  intn3an2d  1398  stoic4b  1482  nlim0  4539  tfisi  4734  sotri2  5185  sotri3  5186  feq123  5525  sefvex  5716  fvmptt  5797  fnfvima  5953  cocan1  5993  cocan2  5994  ovexg  6119  ovmpox  6217  ovmpoga  6218  fvmpopr2d  6225  caovimo  6283  suppval1  6479  suppimacnvfn  6486  suppfnss  6497  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfrcllembxssdm  6627  tfrcllembfn  6628  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecrdg  6679  domssr  7064  mapxpen  7148  dif1en  7183  diffifi  7198  unsnfidcex  7227  unfidisj  7229  undifdc  7231  resfnfinfinss  7253  funrnfi  7256  fissfi  7263  sbthlemi9  7282  elfir  7307  difinfsn  7440  ctssdc  7453  djuassen  7573  xpdjuen  7574  mulcanenq  7752  ltanqg  7767  mulcanenq0ec  7812  addnnnq0  7816  distrprg  7955  aptipr  8008  addsrpr  8112  mulsrpr  8113  mulasssrg  8125  ltpsrprg  8170  axmulass  8240  axpre-ltadd  8253  subadd2  8531  nppcan  8549  nppcan3  8551  subsub2  8555  subsub4  8560  npncan3  8565  pnpcan  8566  pnncan  8568  subcan  8582  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  gt0add  8903  apreap  8917  lemul1  8923  reapmul1lem  8924  reapmul1  8925  reapadd1  8926  remulext1  8929  remulext2  8930  apadd2  8939  mulext2  8943  mulap0r  8945  leltap  8955  ltap  8963  apsub1  8972  recexaplem2  8982  mulcanap  8995  mulcanap2  8996  divvalap  9006  divmulap  9007  divcanap1  9013  diveqap0  9014  divap0b  9015  divrecap  9020  divassap  9022  div23ap  9023  divdirap  9029  divcanap3  9030  div11ap  9032  diveqap1  9037  divmuldivap  9044  divcanap5  9046  redivclap  9063  div2negap  9067  apmul1  9120  apmul2  9121  div2subap  9169  ltdiv1  9200  ledivmul  9209  lemuldiv  9213  lt2msq1  9217  ltdiv23  9224  squeeze0  9236  ofnegsub  9294  ind1  9302  zaddcllemneg  9687  zfidc  9727  eluzsub  9961  nn01to3  10026  rpgecl  10093  addlelt  10179  xleadd1  10287  xltadd1  10288  lbioog  10325  ubioc1  10341  ubicc2  10397  icoshftf1o  10403  fzen  10457  nelfzo  10569  ubmelfzo  10628  ssfzo12  10652  ubmelm1fzo  10654  fzosplitprm1  10663  zsupssdc  10683  rebtwn2zlemshrink  10698  qbtwnre  10701  icogelb  10710  flqwordi  10736  flqword2  10737  flltdivnn0lt  10752  modqcl  10776  mulqmod0  10780  modqmulnn  10792  modqabs2  10808  modqmuladdnn0  10818  qnegmod  10819  addmodid  10822  modqm1p1mod0  10825  modifeq2int  10836  modqdi  10842  modqeqmodmin  10844  modfzo0difsn  10845  frec2uzf1od  10856  exp3val  10991  expnegap0  10997  expgt1  11027  exprecap  11030  expmulzap  11035  leexp2a  11042  expubnd  11046  mulbinom2  11106  bernneq2  11112  expnbnd  11114  fihashss  11271  fihashssdif  11273  fimaxq  11284  ccatval2  11380  ccatass  11390  ccatw2s1leng  11420  ccat2s1fvwd  11429  swrdval  11434  swrdnd  11445  pfxfv  11470  pfxpfx  11494  ccats1pfxeq  11500  ccats1pfxeqrex  11501  s3cl  11572  s3fv0g  11577  s3fv1g  11578  s3fv2g  11579  shftuz  11596  shftfibg  11599  cjdivap  11689  resqrtcl  11809  absdivap  11850  abssubne0  11872  maxleast  11994  lemininf  12015  ltmininf  12016  xrmaxltsup  12040  xrmaxaddlem  12042  xrmaxadd  12043  xrmineqinf  12051  xrltmininf  12052  xrminltinf  12054  xrminadd  12057  climuni  12075  reccn2ap  12095  isumz  12172  geoisum1c  12303  prod1dc  12369  efltim  12481  dvdsval2  12573  dvdscmulr  12603  dvdsmulcr  12604  modmulconst  12606  dvdsadd2b  12623  dvdsexp  12644  mulmoddvds  12646  divalglemeuneg  12706  gcdaddm  12777  dvdsgcdb  12806  mulgcd  12809  gcddiv  12812  uzwodc  12830  lcmdvdsb  12878  mulgcddvds  12888  qredeq  12890  divgcdcoprm0  12895  cncongr1  12897  euclemma  12941  rpexp  12948  rpexp12i  12950  fermltl  13032  prmdiv  13033  odzcllem  13041  odzdvds  13044  odzphi  13045  vfermltl  13050  coprimeprodsq  13056  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem12  13074  pythagtriplem13  13075  pceu  13094  pcdvdsb  13119  pcgcd1  13127  dvdsprmpweq  13134  sumhashdc  13146  ctinf  13370  fvsetsid  13435  ressressg  13478  ressabsg  13479  rngplusgg  13540  imasaddvallemg  13685  qusaddvallemg  13703  plusfvalg  13732  mgmb1mgm1  13737  issubmnd  13804  ress0g  13805  imasmnd2  13808  imasmnd  13809  grpasscan2  13918  grpidrcan  13919  grpidlcan  13920  grpinvadd  13932  grpsubeq0  13940  grppncan  13945  dfgrp3mlem  13952  dfgrp3me  13954  grpsubpropd2  13959  imasgrp2  13962  imasgrp  13963  mhmmnd  13968  mulgnn0p1  13985  mulgnnsubcl  13986  mulgnn0subcl  13987  mulgsubcl  13988  mulgneg  13992  mulgaddcom  13998  mulginvcom  13999  submmulg  14018  subgcl  14036  subgsubcl  14037  subgsub  14038  subgmulg  14040  nsgconj  14058  nsgid  14067  quseccl0g  14083  ghmmulg  14108  ghmeqker  14123  f1ghm0to0  14124  kerf1ghm  14126  ablinvadd  14163  ablsub4  14166  ablpncan2  14169  subgabl  14185  gzsumconst  14192  gsumsncmn  14205  gsumconstcmn  14215  pwsinvg  14264  rngcl  14292  imasrng  14304  srgcl  14323  ringcl  14366  crngcom  14367  ringidss  14383  ringcom  14385  imasring  14418  opprringbg  14434  unitmulcl  14469  unitmulclb  14470  dvrcl  14491  unitdvcl  14492  dvrcan1  14496  dvrcan3  14497  rhmmul  14520  subrngrng  14559  subrngmcl  14566  subrgmcl  14590  subrgdv  14595  rrgeq0  14622  domneq0  14630  islmod  14676  scafvalg  14693  lmodcom  14719  rmodislmodlem  14736  rmodislmod  14737  lssclg  14750  lssvnegcl  14762  lssintclm  14770  lspss  14785  lspun  14788  lspsnvsi  14804  rspssp  14880  rnglidlmmgm  14882  rnglidlmsgrp  14883  rnglidlrng  14884  zndvds  15033  aspss  15068  asclmul1  15078  asclmul2  15079  ascldimul  15080  asclinvg  15081  asclmulg  15093  psrbaglecl  15109  psrbagcon  15111  2basgeng  15232  iuncld  15265  ntrss  15269  restco  15324  restabs  15325  cnprcl2k  15356  lmconst  15366  cnrest2  15386  cnmpt2t  15443  psmetsym  15479  psmetge0  15481  xmetge0  15515  xmetsym  15518  blvalps  15538  blval  15539  xblcntrps  15563  xblcntr  15564  xmssym  15619  blsscls2  15643  bdxmet  15651  txmetcnp  15668  dvfvalap  15831  dvid  15845  dvidre  15847  dvcnp2cntop  15849  elplyr  15890  logfac  16048  rpcxpadd  16060  rpcxpsub  16063  rpmulcxp  16064  rpdivcxp  16066  cxpmul  16067  rpcxple2  16073  rpcxplt2  16074  rplogbval  16100  rplogbcl  16101  rplogbreexp  16108  relogbexpap  16113  logbleb  16116  logblt  16117  rplogbcxp  16118  rpcxplogb  16119  relogbcxpbap  16120  sgmppw  16187  bcmono  16202  prmefexple  16206  lgsneg1  16242  lgsmod  16243  lgsne0  16255  lgssq  16257  lgsdirnn0  16264  lgsdinn0  16265  lgsquad  16297  funvtxvalg  16375  funiedgvalg  16376  lpvtx  16418  ausgrumgrien  16509  ausgrusgrien  16510  uhgrissubgr  16600  egrsubgr  16602  subumgredg2en  16610  subusgr  16614  wlkl1loop  16697  clwwlknonex2  16778  eulerpathprum  16819  eulerpathum  16820  findset  17069  repiecele0  17173  repiecege0  17174