Theorem simpl1 1027

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

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

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 1007

This theorem is referenced by:  simpll1  1063  simprl1  1069  simp1l1  1117  simp2l1  1123  simp3l1  1129  3anandirs  1385  rspc3ev  2938  brcogw  4924  cocan1  5960  oawordi  6702  nnmord  6750  nnmword  6751  mapunen  7104  dif1en  7136  ac6sfi  7155  ordiso2  7326  difinfsn  7391  ctssdc  7404  2omotaplemap  7571  enq0tr  7749  distrlem4prl  7899  distrlem4pru  7900  ltaprg  7934  aptiprlemu  7955  lelttr  8362  readdcan  8413  addcan  8453  addcan2  8454  ltadd2  8693  ltmul1a  8865  ltmul1  8866  divmulassap  8969  divmulasscomap  8970  lemul1a  9132  xrlelttr  10139  xleadd1a  10206  xlesubadd  10216  icoshftf1o  10324  lincmb01cmp  10336  lincmble  10337  iccf1o  10338  fztri3or  10373  nn0p1elfzo  10521  fzofzim  10527  ioom  10620  modqmuladdim  10729  modqm1p1mod0  10737  q2submod  10747  modqaddmulmod  10753  ltexp2a  10953  exple1  10957  expnlbnd2  11027  nn0ltexp2  11071  nn0leexp2  11072  expcan  11078  fiprsshashgt1  11182  fimaxq  11194  hashtpgim  11217  hashtpg  11219  fun2dmnop0  11222  ccatass  11296  swrdlen  11344  swrdfv  11345  swrdswrdlem  11396  ccatopth  11408  maxleastb  11899  maxltsup  11903  xrltmaxsup  11942  xrmaxltsup  11943  xrmaxaddlem  11945  addcn2  11995  mulcn2  11997  dvdsmodexp  12481  dvdsadd2b  12526  dvdsmod  12548  oexpneg  12563  divalglemex  12608  divalg  12610  gcdass  12711  rplpwr  12723  rppwr  12724  nnwodc  12732  coprmdvds2  12790  rpmulgcd2  12792  qredeq  12793  rpdvds  12796  cncongr2  12801  rpexp  12850  znege1  12875  prmdiveq  12933  hashgcdlem  12935  odzdvds  12943  modprmn0modprm0  12954  coprimeprodsq2  12956  pythagtriplem3  12965  pcdvdsb  13018  pcgcd1  13026  qexpz  13050  pockthg  13055  ctinf  13181  nninfdc  13204  unbendc  13205  isnsgrp  13619  issubmnd  13655  ress0g  13656  mulgneg  13857  mulgdirlem  13870  submmulg  13883  subgmulg  13905  nmzsubg  13927  ghmmulg  13973  srg1zr  14131  ring1eq0  14192  mulgass2  14202  rhmdvdsr  14320  rmodislmodlem  14498  rmodislmod  14499  lssintclm  14532  rnglidlrng  14646  2idlcpblrng  14671  neiint  15010  topssnei  15027  iscnp4  15083  cnptopco  15087  cnconst2  15098  cnrest2  15101  cnptoprest  15104  cnpdis  15107  bldisj  15266  blgt0  15267  bl2in  15268  blss2ps  15271  blss2  15272  xblm  15282  blssps  15292  blss  15293  xmetresbl  15305  bdbl  15368  metcnp3  15376  metcnp2  15378  cncfmptc  15461  dvcnp2cntop  15564  dvcn  15565  logdivlti  15746  ltexp2  15806  pellexlem2  15846  lgsfcl2  15879  lgsdilem  15900  lgsdirprm  15907  lgsdir  15908  lgsdi  15910  lgsne0  15911  incistruhgr  16085  clwwlkext2edg  16417  clwwlknonex2e  16435