Theorem 3simp3 792

Description: Simplification of triple conjunction.

Assertion

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

Proof of Theorem 3simp3

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

Syntax hints:   -> wi 3   /\ w3a 777

This theorem is referenced by:  3simp3i 795  3simp3d 798  3anandis 922  3anandirs 923  reuuniss 2895  limuni 3035  fiint 4572  fiintOLD 4573  ltsopi 5028  nppcant 5413  subdit 5439  divdiv23t 5794  lemuldivtOLD 5877  ltdiv23t 5894  lediv23t 5895  xrmaxltt 5915  maxlet 5920  maxltt 5924  supxrre 6085  gtndivt 6195  eliooret 6387  lbicc2t 6405  ubicc2t 6406  eluzle 6426  infmssuzle 6466  eluzfz1t 6488  fzrev2it 6514  expsubt 6599  exple1t 6608  caure 6927  cauim 6928  fsumcmp 7040  climcmplem 7137  acdc2lem2 7490  acdc5lem2 7493  tgtop11t 7633  clsndisj 7703  neiint 7716  neiss 7720  opnneiss 7729  cnco 7765  cnpco 7766  metdnsconst 7898  lmle 7957  iscms2lem4 7989  grpinvop 8076  grpmuldivass 8084  grppncan 8086  grpnpcan 8087  grppnpcan2 8088  grpnpncan 8090  abldivdiv4 8105  ablnnncan 8107  ringdir 8143  nvmul0or 8268  nvsubadd 8271  nvpncan2 8272  nvnncan 8279  nvs 8286  nvdif 8289  nvtri 8294  nvabs 8297  sspn 8391  ipdi 8499  ipsubdi 8505  ssphl 8615  bcs2t 9044  shlej1t 9350  adj2t 9853  hstel2t 10141  atcvatlem 10307  lediv2itALT 10366  hmeogrp 10524  hmeobc 10528  filint2 10557  fgsb2 10560  rcfpfillem3 10565  sfvlim 10576  mslb1 10600  msra3 10602  cmpmorp 10683  cmpassoh 10700

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