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  2881  brcogw  4831  cocan1  5830  oawordi  6522  nnmord  6570  nnmword  6571  dif1en  6935  ac6sfi  6954  ordiso2  7094  difinfsn  7159  ctssdc  7172  2omotaplemap  7317  enq0tr  7494  distrlem4prl  7644  distrlem4pru  7645  ltaprg  7679  aptiprlemu  7700  lelttr  8108  readdcan  8159  addcan  8199  addcan2  8200  ltadd2  8438  ltmul1a  8610  ltmul1  8611  divmulassap  8714  divmulasscomap  8715  lemul1a  8877  xrlelttr  9872  xleadd1a  9939  xlesubadd  9949  icoshftf1o  10057  lincmb01cmp  10069  iccf1o  10070  fztri3or  10105  fzofzim  10255  ioom  10329  modqmuladdim  10438  modqm1p1mod0  10446  q2submod  10456  modqaddmulmod  10462  ltexp2a  10662  exple1  10666  expnlbnd2  10736  nn0ltexp2  10780  nn0leexp2  10781  expcan  10787  fiprsshashgt1  10888  fimaxq  10898  maxleastb  11358  maxltsup  11362  xrltmaxsup  11400  xrmaxltsup  11401  xrmaxaddlem  11403  addcn2  11453  mulcn2  11455  dvdsmodexp  11938  dvdsadd2b  11983  dvdsmod  12004  oexpneg  12018  divalglemex  12063  divalg  12065  gcdass  12152  rplpwr  12164  rppwr  12165  nnwodc  12173  coprmdvds2  12231  rpmulgcd2  12233  qredeq  12234  rpdvds  12237  cncongr2  12242  rpexp  12291  znege1  12316  prmdiveq  12374  hashgcdlem  12376  odzdvds  12383  modprmn0modprm0  12394  coprimeprodsq2  12396  pythagtriplem3  12405  pcdvdsb  12458  pcgcd1  12466  qexpz  12490  pockthg  12495  ctinf  12587  nninfdc  12610  unbendc  12611  isnsgrp  12989  issubmnd  13023  ress0g  13024  mulgneg  13210  mulgdirlem  13223  submmulg  13236  subgmulg  13258  nmzsubg  13280  ghmmulg  13326  srg1zr  13483  ring1eq0  13544  mulgass2  13554  rhmdvdsr  13671  rmodislmodlem  13846  rmodislmod  13847  lssintclm  13880  rnglidlrng  13994  2idlcpblrng  14019  neiint  14313  topssnei  14330  iscnp4  14386  cnptopco  14390  cnconst2  14401  cnrest2  14404  cnptoprest  14407  cnpdis  14410  bldisj  14569  blgt0  14570  bl2in  14571  blss2ps  14574  blss2  14575  xblm  14585  blssps  14595  blss  14596  xmetresbl  14608  bdbl  14671  metcnp3  14679  metcnp2  14681  cncfmptc  14750  dvcnp2cntop  14848  dvcn  14849  logdivlti  15016  ltexp2  15074  lgsfcl2  15122  lgsdilem  15143  lgsdirprm  15150  lgsdir  15151  lgsdi  15153  lgsne0  15154