Theorem 3simp2 789

Description: Simplification of triple conjunction.

Assertion

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

Proof of Theorem 3simp2

Step	Hyp	Ref	Expression
1		3simpa 785	. 2 |- ((ph /\ ps /\ ch) -> (ph /\ ps))
2	1	pm3.27d 325	1 |- ((ph /\ ps /\ ch) -> ps)

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  3simp2i 792  3simp2d 795  syld3an3 870  3anandis 920  3anandirs 921  nlim0 3027  abianfplem 3961  supmax 4589  nppcant 5401  divcan2t 5726  div23t 5742  div12t 5744  divmuldivt 5780  divdiv23t 5792  ltdivmultOLD 5868  ledivmultOLD 5869  lemuldivt 5874  ltdiv23t 5892  lediv23t 5893  xrmaxltt 5913  xrltmint 5914  maxlet 5918  lemint 5921  maxltt 5922  elioo4g 6385  ubicc2t 6405  eluzelz 6423  elfzel2 6479  elfzel2g 6480  eluzfz1t 6487  elfz3nn0t 6497  expordit 6600  expubndt 6608  bernneq2 6653  fsumshft 7031  fsumcmp 7040  climcmplem 7137  iserzcmp 7142  isummulc1ALT 7213  acdc2lem2 7489  acdc5lem2 7492  clsndisj 7706  cnco 7768  cnpco 7769  methausi 7881  metcnp2 7888  metcni2 7895  tgioolem 7914  lmbrf2 7931  iscau3 7938  iscau4 7940  lmcl 7949  metcnp4 7970  iscms2lem4 7992  grpinvop 8080  grpmuldivass 8088  grppncan 8090  grpnpcan 8091  grpnpncan 8094  ablmuldiv 8107  abldivdiv4 8109  ablnnncan1 8113  ringdi 8146  nvex 8230  nvmdi 8270  nvmul0or 8272  nvsubadd 8275  nvpncan2 8276  nvnncan 8283  nvs 8290  nvdif 8293  nvpi 8294  nvabs 8301  nv1 8304  nvcni 8329  nvcni2 8330  ipval2lem2 8354  ipval2lem5 8360  ssps 8389  lno0 8417  lnomul 8421  nmoge0 8430  nmoubi 8435  nmobndi 8438  nmblore 8446  ipassr 8506  nmopubt 9832  nmfnleubt 9849  adj2t 9858  kbmult 9879  adjlnopt 10019  kbass2t 10050  hst1t 10145  cdj3lem3a 10366  elo 10444  truni1 10499  hmeogrp 10538  cnfilca 10583  cnfilcaOLD 10584  mslb1 10629  2wsms 10630  msra3 10631  iintlem1 10632  cmpassoh 10729  imonclem 10741  ismonc 10742  icmpmon 10744

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain