Theorem 3simp2 801

Description: Simplification of triple conjunction.

Assertion

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

Proof of Theorem 3simp2

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

Syntax hints:   -> wi 3   /\ w3a 787

This theorem is referenced by:  3simp2i 804  3simp2d 807  syld3an3 882  3anandis 932  3anandirs 933  nlim0 3084  abianfplem 4019  supmax 4649  nppcan 5466  divcan2 5789  divass 5804  div23 5805  div12 5807  divmuldiv 5838  divdiv23 5850  ltdivmulOLD 5926  ledivmulOLD 5928  lemuldiv 5934  ltdiv23 5952  lediv23 5953  xrmaxlt 5973  xrltmin 5974  maxle 5978  lemin 5981  maxlt 5982  modcyc 6376  modcycOLD 6377  elioo4g 6410  ubicc2 6431  eluzelz 6449  elfzel2i 6505  elfzel2g 6506  eluzfz1 6513  elfz3nn0 6523  expordi 6689  expubnd 6697  bernneq2 6742  fsumshf 7121  fsumcmp 7130  climcmplem 7227  iserzcmp 7232  isummulc1iALT 7303  acdc2lem2 7581  acdc5lem2 7584  clsndisj 7791  cnco 7853  cnpco 7854  methausi 7966  metcnp2 7973  metcni2 7980  tgioolem 7999  lmbrf2 8016  iscau3 8023  iscau4 8025  lmcl 8034  metcnp4 8055  iscms2lem4 8077  grpinvop 8164  grpmuldivass 8172  grppncan 8174  grpnpcan 8175  grpnpncan 8178  ablmuldiv 8191  abldivdiv4 8193  ablnnncan1 8197  ringdi 8230  nvex 8314  nvmdi 8354  nvmul0or 8356  nvsubadd 8359  nvpncan2 8360  nvnncan 8367  nvs 8374  nvdif 8377  nvpi 8378  nvabs 8385  nv1 8388  nvcni 8413  nvcni2 8414  ipval2lem2 8438  ipval2lem5 8444  ssps 8473  lno0 8501  lnomul 8505  nmoge0 8514  nmoubi 8519  nmobndi 8522  nmblore 8530  ipassr 8590  nmopub 9915  nmfnleub 9932  adj2 9941  kbmul 9962  adjlnop 10102  kbass2 10133  hst1a 10229  cdj3lem3a 10450  elo 10530  inposet 10578  truni1 10593  hmeogrp 10632  cnfilca 10670  mslb1 10711  2wsms 10712  msra3 10713  iintlem1 10714  cmpassoh 10811  imonclem 10823  ismonc 10824  icmpmon 10826  iepiclem 10833

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 154  df-an 232  df-3an 789

Copyright terms: Public domain