Theorem simpl1 1031

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpll1  1067  simprl1  1073  simp1l1  1121  simp2l1  1127  simp3l1  1133  3anandirs  1389  rspc3ev  2947  brcogw  4949  cocan1  5993  oawordi  6742  nnmord  6790  nnmword  6791  mapunen  7151  dif1en  7183  ac6sfi  7202  ordiso2  7375  difinfsn  7440  ctssdc  7453  2omotaplemap  7623  enq0tr  7801  distrlem4prl  7951  distrlem4pru  7952  ltaprg  7986  aptiprlemu  8007  lelttr  8414  readdcan  8467  addcan  8507  addcan2  8508  ltadd2  8748  ltmul1a  8921  ltmul1  8922  divmulassap  9027  divmulasscomap  9028  lemul1a  9190  xrlelttr  10218  xleadd1a  10285  xlesubadd  10295  icoshftf1o  10403  lincmb01cmp  10415  lincmble  10416  iccf1o  10417  fztri3or  10453  nn0p1elfzo  10604  fzofzim  10610  ioom  10705  modqmuladdim  10817  modqm1p1mod0  10825  q2submod  10835  modqaddmulmod  10841  ltexp2a  11041  exple1  11045  expnlbnd2  11116  nn0ltexp2  11161  nn0leexp2  11162  expcan  11168  fiprsshashgt1  11272  fimaxq  11284  hashtpgim  11311  hashtpg  11313  fun2dmnop0  11316  ccatass  11390  swrdlen  11438  swrdfv  11439  swrdswrdlem  11490  ccatopth  11502  maxleastb  11995  maxltsup  11999  xrltmaxsup  12039  xrmaxltsup  12040  xrmaxaddlem  12042  addcn2  12092  mulcn2  12094  dvdsmodexp  12578  dvdsadd2b  12623  dvdsmod  12645  oexpneg  12660  divalglemex  12705  divalg  12707  gcdass  12808  rplpwr  12820  rppwr  12821  nnwodc  12829  coprmdvds2  12887  rpmulgcd2  12889  qredeq  12890  rpdvds  12893  cncongr2  12898  rpexp  12948  znege1  12974  prmdiveq  13034  hashgcdlem  13036  odzdvds  13044  modprmn0modprm0  13055  coprimeprodsq2  13057  pythagtriplem3  13066  pcdvdsb  13119  pcgcd1  13127  qexpz  13151  pockthg  13156  ctinf  13370  nninfdc  13393  unbendc  13394  isnsgrp  13770  issubmnd  13804  ress0g  13805  mulgneg  13992  mulgdirlem  14005  submmulg  14018  subgmulg  14040  nmzsubg  14062  ghmmulg  14108  ring1eq0  14402  mulgass2  14412  rhmdvdsr  14531  rmodislmodlem  14736  rmodislmod  14737  lssintclm  14770  rnglidlrng  14884  2idlcpblrng  14909  issubassa  15062  neiint  15295  topssnei  15312  iscnp4  15368  cnptopco  15372  cnconst2  15383  cnrest2  15386  cnptoprest  15389  cnpdis  15392  bldisj  15551  blgt0  15552  bl2in  15553  blss2ps  15556  blss2  15557  xblm  15567  blssps  15577  blss  15578  xmetresbl  15590  bdbl  15653  metcnp3  15661  metcnp2  15663  cncfmptc  15746  dvcnp2cntop  15849  dvcn  15850  logdivlti  16033  ltexp2  16096  pellexlem2  16149  bcmono  16202  lgsfcl2  16223  lgsdilem  16244  lgsdirprm  16251  lgsdir  16252  lgsdi  16254  lgsne0  16255  incistruhgr  16429  clwwlkext2edg  16761  clwwlknonex2e  16779