Theorem simpl3 992

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

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

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 970

This theorem is referenced by:  simpll3  1028  simprl3  1034  simp1l3  1082  simp2l3  1088  simp3l3  1094  3anandirs  1338  frirrg  4328  fcofo  5752  acexmid  5841  rdgon  6354  oawordi  6437  nnmord  6485  nnmword  6486  fidifsnen  6836  dif1en  6845  ac6sfi  6864  difinfsn  7065  enq0tr  7375  distrlem4prl  7525  distrlem4pru  7526  ltaprg  7560  lelttr  7987  ltletr  7988  readdcan  8038  addcan  8078  addcan2  8079  ltadd2  8317  divmulassap  8591  xrlelttr  9742  xrltletr  9743  xaddass  9805  xleadd1a  9809  xlesubadd  9819  icoshftf1o  9927  difelfzle  10069  fzo1fzo0n0  10118  modqmuladdim  10302  modqmuladdnn0  10303  modqm1p1mod0  10310  q2submod  10320  modifeq2int  10321  modqaddmulmod  10326  ltexp2a  10507  exple1  10511  expnlbnd2  10580  nn0ltexp2  10623  nn0leexp2  10624  expcan  10629  fiprsshashgt1  10730  maxleastb  11156  maxltsup  11160  xrltmaxsup  11198  xrmaxltsup  11199  xrmaxaddlem  11201  xrmaxadd  11202  addcn2  11251  mulcn2  11253  isumz  11330  dvdsmodexp  11735  modmulconst  11763  dvdsmod  11800  divalglemex  11859  divalg  11861  gcdass  11948  rplpwr  11960  rppwr  11961  nnwodc  11969  uzwodc  11970  rpmulgcd2  12027  rpdvds  12031  rpexp  12085  znege1  12110  prmdiveq  12168  hashgcdlem  12170  coprimeprodsq  12189  coprimeprodsq2  12190  pythagtriplem3  12199  pcdvdsb  12251  pcgcd1  12259  dvdsprmpweq  12266  pcbc  12281  ctinf  12363  nninfdc  12386  neiint  12785  topssnei  12802  cnptopco  12862  cnrest2  12876  cnptoprest  12879  upxp  12912  bldisj  13041  blgt0  13042  bl2in  13043  blss2ps  13046  blss2  13047  xblm  13057  blssps  13067  blss  13068  bdmopn  13144  metcnp2  13153  txmetcnp  13158  cncfmptc  13222  dvcnp2cntop  13303  dvcn  13304  logdivlti  13442  ltexp2  13500  lgsfvalg  13546  lgsneg  13565  lgsmod  13567  lgsdilem  13568  lgsdirprm  13575  lgsdir  13576  lgsdi  13578  lgsne0  13579