Theorem simpl1 1000

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

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

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 980

This theorem is referenced by:  simpll1  1036  simprl1  1042  simp1l1  1090  simp2l1  1096  simp3l1  1102  3anandirs  1348  rspc3ev  2859  brcogw  4797  cocan1  5788  oawordi  6470  nnmord  6518  nnmword  6519  dif1en  6879  ac6sfi  6898  ordiso2  7034  difinfsn  7099  ctssdc  7112  2omotaplemap  7256  enq0tr  7433  distrlem4prl  7583  distrlem4pru  7584  ltaprg  7618  aptiprlemu  7639  lelttr  8046  readdcan  8097  addcan  8137  addcan2  8138  ltadd2  8376  ltmul1a  8548  ltmul1  8549  divmulassap  8652  divmulasscomap  8653  lemul1a  8815  xrlelttr  9806  xleadd1a  9873  xlesubadd  9883  icoshftf1o  9991  lincmb01cmp  10003  iccf1o  10004  fztri3or  10039  fzofzim  10188  ioom  10261  modqmuladdim  10367  modqm1p1mod0  10375  q2submod  10385  modqaddmulmod  10391  ltexp2a  10572  exple1  10576  expnlbnd2  10646  nn0ltexp2  10689  nn0leexp2  10690  expcan  10696  fiprsshashgt1  10797  fimaxq  10807  maxleastb  11223  maxltsup  11227  xrltmaxsup  11265  xrmaxltsup  11266  xrmaxaddlem  11268  addcn2  11318  mulcn2  11320  dvdsmodexp  11802  dvdsadd2b  11847  dvdsmod  11868  oexpneg  11882  divalglemex  11927  divalg  11929  gcdass  12016  rplpwr  12028  rppwr  12029  nnwodc  12037  coprmdvds2  12093  rpmulgcd2  12095  qredeq  12096  rpdvds  12099  cncongr2  12104  rpexp  12153  znege1  12178  prmdiveq  12236  hashgcdlem  12238  odzdvds  12245  modprmn0modprm0  12256  coprimeprodsq2  12258  pythagtriplem3  12267  pcdvdsb  12319  pcgcd1  12327  qexpz  12350  pockthg  12355  ctinf  12431  nninfdc  12454  unbendc  12455  isnsgrp  12812  issubmnd  12843  ress0g  12844  mulgneg  13001  mulgdirlem  13014  subgmulg  13048  nmzsubg  13070  srg1zr  13170  ring1eq0  13225  mulgass2  13235  rmodislmodlem  13440  rmodislmod  13441  neiint  13648  topssnei  13665  iscnp4  13721  cnptopco  13725  cnconst2  13736  cnrest2  13739  cnptoprest  13742  cnpdis  13745  bldisj  13904  blgt0  13905  bl2in  13906  blss2ps  13909  blss2  13910  xblm  13920  blssps  13930  blss  13931  xmetresbl  13943  bdbl  14006  metcnp3  14014  metcnp2  14016  cncfmptc  14085  dvcnp2cntop  14166  dvcn  14167  logdivlti  14305  ltexp2  14363  lgsfcl2  14410  lgsdilem  14431  lgsdirprm  14438  lgsdir  14439  lgsdi  14441  lgsne0  14442