Theorem simpl1 1024

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

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

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 1004

This theorem is referenced by:  simpll1  1060  simprl1  1066  simp1l1  1114  simp2l1  1120  simp3l1  1126  3anandirs  1382  rspc3ev  2924  brcogw  4891  cocan1  5917  oawordi  6623  nnmord  6671  nnmword  6672  dif1en  7049  ac6sfi  7068  ordiso2  7213  difinfsn  7278  ctssdc  7291  2omotaplemap  7454  enq0tr  7632  distrlem4prl  7782  distrlem4pru  7783  ltaprg  7817  aptiprlemu  7838  lelttr  8246  readdcan  8297  addcan  8337  addcan2  8338  ltadd2  8577  ltmul1a  8749  ltmul1  8750  divmulassap  8853  divmulasscomap  8854  lemul1a  9016  xrlelttr  10014  xleadd1a  10081  xlesubadd  10091  icoshftf1o  10199  lincmb01cmp  10211  iccf1o  10212  fztri3or  10247  fzofzim  10400  ioom  10492  modqmuladdim  10601  modqm1p1mod0  10609  q2submod  10619  modqaddmulmod  10625  ltexp2a  10825  exple1  10829  expnlbnd2  10899  nn0ltexp2  10943  nn0leexp2  10944  expcan  10950  fiprsshashgt1  11052  fimaxq  11062  fun2dmnop0  11082  ccatass  11156  swrdlen  11199  swrdfv  11200  swrdswrdlem  11251  ccatopth  11263  maxleastb  11740  maxltsup  11744  xrltmaxsup  11783  xrmaxltsup  11784  xrmaxaddlem  11786  addcn2  11836  mulcn2  11838  dvdsmodexp  12321  dvdsadd2b  12366  dvdsmod  12388  oexpneg  12403  divalglemex  12448  divalg  12450  gcdass  12551  rplpwr  12563  rppwr  12564  nnwodc  12572  coprmdvds2  12630  rpmulgcd2  12632  qredeq  12633  rpdvds  12636  cncongr2  12641  rpexp  12690  znege1  12715  prmdiveq  12773  hashgcdlem  12775  odzdvds  12783  modprmn0modprm0  12794  coprimeprodsq2  12796  pythagtriplem3  12805  pcdvdsb  12858  pcgcd1  12866  qexpz  12890  pockthg  12895  ctinf  13016  nninfdc  13039  unbendc  13040  isnsgrp  13454  issubmnd  13490  ress0g  13491  mulgneg  13692  mulgdirlem  13705  submmulg  13718  subgmulg  13740  nmzsubg  13762  ghmmulg  13808  srg1zr  13965  ring1eq0  14026  mulgass2  14036  rhmdvdsr  14154  rmodislmodlem  14329  rmodislmod  14330  lssintclm  14363  rnglidlrng  14477  2idlcpblrng  14502  neiint  14834  topssnei  14851  iscnp4  14907  cnptopco  14911  cnconst2  14922  cnrest2  14925  cnptoprest  14928  cnpdis  14931  bldisj  15090  blgt0  15091  bl2in  15092  blss2ps  15095  blss2  15096  xblm  15106  blssps  15116  blss  15117  xmetresbl  15129  bdbl  15192  metcnp3  15200  metcnp2  15202  cncfmptc  15285  dvcnp2cntop  15388  dvcn  15389  logdivlti  15570  ltexp2  15630  lgsfcl2  15700  lgsdilem  15721  lgsdirprm  15728  lgsdir  15729  lgsdi  15731  lgsne0  15732  incistruhgr  15905