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  2925  brcogw  4897  cocan1  5923  oawordi  6632  nnmord  6680  nnmword  6681  dif1en  7061  ac6sfi  7080  ordiso2  7225  difinfsn  7290  ctssdc  7303  2omotaplemap  7466  enq0tr  7644  distrlem4prl  7794  distrlem4pru  7795  ltaprg  7829  aptiprlemu  7850  lelttr  8258  readdcan  8309  addcan  8349  addcan2  8350  ltadd2  8589  ltmul1a  8761  ltmul1  8762  divmulassap  8865  divmulasscomap  8866  lemul1a  9028  xrlelttr  10031  xleadd1a  10098  xlesubadd  10108  icoshftf1o  10216  lincmb01cmp  10228  iccf1o  10229  fztri3or  10264  fzofzim  10417  ioom  10510  modqmuladdim  10619  modqm1p1mod0  10627  q2submod  10637  modqaddmulmod  10643  ltexp2a  10843  exple1  10847  expnlbnd2  10917  nn0ltexp2  10961  nn0leexp2  10962  expcan  10968  fiprsshashgt1  11071  fimaxq  11081  fun2dmnop0  11101  ccatass  11175  swrdlen  11223  swrdfv  11224  swrdswrdlem  11275  ccatopth  11287  maxleastb  11765  maxltsup  11769  xrltmaxsup  11808  xrmaxltsup  11809  xrmaxaddlem  11811  addcn2  11861  mulcn2  11863  dvdsmodexp  12346  dvdsadd2b  12391  dvdsmod  12413  oexpneg  12428  divalglemex  12473  divalg  12475  gcdass  12576  rplpwr  12588  rppwr  12589  nnwodc  12597  coprmdvds2  12655  rpmulgcd2  12657  qredeq  12658  rpdvds  12661  cncongr2  12666  rpexp  12715  znege1  12740  prmdiveq  12798  hashgcdlem  12800  odzdvds  12808  modprmn0modprm0  12819  coprimeprodsq2  12821  pythagtriplem3  12830  pcdvdsb  12883  pcgcd1  12891  qexpz  12915  pockthg  12920  ctinf  13041  nninfdc  13064  unbendc  13065  isnsgrp  13479  issubmnd  13515  ress0g  13516  mulgneg  13717  mulgdirlem  13730  submmulg  13743  subgmulg  13765  nmzsubg  13787  ghmmulg  13833  srg1zr  13990  ring1eq0  14051  mulgass2  14061  rhmdvdsr  14179  rmodislmodlem  14354  rmodislmod  14355  lssintclm  14388  rnglidlrng  14502  2idlcpblrng  14527  neiint  14859  topssnei  14876  iscnp4  14932  cnptopco  14936  cnconst2  14947  cnrest2  14950  cnptoprest  14953  cnpdis  14956  bldisj  15115  blgt0  15116  bl2in  15117  blss2ps  15120  blss2  15121  xblm  15131  blssps  15141  blss  15142  xmetresbl  15154  bdbl  15217  metcnp3  15225  metcnp2  15227  cncfmptc  15310  dvcnp2cntop  15413  dvcn  15414  logdivlti  15595  ltexp2  15655  lgsfcl2  15725  lgsdilem  15746  lgsdirprm  15753  lgsdir  15754  lgsdi  15756  lgsne0  15757  incistruhgr  15931  clwwlkext2edg  16217  clwwlknonex2e  16235