Theorem simpl3 1002

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  simpll3  1038  simprl3  1044  simp1l3  1092  simp2l3  1098  simp3l3  1104  3anandirs  1348  frirrg  4348  fcofo  5780  acexmid  5869  rdgon  6382  oawordi  6465  nnmord  6513  nnmword  6514  fidifsnen  6865  dif1en  6874  ac6sfi  6893  difinfsn  7094  2omotaplemap  7251  enq0tr  7428  distrlem4prl  7578  distrlem4pru  7579  ltaprg  7613  lelttr  8040  ltletr  8041  readdcan  8091  addcan  8131  addcan2  8132  ltadd2  8370  divmulassap  8646  xrlelttr  9800  xrltletr  9801  xaddass  9863  xleadd1a  9867  xlesubadd  9877  icoshftf1o  9985  difelfzle  10127  fzo1fzo0n0  10176  modqmuladdim  10360  modqmuladdnn0  10361  modqm1p1mod0  10368  q2submod  10378  modifeq2int  10379  modqaddmulmod  10384  ltexp2a  10565  exple1  10569  expnlbnd2  10638  nn0ltexp2  10681  nn0leexp2  10682  expcan  10687  fiprsshashgt1  10788  maxleastb  11214  maxltsup  11218  xrltmaxsup  11256  xrmaxltsup  11257  xrmaxaddlem  11259  xrmaxadd  11260  addcn2  11309  mulcn2  11311  isumz  11388  dvdsmodexp  11793  modmulconst  11821  dvdsmod  11858  divalglemex  11917  divalg  11919  gcdass  12006  rplpwr  12018  rppwr  12019  nnwodc  12027  uzwodc  12028  rpmulgcd2  12085  rpdvds  12089  rpexp  12143  znege1  12168  prmdiveq  12226  hashgcdlem  12228  coprimeprodsq  12247  coprimeprodsq2  12248  pythagtriplem3  12257  pcdvdsb  12309  pcgcd1  12317  dvdsprmpweq  12324  pcbc  12339  ctinf  12421  nninfdc  12444  isnsgrp  12742  issubmnd  12773  mulgnn0p1  12922  mulgnnsubcl  12923  mulgneg  12929  mulgdirlem  12941  ring1eq0  13125  neiint  13427  topssnei  13444  cnptopco  13504  cnrest2  13518  cnptoprest  13521  upxp  13554  bldisj  13683  blgt0  13684  bl2in  13685  blss2ps  13688  blss2  13689  xblm  13699  blssps  13709  blss  13710  bdmopn  13786  metcnp2  13795  txmetcnp  13800  cncfmptc  13864  dvcnp2cntop  13945  dvcn  13946  logdivlti  14084  ltexp2  14142  lgsfvalg  14188  lgsneg  14207  lgsmod  14209  lgsdilem  14210  lgsdirprm  14217  lgsdir  14218  lgsdi  14220  lgsne0  14221