Theorem simpl1 1003

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

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

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 983

This theorem is referenced by:  simpll1  1039  simprl1  1045  simp1l1  1093  simp2l1  1099  simp3l1  1105  3anandirs  1361  rspc3ev  2894  brcogw  4847  cocan1  5856  oawordi  6555  nnmord  6603  nnmword  6604  dif1en  6976  ac6sfi  6995  ordiso2  7137  difinfsn  7202  ctssdc  7215  2omotaplemap  7369  enq0tr  7547  distrlem4prl  7697  distrlem4pru  7698  ltaprg  7732  aptiprlemu  7753  lelttr  8161  readdcan  8212  addcan  8252  addcan2  8253  ltadd2  8492  ltmul1a  8664  ltmul1  8665  divmulassap  8768  divmulasscomap  8769  lemul1a  8931  xrlelttr  9928  xleadd1a  9995  xlesubadd  10005  icoshftf1o  10113  lincmb01cmp  10125  iccf1o  10126  fztri3or  10161  fzofzim  10312  ioom  10403  modqmuladdim  10512  modqm1p1mod0  10520  q2submod  10530  modqaddmulmod  10536  ltexp2a  10736  exple1  10740  expnlbnd2  10810  nn0ltexp2  10854  nn0leexp2  10855  expcan  10861  fiprsshashgt1  10962  fimaxq  10972  fun2dmnop0  10992  ccatass  11064  swrdlen  11105  swrdfv  11106  maxleastb  11525  maxltsup  11529  xrltmaxsup  11568  xrmaxltsup  11569  xrmaxaddlem  11571  addcn2  11621  mulcn2  11623  dvdsmodexp  12106  dvdsadd2b  12151  dvdsmod  12173  oexpneg  12188  divalglemex  12233  divalg  12235  gcdass  12336  rplpwr  12348  rppwr  12349  nnwodc  12357  coprmdvds2  12415  rpmulgcd2  12417  qredeq  12418  rpdvds  12421  cncongr2  12426  rpexp  12475  znege1  12500  prmdiveq  12558  hashgcdlem  12560  odzdvds  12568  modprmn0modprm0  12579  coprimeprodsq2  12581  pythagtriplem3  12590  pcdvdsb  12643  pcgcd1  12651  qexpz  12675  pockthg  12680  ctinf  12801  nninfdc  12824  unbendc  12825  isnsgrp  13238  issubmnd  13274  ress0g  13275  mulgneg  13476  mulgdirlem  13489  submmulg  13502  subgmulg  13524  nmzsubg  13546  ghmmulg  13592  srg1zr  13749  ring1eq0  13810  mulgass2  13820  rhmdvdsr  13937  rmodislmodlem  14112  rmodislmod  14113  lssintclm  14146  rnglidlrng  14260  2idlcpblrng  14285  neiint  14617  topssnei  14634  iscnp4  14690  cnptopco  14694  cnconst2  14705  cnrest2  14708  cnptoprest  14711  cnpdis  14714  bldisj  14873  blgt0  14874  bl2in  14875  blss2ps  14878  blss2  14879  xblm  14889  blssps  14899  blss  14900  xmetresbl  14912  bdbl  14975  metcnp3  14983  metcnp2  14985  cncfmptc  15068  dvcnp2cntop  15171  dvcn  15172  logdivlti  15353  ltexp2  15413  lgsfcl2  15483  lgsdilem  15504  lgsdirprm  15511  lgsdir  15512  lgsdi  15514  lgsne0  15515