Theorem simpl1 1002

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpl1	|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simp1 999	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2	1	adantr 276	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )

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

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

This theorem is referenced by:  simpll1  1038  simprl1  1044  simp1l1  1092  simp2l1  1098  simp3l1  1104  3anandirs  1359  rspc3ev  2885  brcogw  4835  cocan1  5834  oawordi  6527  nnmord  6575  nnmword  6576  dif1en  6940  ac6sfi  6959  ordiso2  7101  difinfsn  7166  ctssdc  7179  2omotaplemap  7324  enq0tr  7501  distrlem4prl  7651  distrlem4pru  7652  ltaprg  7686  aptiprlemu  7707  lelttr  8115  readdcan  8166  addcan  8206  addcan2  8207  ltadd2  8446  ltmul1a  8618  ltmul1  8619  divmulassap  8722  divmulasscomap  8723  lemul1a  8885  xrlelttr  9881  xleadd1a  9948  xlesubadd  9958  icoshftf1o  10066  lincmb01cmp  10078  iccf1o  10079  fztri3or  10114  fzofzim  10264  ioom  10350  modqmuladdim  10459  modqm1p1mod0  10467  q2submod  10477  modqaddmulmod  10483  ltexp2a  10683  exple1  10687  expnlbnd2  10757  nn0ltexp2  10801  nn0leexp2  10802  expcan  10808  fiprsshashgt1  10909  fimaxq  10919  maxleastb  11379  maxltsup  11383  xrltmaxsup  11422  xrmaxltsup  11423  xrmaxaddlem  11425  addcn2  11475  mulcn2  11477  dvdsmodexp  11960  dvdsadd2b  12005  dvdsmod  12027  oexpneg  12042  divalglemex  12087  divalg  12089  gcdass  12182  rplpwr  12194  rppwr  12195  nnwodc  12203  coprmdvds2  12261  rpmulgcd2  12263  qredeq  12264  rpdvds  12267  cncongr2  12272  rpexp  12321  znege1  12346  prmdiveq  12404  hashgcdlem  12406  odzdvds  12414  modprmn0modprm0  12425  coprimeprodsq2  12427  pythagtriplem3  12436  pcdvdsb  12489  pcgcd1  12497  qexpz  12521  pockthg  12526  ctinf  12647  nninfdc  12670  unbendc  12671  isnsgrp  13049  issubmnd  13083  ress0g  13084  mulgneg  13270  mulgdirlem  13283  submmulg  13296  subgmulg  13318  nmzsubg  13340  ghmmulg  13386  srg1zr  13543  ring1eq0  13604  mulgass2  13614  rhmdvdsr  13731  rmodislmodlem  13906  rmodislmod  13907  lssintclm  13940  rnglidlrng  14054  2idlcpblrng  14079  neiint  14381  topssnei  14398  iscnp4  14454  cnptopco  14458  cnconst2  14469  cnrest2  14472  cnptoprest  14475  cnpdis  14478  bldisj  14637  blgt0  14638  bl2in  14639  blss2ps  14642  blss2  14643  xblm  14653  blssps  14663  blss  14664  xmetresbl  14676  bdbl  14739  metcnp3  14747  metcnp2  14749  cncfmptc  14832  dvcnp2cntop  14935  dvcn  14936  logdivlti  15117  ltexp2  15177  lgsfcl2  15247  lgsdilem  15268  lgsdirprm  15275  lgsdir  15276  lgsdi  15278  lgsne0  15279