Theorem simpl1 984

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

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

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 964

This theorem is referenced by:  simpll1  1020  simprl1  1026  simp1l1  1074  simp2l1  1080  simp3l1  1086  3anandirs  1326  rspc3ev  2806  brcogw  4708  cocan1  5688  oawordi  6365  nnmord  6413  nnmword  6414  dif1en  6773  ac6sfi  6792  ordiso2  6920  difinfsn  6985  ctssdc  6998  enq0tr  7242  distrlem4prl  7392  distrlem4pru  7393  ltaprg  7427  aptiprlemu  7448  lelttr  7852  readdcan  7902  addcan  7942  addcan2  7943  ltadd2  8181  ltmul1a  8353  ltmul1  8354  divmulassap  8455  divmulasscomap  8456  lemul1a  8616  xrlelttr  9589  xleadd1a  9656  xlesubadd  9666  icoshftf1o  9774  lincmb01cmp  9786  iccf1o  9787  fztri3or  9819  fzofzim  9965  ioom  10038  modqmuladdim  10140  modqm1p1mod0  10148  q2submod  10158  modqaddmulmod  10164  ltexp2a  10345  exple1  10349  expnlbnd2  10417  expcan  10463  fiprsshashgt1  10563  fimaxq  10573  maxleastb  10986  maxltsup  10990  xrltmaxsup  11026  xrmaxltsup  11027  xrmaxaddlem  11029  addcn2  11079  mulcn2  11081  dvdsadd2b  11540  dvdsmod  11560  oexpneg  11574  divalglemex  11619  divalg  11621  gcdass  11703  rplpwr  11715  rppwr  11716  coprmdvds2  11774  rpmulgcd2  11776  qredeq  11777  rpdvds  11780  cncongr2  11785  rpexp  11831  znege1  11856  hashgcdlem  11903  ctinf  11943  neiint  12314  topssnei  12331  iscnp4  12387  cnptopco  12391  cnconst2  12402  cnrest2  12405  cnptoprest  12408  cnpdis  12411  bldisj  12570  blgt0  12571  bl2in  12572  blss2ps  12575  blss2  12576  xblm  12586  blssps  12596  blss  12597  xmetresbl  12609  bdbl  12672  metcnp3  12680  metcnp2  12682  cncfmptc  12751  dvcnp2cntop  12832  dvcn  12833