Theorem 3simp2 791

Description: Simplification of triple conjunction.

Assertion

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

Proof of Theorem 3simp2

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

Syntax hints:   -> wi 3   /\ w3a 777

This theorem is referenced by:  3simp2i 794  3simp2d 797  syld3an3 872  3anandis 922  3anandirs 923  nlim0 3033  abianfplem 3967  supmax 4598  nppcant 5413  divcan2t 5733  div23t 5749  div12t 5751  divmuldivt 5782  divdiv23t 5794  ltdivmultOLD 5870  ledivmultOLD 5871  lemuldivt 5876  ltdiv23t 5894  lediv23t 5895  xrmaxltt 5915  xrltmint 5916  maxlet 5920  lemint 5923  maxltt 5924  elioo4g 6386  ubicc2t 6406  eluzelz 6424  elfzel2 6480  elfzel2g 6481  eluzfz1t 6488  elfz3nn0t 6498  expordit 6601  expubndt 6609  bernneq2 6654  fsumshft 7031  fsumcmp 7040  climcmplem 7137  iserzcmp 7142  isummulc1ALT 7213  acdc2lem2 7490  acdc5lem2 7493  clsndisj 7703  cnco 7765  cnpco 7766  methausi 7878  metcnp2 7885  metcni2 7892  tgioolem 7911  lmbrf2 7928  iscau3 7935  iscau4 7937  lmcl 7946  metcnp4 7967  iscms2lem4 7989  grpinvop 8076  grpmuldivass 8084  grppncan 8086  grpnpcan 8087  grpnpncan 8090  ablmuldiv 8103  abldivdiv4 8105  ablnnncan1 8109  ringdi 8142  nvex 8226  nvmdi 8266  nvmul0or 8268  nvsubadd 8271  nvpncan2 8272  nvnncan 8279  nvs 8286  nvdif 8289  nvpi 8290  nvabs 8297  nv1 8300  nvcni 8325  nvcni2 8326  ipval2lem2 8350  ipval2lem5 8356  ssps 8385  lno0 8413  lnomul 8417  nmoge0 8426  nmoubi 8431  nmobndi 8434  nmblore 8442  ipassr 8502  nmopubt 9827  nmfnleubt 9844  adj2t 9853  kbmult 9874  adjlnopt 10014  kbass2t 10045  hst1t 10140  cdj3lem3a 10361  elo 10439  inposet 10477  truni1 10485  hmeogrp 10524  cnfilca 10562  mslb1 10600  2wsms 10601  msra3 10602  iintlem1 10603  cmpassoh 10700  imonclem 10712  ismonc 10713  icmpmon 10715

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 779

Copyright terms: Public domain