Theorem simpl3 944

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 941	. 2 |- ( ( ph /\ ps /\ ch ) -> ch )
2	1	adantr 270	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  simpll3  980  simprl3  986  simp1l3  1034  simp2l3  1040  simp3l3  1046  3anandirs  1280  frirrg  4113  fcofo  5455  acexmid  5542  rdgon  6035  oawordi  6113  nnmord  6156  nnmword  6157  fidifsnen  6405  dif1en  6414  ac6sfi  6431  enq0tr  6686  distrlem4prl  6836  distrlem4pru  6837  ltaprg  6871  lelttr  7266  ltletr  7267  readdcan  7315  addcan  7355  addcan2  7356  ltadd2  7590  divmulassap  7850  xrlelttr  8952  xrltletr  8953  icoshftf1o  9089  difelfzle  9222  fzo1fzo0n0  9269  modqmuladdim  9449  modqmuladdnn0  9450  modqm1p1mod0  9457  q2submod  9467  modifeq2int  9468  modqaddmulmod  9473  ltexp2a  9625  exple1  9629  expnlbnd2  9695  expcan  9741  maxleastb  10238  maxltsup  10242  addcn2  10287  mulcn2  10289  modmulconst  10372  dvdsmod  10407  divalglemex  10466  divalg  10468  gcdass  10548  rplpwr  10560  rppwr  10561  rpmulgcd2  10621  rpdvds  10625  rpexp  10676  znege1  10700