Theorem 3simp3 790

Description: Simplification of triple conjunction.

Assertion

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

Proof of Theorem 3simp3

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

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  3simp3i 793  3simp3d 796  3anandis 920  3anandirs 921  reuuniss 2889  limuni 3029  fiint 4559  fiintOLD 4560  ltsopi 5016  nppcant 5401  subdit 5427  divdiv23t 5792  lemuldivtOLD 5875  ltdiv23t 5892  lediv23t 5893  xrmaxltt 5913  maxlet 5918  maxltt 5922  supxrre 6083  gtndivt 6193  eliooret 6386  lbicc2t 6404  ubicc2t 6405  eluzle 6425  infmssuzle 6465  eluzfz1t 6487  fzrev2it 6513  expsubt 6598  exple1t 6607  caure 6927  cauim 6928  fsumcmp 7040  climcmplem 7137  acdc2lem2 7489  acdc5lem2 7492  tgtop11t 7634  clsndisj 7706  neiint 7719  neiss 7723  opnneiss 7732  cnco 7768  cnpco 7769  metdnsconst 7901  lmle 7960  iscms2lem4 7992  grpinvop 8080  grpmuldivass 8088  grppncan 8090  grpnpcan 8091  grppnpcan2 8092  grpnpncan 8094  abldivdiv4 8109  ablnnncan 8111  ringdir 8147  nvmul0or 8272  nvsubadd 8275  nvpncan2 8276  nvnncan 8283  nvs 8290  nvdif 8293  nvtri 8298  nvabs 8301  sspn 8395  ipdi 8503  ipsubdi 8509  ssphl 8619  spwpr3OLD 8662  bcs2t 9049  shlej1t 9355  adj2t 9858  hstel2t 10146  atcvatlem 10312  lediv2itALT 10371  hmeogrp 10538  hmeobc 10542  filint2 10574  filint2OLD 10575  fgsb2 10580  rcfpfillem3 10589  rcfpfillem3OLD 10590  sfvlim 10605  mslb1 10629  msra3 10631  cmpmorp 10712  cmpassoh 10729

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