Theorem 3simp3 802

Description: Simplification of triple conjunction.

Assertion

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

Proof of Theorem 3simp3

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

Syntax hints:   -> wi 3   /\ w3a 787

This theorem is referenced by:  3simp3i 805  3simp3d 808  3anandis 932  3anandirs 933  reuuniss 2946  limuni 3086  fiint 4620  ltsopi 5081  nppcan 5466  subdi 5492  divdiv23 5850  lemuldivOLD 5935  ltdiv23 5952  lediv23 5953  xrmaxlt 5973  maxle 5978  maxlt 5982  supxrre 6165  gtndiv 6278  modcyc 6376  modcycOLD 6377  elioore 6411  lbicc2 6430  ubicc2 6431  eluzle 6451  infmssuzle 6491  eluzfz1 6513  fzrev2i 6539  expsub 6687  exple1 6696  caurei 7017  cauimi 7018  fsumcmp 7130  climcmplem 7227  acdc2lem2 7581  acdc5lem2 7584  tgtop11 7723  clsndisj 7791  neiint 7804  neiss 7808  opnneiss 7817  cnco 7853  cnpco 7854  metdnsconst 7986  lmle 8045  iscms2lem4 8077  grpinvop 8164  grpmuldivass 8172  grppncan 8174  grpnpcan 8175  grppnpcan2 8176  grpnpncan 8178  abldivdiv4 8193  ablnnncan 8195  ringdir 8231  nvmul0or 8356  nvsubadd 8359  nvpncan2 8360  nvnncan 8367  nvs 8374  nvdif 8377  nvtri 8382  nvabs 8385  sspn 8479  ipdi 8587  ipsubdi 8593  ssphl 8703  bcs2 9132  shlej1 9438  adj2 9941  hstel2 10230  atcvatlem 10396  lediv2aALT 10456  hmeogrp 10632  hmeobc 10636  filint2 10665  fgsb2 10668  rcfpfillem3 10673  sfvlim 10684  mslb1 10711  msra3 10713  cmpmorp 10794  cmpassoh 10811  iepiclem 10833

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 154  df-an 232  df-3an 789

Copyright terms: Public domain