Theorem simpl1 990

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simpll1  1026  simprl1  1032  simp1l1  1080  simp2l1  1086  simp3l1  1092  3anandirs  1338  rspc3ev  2846  brcogw  4772  cocan1  5754  oawordi  6433  nnmord  6481  nnmword  6482  dif1en  6841  ac6sfi  6860  ordiso2  6996  difinfsn  7061  ctssdc  7074  enq0tr  7371  distrlem4prl  7521  distrlem4pru  7522  ltaprg  7556  aptiprlemu  7577  lelttr  7983  readdcan  8034  addcan  8074  addcan2  8075  ltadd2  8313  ltmul1a  8485  ltmul1  8486  divmulassap  8587  divmulasscomap  8588  lemul1a  8749  xrlelttr  9738  xleadd1a  9805  xlesubadd  9815  icoshftf1o  9923  lincmb01cmp  9935  iccf1o  9936  fztri3or  9970  fzofzim  10119  ioom  10192  modqmuladdim  10298  modqm1p1mod0  10306  q2submod  10316  modqaddmulmod  10322  ltexp2a  10503  exple1  10507  expnlbnd2  10576  nn0ltexp2  10619  nn0leexp2  10620  expcan  10625  fiprsshashgt1  10726  fimaxq  10736  maxleastb  11152  maxltsup  11156  xrltmaxsup  11194  xrmaxltsup  11195  xrmaxaddlem  11197  addcn2  11247  mulcn2  11249  dvdsmodexp  11731  dvdsadd2b  11776  dvdsmod  11796  oexpneg  11810  divalglemex  11855  divalg  11857  gcdass  11944  rplpwr  11956  rppwr  11957  nnwodc  11965  coprmdvds2  12021  rpmulgcd2  12023  qredeq  12024  rpdvds  12027  cncongr2  12032  rpexp  12081  znege1  12106  prmdiveq  12164  hashgcdlem  12166  odzdvds  12173  modprmn0modprm0  12184  coprimeprodsq2  12186  pythagtriplem3  12195  pcdvdsb  12247  pcgcd1  12255  qexpz  12278  pockthg  12283  ctinf  12359  nninfdc  12382  unbendc  12383  neiint  12745  topssnei  12762  iscnp4  12818  cnptopco  12822  cnconst2  12833  cnrest2  12836  cnptoprest  12839  cnpdis  12842  bldisj  13001  blgt0  13002  bl2in  13003  blss2ps  13006  blss2  13007  xblm  13017  blssps  13027  blss  13028  xmetresbl  13040  bdbl  13103  metcnp3  13111  metcnp2  13113  cncfmptc  13182  dvcnp2cntop  13263  dvcn  13264  logdivlti  13402  ltexp2  13460  lgsfcl2  13507  lgsdilem  13528  lgsdirprm  13535  lgsdir  13536  lgsdi  13538  lgsne0  13539