Theorem simpl1 985

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

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

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 965

This theorem is referenced by:  simpll1  1021  simprl1  1027  simp1l1  1075  simp2l1  1081  simp3l1  1087  3anandirs  1330  rspc3ev  2833  brcogw  4752  cocan1  5732  oawordi  6409  nnmord  6457  nnmword  6458  dif1en  6817  ac6sfi  6836  ordiso2  6969  difinfsn  7034  ctssdc  7047  enq0tr  7337  distrlem4prl  7487  distrlem4pru  7488  ltaprg  7522  aptiprlemu  7543  lelttr  7948  readdcan  7998  addcan  8038  addcan2  8039  ltadd2  8277  ltmul1a  8449  ltmul1  8450  divmulassap  8551  divmulasscomap  8552  lemul1a  8712  xrlelttr  9692  xleadd1a  9759  xlesubadd  9769  icoshftf1o  9877  lincmb01cmp  9889  iccf1o  9890  fztri3or  9923  fzofzim  10069  ioom  10142  modqmuladdim  10248  modqm1p1mod0  10256  q2submod  10266  modqaddmulmod  10272  ltexp2a  10453  exple1  10457  expnlbnd2  10525  expcan  10572  fiprsshashgt1  10673  fimaxq  10683  maxleastb  11096  maxltsup  11100  xrltmaxsup  11136  xrmaxltsup  11137  xrmaxaddlem  11139  addcn2  11189  mulcn2  11191  dvdsmodexp  11673  dvdsadd2b  11715  dvdsmod  11735  oexpneg  11749  divalglemex  11794  divalg  11796  gcdass  11879  rplpwr  11891  rppwr  11892  coprmdvds2  11950  rpmulgcd2  11952  qredeq  11953  rpdvds  11956  cncongr2  11961  rpexp  12007  znege1  12032  prmdiveq  12088  hashgcdlem  12090  ctinf  12131  neiint  12505  topssnei  12522  iscnp4  12578  cnptopco  12582  cnconst2  12593  cnrest2  12596  cnptoprest  12599  cnpdis  12602  bldisj  12761  blgt0  12762  bl2in  12763  blss2ps  12766  blss2  12767  xblm  12777  blssps  12787  blss  12788  xmetresbl  12800  bdbl  12863  metcnp3  12871  metcnp2  12873  cncfmptc  12942  dvcnp2cntop  13023  dvcn  13024  logdivlti  13162