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 )

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

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 1011

This theorem is referenced by:  simpll1  1067  simprl1  1073  simp1l1  1121  simp2l1  1127  simp3l1  1133  3anandirs  1389  rspc3ev  2947  brcogw  4944  cocan1  5983  oawordi  6732  nnmord  6780  nnmword  6781  mapunen  7141  dif1en  7173  ac6sfi  7192  ordiso2  7365  difinfsn  7430  ctssdc  7443  2omotaplemap  7613  enq0tr  7791  distrlem4prl  7941  distrlem4pru  7942  ltaprg  7976  aptiprlemu  7997  lelttr  8404  readdcan  8456  addcan  8496  addcan2  8497  ltadd2  8737  ltmul1a  8909  ltmul1  8910  divmulassap  9015  divmulasscomap  9016  lemul1a  9178  xrlelttr  10187  xleadd1a  10254  xlesubadd  10264  icoshftf1o  10372  lincmb01cmp  10384  lincmble  10385  iccf1o  10386  fztri3or  10422  nn0p1elfzo  10572  fzofzim  10578  ioom  10673  modqmuladdim  10782  modqm1p1mod0  10790  q2submod  10800  modqaddmulmod  10806  ltexp2a  11006  exple1  11010  expnlbnd2  11081  nn0ltexp2  11125  nn0leexp2  11126  expcan  11132  fiprsshashgt1  11236  fimaxq  11248  hashtpgim  11275  hashtpg  11277  fun2dmnop0  11280  ccatass  11354  swrdlen  11402  swrdfv  11403  swrdswrdlem  11454  ccatopth  11466  maxleastb  11958  maxltsup  11962  xrltmaxsup  12001  xrmaxltsup  12002  xrmaxaddlem  12004  addcn2  12054  mulcn2  12056  dvdsmodexp  12540  dvdsadd2b  12585  dvdsmod  12607  oexpneg  12622  divalglemex  12667  divalg  12669  gcdass  12770  rplpwr  12782  rppwr  12783  nnwodc  12791  coprmdvds2  12849  rpmulgcd2  12851  qredeq  12852  rpdvds  12855  cncongr2  12860  rpexp  12909  znege1  12934  prmdiveq  12992  hashgcdlem  12994  odzdvds  13002  modprmn0modprm0  13013  coprimeprodsq2  13015  pythagtriplem3  13024  pcdvdsb  13077  pcgcd1  13085  qexpz  13109  pockthg  13114  ctinf  13299  nninfdc  13322  unbendc  13323  isnsgrp  13698  issubmnd  13732  ress0g  13733  mulgneg  13920  mulgdirlem  13933  submmulg  13946  subgmulg  13968  nmzsubg  13990  ghmmulg  14036  ring1eq0  14326  mulgass2  14336  rhmdvdsr  14455  rmodislmodlem  14659  rmodislmod  14660  lssintclm  14693  rnglidlrng  14807  2idlcpblrng  14832  neiint  15169  topssnei  15186  iscnp4  15242  cnptopco  15246  cnconst2  15257  cnrest2  15260  cnptoprest  15263  cnpdis  15266  bldisj  15425  blgt0  15426  bl2in  15427  blss2ps  15430  blss2  15431  xblm  15441  blssps  15451  blss  15452  xmetresbl  15464  bdbl  15527  metcnp3  15535  metcnp2  15537  cncfmptc  15620  dvcnp2cntop  15723  dvcn  15724  logdivlti  15905  ltexp2  15966  pellexlem2  16006  lgsfcl2  16039  lgsdilem  16060  lgsdirprm  16067  lgsdir  16068  lgsdi  16070  lgsne0  16071  incistruhgr  16245  clwwlkext2edg  16577  clwwlknonex2e  16595