Theorem simpl1 1003

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

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

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 983

This theorem is referenced by:  simpll1  1039  simprl1  1045  simp1l1  1093  simp2l1  1099  simp3l1  1105  3anandirs  1361  rspc3ev  2901  brcogw  4865  cocan1  5879  oawordi  6578  nnmord  6626  nnmword  6627  dif1en  7002  ac6sfi  7021  ordiso2  7163  difinfsn  7228  ctssdc  7241  2omotaplemap  7404  enq0tr  7582  distrlem4prl  7732  distrlem4pru  7733  ltaprg  7767  aptiprlemu  7788  lelttr  8196  readdcan  8247  addcan  8287  addcan2  8288  ltadd2  8527  ltmul1a  8699  ltmul1  8700  divmulassap  8803  divmulasscomap  8804  lemul1a  8966  xrlelttr  9963  xleadd1a  10030  xlesubadd  10040  icoshftf1o  10148  lincmb01cmp  10160  iccf1o  10161  fztri3or  10196  fzofzim  10349  ioom  10440  modqmuladdim  10549  modqm1p1mod0  10557  q2submod  10567  modqaddmulmod  10573  ltexp2a  10773  exple1  10777  expnlbnd2  10847  nn0ltexp2  10891  nn0leexp2  10892  expcan  10898  fiprsshashgt1  10999  fimaxq  11009  fun2dmnop0  11029  ccatass  11102  swrdlen  11143  swrdfv  11144  swrdswrdlem  11195  ccatopth  11207  maxleastb  11640  maxltsup  11644  xrltmaxsup  11683  xrmaxltsup  11684  xrmaxaddlem  11686  addcn2  11736  mulcn2  11738  dvdsmodexp  12221  dvdsadd2b  12266  dvdsmod  12288  oexpneg  12303  divalglemex  12348  divalg  12350  gcdass  12451  rplpwr  12463  rppwr  12464  nnwodc  12472  coprmdvds2  12530  rpmulgcd2  12532  qredeq  12533  rpdvds  12536  cncongr2  12541  rpexp  12590  znege1  12615  prmdiveq  12673  hashgcdlem  12675  odzdvds  12683  modprmn0modprm0  12694  coprimeprodsq2  12696  pythagtriplem3  12705  pcdvdsb  12758  pcgcd1  12766  qexpz  12790  pockthg  12795  ctinf  12916  nninfdc  12939  unbendc  12940  isnsgrp  13353  issubmnd  13389  ress0g  13390  mulgneg  13591  mulgdirlem  13604  submmulg  13617  subgmulg  13639  nmzsubg  13661  ghmmulg  13707  srg1zr  13864  ring1eq0  13925  mulgass2  13935  rhmdvdsr  14052  rmodislmodlem  14227  rmodislmod  14228  lssintclm  14261  rnglidlrng  14375  2idlcpblrng  14400  neiint  14732  topssnei  14749  iscnp4  14805  cnptopco  14809  cnconst2  14820  cnrest2  14823  cnptoprest  14826  cnpdis  14829  bldisj  14988  blgt0  14989  bl2in  14990  blss2ps  14993  blss2  14994  xblm  15004  blssps  15014  blss  15015  xmetresbl  15027  bdbl  15090  metcnp3  15098  metcnp2  15100  cncfmptc  15183  dvcnp2cntop  15286  dvcn  15287  logdivlti  15468  ltexp2  15528  lgsfcl2  15598  lgsdilem  15619  lgsdirprm  15626  lgsdir  15627  lgsdi  15629  lgsne0  15630  incistruhgr  15801