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  4351  fcofo  5785  acexmid  5874  rdgon  6387  oawordi  6470  nnmord  6518  nnmword  6519  fidifsnen  6870  dif1en  6879  ac6sfi  6898  difinfsn  7099  2omotaplemap  7256  enq0tr  7433  distrlem4prl  7583  distrlem4pru  7584  ltaprg  7618  lelttr  8046  ltletr  8047  readdcan  8097  addcan  8137  addcan2  8138  ltadd2  8376  divmulassap  8652  xrlelttr  9806  xrltletr  9807  xaddass  9869  xleadd1a  9873  xlesubadd  9883  icoshftf1o  9991  difelfzle  10134  fzo1fzo0n0  10183  modqmuladdim  10367  modqmuladdnn0  10368  modqm1p1mod0  10375  q2submod  10385  modifeq2int  10386  modqaddmulmod  10391  ltexp2a  10572  exple1  10576  expnlbnd2  10646  nn0ltexp2  10689  nn0leexp2  10690  mulsubdivbinom2ap  10691  expcan  10696  fiprsshashgt1  10797  maxleastb  11223  maxltsup  11227  xrltmaxsup  11265  xrmaxltsup  11266  xrmaxaddlem  11268  xrmaxadd  11269  addcn2  11318  mulcn2  11320  isumz  11397  dvdsmodexp  11802  modmulconst  11830  dvdsmod  11868  divalglemex  11927  divalg  11929  gcdass  12016  rplpwr  12028  rppwr  12029  nnwodc  12037  uzwodc  12038  rpmulgcd2  12095  rpdvds  12099  rpexp  12153  znege1  12178  prmdiveq  12236  hashgcdlem  12238  coprimeprodsq  12257  coprimeprodsq2  12258  pythagtriplem3  12267  pcdvdsb  12319  pcgcd1  12327  dvdsprmpweq  12334  pcbc  12349  ctinf  12431  nninfdc  12454  isnsgrp  12812  issubmnd  12843  mulgnn0p1  12994  mulgnnsubcl  12995  mulgneg  13001  mulgdirlem  13014  nmzsubg  13070  ring1eq0  13225  rmodislmod  13441  neiint  13648  topssnei  13665  cnptopco  13725  cnrest2  13739  cnptoprest  13742  upxp  13775  bldisj  13904  blgt0  13905  bl2in  13906  blss2ps  13909  blss2  13910  xblm  13920  blssps  13930  blss  13931  bdmopn  14007  metcnp2  14016  txmetcnp  14021  cncfmptc  14085  dvcnp2cntop  14166  dvcn  14167  logdivlti  14305  ltexp2  14363  lgsfvalg  14409  lgsneg  14428  lgsmod  14430  lgsdilem  14431  lgsdirprm  14438  lgsdir  14439  lgsdi  14441  lgsne0  14442