Theorem simpl3 997

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

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

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 975

This theorem is referenced by:  simpll3  1033  simprl3  1039  simp1l3  1087  simp2l3  1093  simp3l3  1099  3anandirs  1343  frirrg  4335  fcofo  5763  acexmid  5852  rdgon  6365  oawordi  6448  nnmord  6496  nnmword  6497  fidifsnen  6848  dif1en  6857  ac6sfi  6876  difinfsn  7077  enq0tr  7396  distrlem4prl  7546  distrlem4pru  7547  ltaprg  7581  lelttr  8008  ltletr  8009  readdcan  8059  addcan  8099  addcan2  8100  ltadd2  8338  divmulassap  8612  xrlelttr  9763  xrltletr  9764  xaddass  9826  xleadd1a  9830  xlesubadd  9840  icoshftf1o  9948  difelfzle  10090  fzo1fzo0n0  10139  modqmuladdim  10323  modqmuladdnn0  10324  modqm1p1mod0  10331  q2submod  10341  modifeq2int  10342  modqaddmulmod  10347  ltexp2a  10528  exple1  10532  expnlbnd2  10601  nn0ltexp2  10644  nn0leexp2  10645  expcan  10650  fiprsshashgt1  10752  maxleastb  11178  maxltsup  11182  xrltmaxsup  11220  xrmaxltsup  11221  xrmaxaddlem  11223  xrmaxadd  11224  addcn2  11273  mulcn2  11275  isumz  11352  dvdsmodexp  11757  modmulconst  11785  dvdsmod  11822  divalglemex  11881  divalg  11883  gcdass  11970  rplpwr  11982  rppwr  11983  nnwodc  11991  uzwodc  11992  rpmulgcd2  12049  rpdvds  12053  rpexp  12107  znege1  12132  prmdiveq  12190  hashgcdlem  12192  coprimeprodsq  12211  coprimeprodsq2  12212  pythagtriplem3  12221  pcdvdsb  12273  pcgcd1  12281  dvdsprmpweq  12288  pcbc  12303  ctinf  12385  nninfdc  12408  isnsgrp  12647  neiint  12939  topssnei  12956  cnptopco  13016  cnrest2  13030  cnptoprest  13033  upxp  13066  bldisj  13195  blgt0  13196  bl2in  13197  blss2ps  13200  blss2  13201  xblm  13211  blssps  13221  blss  13222  bdmopn  13298  metcnp2  13307  txmetcnp  13312  cncfmptc  13376  dvcnp2cntop  13457  dvcn  13458  logdivlti  13596  ltexp2  13654  lgsfvalg  13700  lgsneg  13719  lgsmod  13721  lgsdilem  13722  lgsdirprm  13729  lgsdir  13730  lgsdi  13732  lgsne0  13733