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  2941  brcogw  4929  cocan1  5966  oawordi  6715  nnmord  6763  nnmword  6764  mapunen  7117  dif1en  7149  ac6sfi  7168  ordiso2  7339  difinfsn  7404  ctssdc  7417  2omotaplemap  7587  enq0tr  7765  distrlem4prl  7915  distrlem4pru  7916  ltaprg  7950  aptiprlemu  7971  lelttr  8378  readdcan  8429  addcan  8469  addcan2  8470  ltadd2  8710  ltmul1a  8882  ltmul1  8883  divmulassap  8986  divmulasscomap  8987  lemul1a  9149  xrlelttr  10158  xleadd1a  10225  xlesubadd  10235  icoshftf1o  10343  lincmb01cmp  10355  lincmble  10356  iccf1o  10357  fztri3or  10393  nn0p1elfzo  10543  fzofzim  10549  ioom  10644  modqmuladdim  10753  modqm1p1mod0  10761  q2submod  10771  modqaddmulmod  10777  ltexp2a  10977  exple1  10981  expnlbnd2  11052  nn0ltexp2  11096  nn0leexp2  11097  expcan  11103  fiprsshashgt1  11207  fimaxq  11219  hashtpgim  11242  hashtpg  11244  fun2dmnop0  11247  ccatass  11321  swrdlen  11369  swrdfv  11370  swrdswrdlem  11421  ccatopth  11433  maxleastb  11924  maxltsup  11928  xrltmaxsup  11967  xrmaxltsup  11968  xrmaxaddlem  11970  addcn2  12020  mulcn2  12022  dvdsmodexp  12506  dvdsadd2b  12551  dvdsmod  12573  oexpneg  12588  divalglemex  12633  divalg  12635  gcdass  12736  rplpwr  12748  rppwr  12749  nnwodc  12757  coprmdvds2  12815  rpmulgcd2  12817  qredeq  12818  rpdvds  12821  cncongr2  12826  rpexp  12875  znege1  12900  prmdiveq  12958  hashgcdlem  12960  odzdvds  12968  modprmn0modprm0  12979  coprimeprodsq2  12981  pythagtriplem3  12990  pcdvdsb  13043  pcgcd1  13051  qexpz  13075  pockthg  13080  ctinf  13265  nninfdc  13288  unbendc  13289  isnsgrp  13669  issubmnd  13703  ress0g  13704  mulgneg  13893  mulgdirlem  13906  submmulg  13919  subgmulg  13941  nmzsubg  13963  ghmmulg  14009  ring1eq0  14291  mulgass2  14301  rhmdvdsr  14420  rmodislmodlem  14624  rmodislmod  14625  lssintclm  14658  rnglidlrng  14772  2idlcpblrng  14797  neiint  15136  topssnei  15153  iscnp4  15209  cnptopco  15213  cnconst2  15224  cnrest2  15227  cnptoprest  15230  cnpdis  15233  bldisj  15392  blgt0  15393  bl2in  15394  blss2ps  15397  blss2  15398  xblm  15408  blssps  15418  blss  15419  xmetresbl  15431  bdbl  15494  metcnp3  15502  metcnp2  15504  cncfmptc  15587  dvcnp2cntop  15690  dvcn  15691  logdivlti  15872  ltexp2  15932  pellexlem2  15972  lgsfcl2  16005  lgsdilem  16026  lgsdirprm  16033  lgsdir  16034  lgsdi  16036  lgsne0  16037  incistruhgr  16211  clwwlkext2edg  16543  clwwlknonex2e  16561