Theorem simpl3 969

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpl3	|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )

Proof of Theorem simpl3

Step	Hyp	Ref	Expression
1		simp3 966	. 2 |- ( ( ph /\ ps /\ ch ) -> ch )
2	1	adantr 272	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 945

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  simpll3  1005  simprl3  1011  simp1l3  1059  simp2l3  1065  simp3l3  1071  3anandirs  1309  frirrg  4232  fcofo  5639  acexmid  5727  rdgon  6237  oawordi  6319  nnmord  6367  nnmword  6368  fidifsnen  6717  dif1en  6726  ac6sfi  6745  difinfsn  6937  enq0tr  7190  distrlem4prl  7340  distrlem4pru  7341  ltaprg  7375  lelttr  7775  ltletr  7776  readdcan  7825  addcan  7865  addcan2  7866  ltadd2  8100  divmulassap  8368  xrlelttr  9482  xrltletr  9483  xaddass  9545  xleadd1a  9549  xlesubadd  9559  icoshftf1o  9667  difelfzle  9804  fzo1fzo0n0  9853  modqmuladdim  10033  modqmuladdnn0  10034  modqm1p1mod0  10041  q2submod  10051  modifeq2int  10052  modqaddmulmod  10057  ltexp2a  10238  exple1  10242  expnlbnd2  10310  expcan  10356  fiprsshashgt1  10456  maxleastb  10878  maxltsup  10882  xrltmaxsup  10918  xrmaxltsup  10919  xrmaxaddlem  10921  xrmaxadd  10922  addcn2  10971  mulcn2  10973  isumz  11050  modmulconst  11373  dvdsmod  11408  divalglemex  11467  divalg  11469  gcdass  11549  rplpwr  11561  rppwr  11562  rpmulgcd2  11622  rpdvds  11626  rpexp  11677  znege1  11701  hashgcdlem  11748  ctinf  11788  neiint  12157  topssnei  12174  cnptopco  12233  cnrest2  12247  cnptoprest  12250  upxp  12283  bldisj  12390  blgt0  12391  bl2in  12392  blss2ps  12395  blss2  12396  xblm  12406  blssps  12416  blss  12417  bdmopn  12493  metcnp2  12502  txmetcnp  12507  cncfmptc  12568  dvcnp2cntop  12618  dvcn  12619