Theorem simpl3 1004

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

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

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 982

This theorem is referenced by:  simpll3  1040  simprl3  1046  simp1l3  1094  simp2l3  1100  simp3l3  1106  3anandirs  1359  ifnetruedc  3602  frirrg  4385  fcofo  5831  acexmid  5921  rdgon  6444  oawordi  6527  nnmord  6575  nnmword  6576  fidifsnen  6931  dif1en  6940  ac6sfi  6959  difinfsn  7166  2omotaplemap  7324  enq0tr  7501  distrlem4prl  7651  distrlem4pru  7652  ltaprg  7686  lelttr  8115  ltletr  8116  readdcan  8166  addcan  8206  addcan2  8207  ltadd2  8446  divmulassap  8722  xrlelttr  9881  xrltletr  9882  xaddass  9944  xleadd1a  9948  xlesubadd  9958  icoshftf1o  10066  difelfzle  10209  fzo1fzo0n0  10259  modqmuladdim  10459  modqmuladdnn0  10460  modqm1p1mod0  10467  q2submod  10477  modifeq2int  10478  modqaddmulmod  10483  seq1g  10555  seqp1g  10558  ltexp2a  10683  exple1  10687  expnlbnd2  10757  nn0ltexp2  10801  nn0leexp2  10802  mulsubdivbinom2ap  10803  expcan  10808  fiprsshashgt1  10909  maxleastb  11379  maxltsup  11383  xrltmaxsup  11422  xrmaxltsup  11423  xrmaxaddlem  11425  xrmaxadd  11426  addcn2  11475  mulcn2  11477  isumz  11554  dvdsmodexp  11960  modmulconst  11988  dvdsmod  12027  divalglemex  12087  divalg  12089  gcdass  12182  rplpwr  12194  rppwr  12195  nnwodc  12203  uzwodc  12204  rpmulgcd2  12263  rpdvds  12267  rpexp  12321  znege1  12346  prmdiveq  12404  hashgcdlem  12406  coprimeprodsq  12426  coprimeprodsq2  12427  pythagtriplem3  12436  pcdvdsb  12489  pcgcd1  12497  dvdsprmpweq  12504  pcbc  12520  ctinf  12647  nninfdc  12670  isnsgrp  13049  issubmnd  13083  mulgnn0p1  13263  mulgnnsubcl  13264  mulgneg  13270  mulgdirlem  13283  nmzsubg  13340  ghmmulg  13386  ring1eq0  13604  rmodislmod  13907  lspss  13955  2idlcpblrng  14079  neiint  14381  topssnei  14398  cnptopco  14458  cnrest2  14472  cnptoprest  14475  upxp  14508  bldisj  14637  blgt0  14638  bl2in  14639  blss2ps  14642  blss2  14643  xblm  14653  blssps  14663  blss  14664  bdmopn  14740  metcnp2  14749  txmetcnp  14754  cncfmptc  14832  dvcnp2cntop  14935  dvcn  14936  ply1term  14979  dvply1  15001  logdivlti  15117  ltexp2  15177  lgsfvalg  15246  lgsneg  15265  lgsmod  15267  lgsdilem  15268  lgsdirprm  15275  lgsdir  15276  lgsdi  15278  lgsne0  15279  1dom1el  15637