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  2882  brcogw  4832  cocan1  5831  oawordi  6524  nnmord  6572  nnmword  6573  dif1en  6937  ac6sfi  6956  ordiso2  7096  difinfsn  7161  ctssdc  7174  2omotaplemap  7319  enq0tr  7496  distrlem4prl  7646  distrlem4pru  7647  ltaprg  7681  aptiprlemu  7702  lelttr  8110  readdcan  8161  addcan  8201  addcan2  8202  ltadd2  8440  ltmul1a  8612  ltmul1  8613  divmulassap  8716  divmulasscomap  8717  lemul1a  8879  xrlelttr  9875  xleadd1a  9942  xlesubadd  9952  icoshftf1o  10060  lincmb01cmp  10072  iccf1o  10073  fztri3or  10108  fzofzim  10258  ioom  10332  modqmuladdim  10441  modqm1p1mod0  10449  q2submod  10459  modqaddmulmod  10465  ltexp2a  10665  exple1  10669  expnlbnd2  10739  nn0ltexp2  10783  nn0leexp2  10784  expcan  10790  fiprsshashgt1  10891  fimaxq  10901  maxleastb  11361  maxltsup  11365  xrltmaxsup  11403  xrmaxltsup  11404  xrmaxaddlem  11406  addcn2  11456  mulcn2  11458  dvdsmodexp  11941  dvdsadd2b  11986  dvdsmod  12007  oexpneg  12021  divalglemex  12066  divalg  12068  gcdass  12155  rplpwr  12167  rppwr  12168  nnwodc  12176  coprmdvds2  12234  rpmulgcd2  12236  qredeq  12237  rpdvds  12240  cncongr2  12245  rpexp  12294  znege1  12319  prmdiveq  12377  hashgcdlem  12379  odzdvds  12386  modprmn0modprm0  12397  coprimeprodsq2  12399  pythagtriplem3  12408  pcdvdsb  12461  pcgcd1  12469  qexpz  12493  pockthg  12498  ctinf  12590  nninfdc  12613  unbendc  12614  isnsgrp  12992  issubmnd  13026  ress0g  13027  mulgneg  13213  mulgdirlem  13226  submmulg  13239  subgmulg  13261  nmzsubg  13283  ghmmulg  13329  srg1zr  13486  ring1eq0  13547  mulgass2  13557  rhmdvdsr  13674  rmodislmodlem  13849  rmodislmod  13850  lssintclm  13883  rnglidlrng  13997  2idlcpblrng  14022  neiint  14324  topssnei  14341  iscnp4  14397  cnptopco  14401  cnconst2  14412  cnrest2  14415  cnptoprest  14418  cnpdis  14421  bldisj  14580  blgt0  14581  bl2in  14582  blss2ps  14585  blss2  14586  xblm  14596  blssps  14606  blss  14607  xmetresbl  14619  bdbl  14682  metcnp3  14690  metcnp2  14692  cncfmptc  14775  dvcnp2cntop  14878  dvcn  14879  logdivlti  15057  ltexp2  15115  lgsfcl2  15163  lgsdilem  15184  lgsdirprm  15191  lgsdir  15192  lgsdi  15194  lgsne0  15195