Theorem 3simp3 788

Description: Simplification of triple conjunction.

Assertion

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

Proof of Theorem 3simp3

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

Syntax hints:   -> wi 3   /\ w3a 773

This theorem is referenced by:  3simp3i 791  3simp3d 794  3anandis 917  3anandirs 918  reuuniss 2879  limuni 3019  fiint 4534  ltsopi 4988  npncant 5372  nppcant 5373  subdit 5399  ppncant 5453  divdiv23t 5748  lemuldivt 5824  ltdiv23t 5840  lediv23t 5841  xrmaxltt 5861  maxlet 5866  maxltt 5870  supxrre 6030  gtndivt 6140  lbicc2t 6337  ubicc2t 6338  eluzle 6357  infmssuzle 6397  eluzfz1t 6419  fzrev2it 6445  expsubt 6529  exple1t 6538  caure 6864  cauim 6865  fsumcmp 6978  climcmplem 7073  acdc2lem2 7431  acdc5lem2 7434  tgtop11t 7576  clsndisj 7648  neiint 7660  neiss 7664  opnneiss 7673  cnco 7707  cnpco 7708  metdnsconst 7840  lmle 7895  iscms2lem4 7926  grpinvop 8015  grpmuldivass 8023  grppncan 8025  grpnpcan 8026  grppnpcan2 8027  grpnpncan 8029  abldivdiv4 8046  ablnnncan 8048  ringdir 8084  nvmul0or 8212  nvsubadd 8215  nvpncan2 8216  nvnncan 8223  nvs 8229  nvdif 8232  nvtri 8237  nvabs 8240  sspn 8329  ipdi 8434  ipsubdi 8440  ssphl 8549  bcs2t 8970  shlej1t 9270  adj2t 9774  hstel2t 10056  atcvatlem 10220  lediv2itALT 10276  hmeogrp 10425  filint2 10446  fgsb2 10449  mslb1 10473  msra3 10475  cmpmorp 10556  cmpassoh 10573

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 775

Copyright terms: Public domain