Theorem 3simp2 788

Description: Simplification of triple conjunction.

Assertion

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

Proof of Theorem 3simp2

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

Syntax hints:   -> wi 3   /\ w3a 774

This theorem is referenced by:  3simp2i 791  3simp2d 794  syl3dan3 869  3anandis 918  3anandirs 919  nlim0 3022  abianfplem 3952  supmax 4569  npncant 5380  nppcant 5381  ppncant 5461  div23t 5713  div12t 5715  divmuldivt 5744  divdiv23t 5756  ltdivmult 5827  ledivmult 5828  ltdiv23t 5848  lediv23t 5849  xrmaxltt 5869  xrltmint 5870  maxlet 5874  lemint 5877  maxltt 5878  elioo4g 6326  ubicc2t 6346  eluzelz 6363  elfzel2 6419  elfzel2g 6420  eluzfz1t 6427  elfz3nn0t 6437  expordit 6539  expubndt 6547  bernneq2 6592  fsumshft 6977  fsumcmp 6986  climcmplem 7081  iserzcmp 7086  isummulc1ALT 7156  acdc2lem2 7439  acdc5lem2 7442  clsndisj 7656  cnco 7718  cnpco 7719  methausi 7833  metcnp2 7840  metcni2 7847  tgioolem 7866  lmbrf2 7883  iscau3 7890  iscau4 7892  lmcl 7900  metcnp4 7920  iscms2lem4 7942  grpinvop 8030  grpmuldivass 8038  grppncan 8040  grpnpcan 8041  grpnpncan 8044  ablmuldiv 8059  abldivdiv4 8061  ablnnncan1 8065  ringdi 8098  nvex 8182  nvmdi 8222  nvmul0or 8224  nvsubadd 8227  nvpncan2 8228  nvnncan 8235  nvs 8242  nvdif 8245  nvpi 8246  nvabs 8253  nv1 8256  nvcni 8279  ipval2lem2 8301  ipval2lem5 8307  ssps 8336  lno0 8364  lnomul 8367  nmoge0 8375  nmoubi 8380  nmobndi 8383  nmblore 8391  ipassr 8450  nmopubt 9772  nmfnleubt 9788  adj2t 9797  kbmult 9818  adjlnopt 9957  kbass2t 9988  hst1t 10083  cdj3lem3a 10300  elo 10381  truni1 10422  hmeogrp 10461  cnfilca 10487  mslb1 10509  2wsms 10510  msra3 10511  iintlem1 10512  cmpassoh 10609  imonclem 10619  ismonc 10620  icmpmon 10623

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 776

Copyright terms: Public domain