Theorem simpl3 986

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

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

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

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

This theorem is referenced by:  simpll3  1022  simprl3  1028  simp1l3  1076  simp2l3  1082  simp3l3  1088  3anandirs  1326  frirrg  4272  fcofo  5685  acexmid  5773  rdgon  6283  oawordi  6365  nnmord  6413  nnmword  6414  fidifsnen  6764  dif1en  6773  ac6sfi  6792  difinfsn  6985  enq0tr  7242  distrlem4prl  7392  distrlem4pru  7393  ltaprg  7427  lelttr  7852  ltletr  7853  readdcan  7902  addcan  7942  addcan2  7943  ltadd2  8181  divmulassap  8455  xrlelttr  9589  xrltletr  9590  xaddass  9652  xleadd1a  9656  xlesubadd  9666  icoshftf1o  9774  difelfzle  9911  fzo1fzo0n0  9960  modqmuladdim  10140  modqmuladdnn0  10141  modqm1p1mod0  10148  q2submod  10158  modifeq2int  10159  modqaddmulmod  10164  ltexp2a  10345  exple1  10349  expnlbnd2  10417  expcan  10463  fiprsshashgt1  10563  maxleastb  10986  maxltsup  10990  xrltmaxsup  11026  xrmaxltsup  11027  xrmaxaddlem  11029  xrmaxadd  11030  addcn2  11079  mulcn2  11081  isumz  11158  modmulconst  11525  dvdsmod  11560  divalglemex  11619  divalg  11621  gcdass  11703  rplpwr  11715  rppwr  11716  rpmulgcd2  11776  rpdvds  11780  rpexp  11831  znege1  11856  hashgcdlem  11903  ctinf  11943  neiint  12314  topssnei  12331  cnptopco  12391  cnrest2  12405  cnptoprest  12408  upxp  12441  bldisj  12570  blgt0  12571  bl2in  12572  blss2ps  12575  blss2  12576  xblm  12586  blssps  12596  blss  12597  bdmopn  12673  metcnp2  12682  txmetcnp  12687  cncfmptc  12751  dvcnp2cntop  12832  dvcn  12833