Theorem simpl1 1024

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

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

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 1004

This theorem is referenced by:  simpll1  1060  simprl1  1066  simp1l1  1114  simp2l1  1120  simp3l1  1126  3anandirs  1382  rspc3ev  2924  brcogw  4890  cocan1  5910  oawordi  6613  nnmord  6661  nnmword  6662  dif1en  7037  ac6sfi  7056  ordiso2  7198  difinfsn  7263  ctssdc  7276  2omotaplemap  7439  enq0tr  7617  distrlem4prl  7767  distrlem4pru  7768  ltaprg  7802  aptiprlemu  7823  lelttr  8231  readdcan  8282  addcan  8322  addcan2  8323  ltadd2  8562  ltmul1a  8734  ltmul1  8735  divmulassap  8838  divmulasscomap  8839  lemul1a  9001  xrlelttr  9998  xleadd1a  10065  xlesubadd  10075  icoshftf1o  10183  lincmb01cmp  10195  iccf1o  10196  fztri3or  10231  fzofzim  10384  ioom  10475  modqmuladdim  10584  modqm1p1mod0  10592  q2submod  10602  modqaddmulmod  10608  ltexp2a  10808  exple1  10812  expnlbnd2  10882  nn0ltexp2  10926  nn0leexp2  10927  expcan  10933  fiprsshashgt1  11034  fimaxq  11044  fun2dmnop0  11064  ccatass  11138  swrdlen  11179  swrdfv  11180  swrdswrdlem  11231  ccatopth  11243  maxleastb  11720  maxltsup  11724  xrltmaxsup  11763  xrmaxltsup  11764  xrmaxaddlem  11766  addcn2  11816  mulcn2  11818  dvdsmodexp  12301  dvdsadd2b  12346  dvdsmod  12368  oexpneg  12383  divalglemex  12428  divalg  12430  gcdass  12531  rplpwr  12543  rppwr  12544  nnwodc  12552  coprmdvds2  12610  rpmulgcd2  12612  qredeq  12613  rpdvds  12616  cncongr2  12621  rpexp  12670  znege1  12695  prmdiveq  12753  hashgcdlem  12755  odzdvds  12763  modprmn0modprm0  12774  coprimeprodsq2  12776  pythagtriplem3  12785  pcdvdsb  12838  pcgcd1  12846  qexpz  12870  pockthg  12875  ctinf  12996  nninfdc  13019  unbendc  13020  isnsgrp  13434  issubmnd  13470  ress0g  13471  mulgneg  13672  mulgdirlem  13685  submmulg  13698  subgmulg  13720  nmzsubg  13742  ghmmulg  13788  srg1zr  13945  ring1eq0  14006  mulgass2  14016  rhmdvdsr  14133  rmodislmodlem  14308  rmodislmod  14309  lssintclm  14342  rnglidlrng  14456  2idlcpblrng  14481  neiint  14813  topssnei  14830  iscnp4  14886  cnptopco  14890  cnconst2  14901  cnrest2  14904  cnptoprest  14907  cnpdis  14910  bldisj  15069  blgt0  15070  bl2in  15071  blss2ps  15074  blss2  15075  xblm  15085  blssps  15095  blss  15096  xmetresbl  15108  bdbl  15171  metcnp3  15179  metcnp2  15181  cncfmptc  15264  dvcnp2cntop  15367  dvcn  15368  logdivlti  15549  ltexp2  15609  lgsfcl2  15679  lgsdilem  15700  lgsdirprm  15707  lgsdir  15708  lgsdi  15710  lgsne0  15711  incistruhgr  15884