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  1360  rspc3ev  2893  brcogw  4846  cocan1  5855  oawordi  6554  nnmord  6602  nnmword  6603  dif1en  6975  ac6sfi  6994  ordiso2  7136  difinfsn  7201  ctssdc  7214  2omotaplemap  7368  enq0tr  7546  distrlem4prl  7696  distrlem4pru  7697  ltaprg  7731  aptiprlemu  7752  lelttr  8160  readdcan  8211  addcan  8251  addcan2  8252  ltadd2  8491  ltmul1a  8663  ltmul1  8664  divmulassap  8767  divmulasscomap  8768  lemul1a  8930  xrlelttr  9927  xleadd1a  9994  xlesubadd  10004  icoshftf1o  10112  lincmb01cmp  10124  iccf1o  10125  fztri3or  10160  fzofzim  10310  ioom  10401  modqmuladdim  10510  modqm1p1mod0  10518  q2submod  10528  modqaddmulmod  10534  ltexp2a  10734  exple1  10738  expnlbnd2  10808  nn0ltexp2  10852  nn0leexp2  10853  expcan  10859  fiprsshashgt1  10960  fimaxq  10970  fun2dmnop0  10990  ccatass  11062  maxleastb  11496  maxltsup  11500  xrltmaxsup  11539  xrmaxltsup  11540  xrmaxaddlem  11542  addcn2  11592  mulcn2  11594  dvdsmodexp  12077  dvdsadd2b  12122  dvdsmod  12144  oexpneg  12159  divalglemex  12204  divalg  12206  gcdass  12307  rplpwr  12319  rppwr  12320  nnwodc  12328  coprmdvds2  12386  rpmulgcd2  12388  qredeq  12389  rpdvds  12392  cncongr2  12397  rpexp  12446  znege1  12471  prmdiveq  12529  hashgcdlem  12531  odzdvds  12539  modprmn0modprm0  12550  coprimeprodsq2  12552  pythagtriplem3  12561  pcdvdsb  12614  pcgcd1  12622  qexpz  12646  pockthg  12651  ctinf  12772  nninfdc  12795  unbendc  12796  isnsgrp  13209  issubmnd  13245  ress0g  13246  mulgneg  13447  mulgdirlem  13460  submmulg  13473  subgmulg  13495  nmzsubg  13517  ghmmulg  13563  srg1zr  13720  ring1eq0  13781  mulgass2  13791  rhmdvdsr  13908  rmodislmodlem  14083  rmodislmod  14084  lssintclm  14117  rnglidlrng  14231  2idlcpblrng  14256  neiint  14588  topssnei  14605  iscnp4  14661  cnptopco  14665  cnconst2  14676  cnrest2  14679  cnptoprest  14682  cnpdis  14685  bldisj  14844  blgt0  14845  bl2in  14846  blss2ps  14849  blss2  14850  xblm  14860  blssps  14870  blss  14871  xmetresbl  14883  bdbl  14946  metcnp3  14954  metcnp2  14956  cncfmptc  15039  dvcnp2cntop  15142  dvcn  15143  logdivlti  15324  ltexp2  15384  lgsfcl2  15454  lgsdilem  15475  lgsdirprm  15482  lgsdir  15483  lgsdi  15485  lgsne0  15486