Theorem simpl3 1028

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

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

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 1006

This theorem is referenced by:  simpll3  1064  simprl3  1070  simp1l3  1118  simp2l3  1124  simp3l3  1130  3anandirs  1384  ifnetruedc  3649  frirrg  4447  fcofo  5925  acexmid  6017  rdgon  6552  oawordi  6637  nnmord  6685  nnmword  6686  1dom1el  6993  fidifsnen  7057  dif1en  7068  ac6sfi  7087  difinfsn  7299  2omotaplemap  7476  enq0tr  7654  distrlem4prl  7804  distrlem4pru  7805  ltaprg  7839  lelttr  8268  ltletr  8269  readdcan  8319  addcan  8359  addcan2  8360  ltadd2  8599  divmulassap  8875  xrlelttr  10041  xrltletr  10042  xaddass  10104  xleadd1a  10108  xlesubadd  10118  icoshftf1o  10226  difelfzle  10369  fzo1fzo0n0  10423  modqmuladdim  10630  modqmuladdnn0  10631  modqm1p1mod0  10638  q2submod  10648  modifeq2int  10649  modqaddmulmod  10654  seq1g  10726  seqp1g  10729  ltexp2a  10854  exple1  10858  expnlbnd2  10928  nn0ltexp2  10972  nn0leexp2  10973  mulsubdivbinom2ap  10974  expcan  10979  fiprsshashgt1  11082  hashtpgim  11110  hashtpg  11112  fun2dmnop0  11115  ccatass  11189  fzowrddc  11232  swrdclg  11235  ccatopth  11301  pfxccatin12lem2a  11312  pfxccat3  11319  maxleastb  11792  maxltsup  11796  xrltmaxsup  11835  xrmaxltsup  11836  xrmaxaddlem  11838  xrmaxadd  11839  addcn2  11888  mulcn2  11890  isumz  11968  dvdsmodexp  12374  modmulconst  12402  dvdsmod  12441  divalglemex  12501  divalg  12503  gcdass  12604  rplpwr  12616  rppwr  12617  nnwodc  12625  uzwodc  12626  rpmulgcd2  12685  rpdvds  12689  rpexp  12743  znege1  12768  prmdiveq  12826  hashgcdlem  12828  coprimeprodsq  12848  coprimeprodsq2  12849  pythagtriplem3  12858  pcdvdsb  12911  pcgcd1  12919  dvdsprmpweq  12926  pcbc  12942  ctinf  13069  nninfdc  13092  isnsgrp  13507  issubmnd  13543  mulgnn0p1  13738  mulgnnsubcl  13739  mulgneg  13745  mulgdirlem  13758  nmzsubg  13815  ghmmulg  13861  ring1eq0  14080  rmodislmod  14384  lspss  14432  2idlcpblrng  14556  neiint  14888  topssnei  14905  cnptopco  14965  cnrest2  14979  cnptoprest  14982  upxp  15015  bldisj  15144  blgt0  15145  bl2in  15146  blss2ps  15149  blss2  15150  xblm  15160  blssps  15170  blss  15171  bdmopn  15247  metcnp2  15256  txmetcnp  15261  cncfmptc  15339  dvcnp2cntop  15442  dvcn  15443  ply1term  15486  dvply1  15508  logdivlti  15624  ltexp2  15684  lgsfvalg  15753  lgsneg  15772  lgsmod  15774  lgsdilem  15775  lgsdirprm  15782  lgsdir  15783  lgsdi  15785  lgsne0  15786  gfsumsn  16737