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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpll1  1067  simprl1  1073  simp1l1  1121  simp2l1  1127  simp3l1  1133  3anandirs  1389  rspc3ev  2947  brcogw  4949  cocan1  5993  oawordi  6742  nnmord  6790  nnmword  6791  mapunen  7151  dif1en  7183  ac6sfi  7202  ordiso2  7375  difinfsn  7440  ctssdc  7453  2omotaplemap  7623  enq0tr  7801  distrlem4prl  7951  distrlem4pru  7952  ltaprg  7986  aptiprlemu  8007  lelttr  8414  readdcan  8466  addcan  8506  addcan2  8507  ltadd2  8747  ltmul1a  8919  ltmul1  8920  divmulassap  9025  divmulasscomap  9026  lemul1a  9188  xrlelttr  10208  xleadd1a  10275  xlesubadd  10285  icoshftf1o  10393  lincmb01cmp  10405  lincmble  10406  iccf1o  10407  fztri3or  10443  nn0p1elfzo  10594  fzofzim  10600  ioom  10695  modqmuladdim  10804  modqm1p1mod0  10812  q2submod  10822  modqaddmulmod  10828  ltexp2a  11028  exple1  11032  expnlbnd2  11103  nn0ltexp2  11147  nn0leexp2  11148  expcan  11154  fiprsshashgt1  11258  fimaxq  11270  hashtpgim  11297  hashtpg  11299  fun2dmnop0  11302  ccatass  11376  swrdlen  11424  swrdfv  11425  swrdswrdlem  11476  ccatopth  11488  maxleastb  11980  maxltsup  11984  xrltmaxsup  12023  xrmaxltsup  12024  xrmaxaddlem  12026  addcn2  12076  mulcn2  12078  dvdsmodexp  12562  dvdsadd2b  12607  dvdsmod  12629  oexpneg  12644  divalglemex  12689  divalg  12691  gcdass  12792  rplpwr  12804  rppwr  12805  nnwodc  12813  coprmdvds2  12871  rpmulgcd2  12873  qredeq  12874  rpdvds  12877  cncongr2  12882  rpexp  12931  znege1  12956  prmdiveq  13014  hashgcdlem  13016  odzdvds  13024  modprmn0modprm0  13035  coprimeprodsq2  13037  pythagtriplem3  13046  pcdvdsb  13099  pcgcd1  13107  qexpz  13131  pockthg  13136  ctinf  13321  nninfdc  13344  unbendc  13345  isnsgrp  13721  issubmnd  13755  ress0g  13756  mulgneg  13943  mulgdirlem  13956  submmulg  13969  subgmulg  13991  nmzsubg  14013  ghmmulg  14059  ring1eq0  14353  mulgass2  14363  rhmdvdsr  14482  rmodislmodlem  14687  rmodislmod  14688  lssintclm  14721  rnglidlrng  14835  2idlcpblrng  14860  issubassa  15013  neiint  15246  topssnei  15263  iscnp4  15319  cnptopco  15323  cnconst2  15334  cnrest2  15337  cnptoprest  15340  cnpdis  15343  bldisj  15502  blgt0  15503  bl2in  15504  blss2ps  15507  blss2  15508  xblm  15518  blssps  15528  blss  15529  xmetresbl  15541  bdbl  15604  metcnp3  15612  metcnp2  15614  cncfmptc  15697  dvcnp2cntop  15800  dvcn  15801  logdivlti  15982  ltexp2  16043  pellexlem2  16092  lgsfcl2  16125  lgsdilem  16146  lgsdirprm  16153  lgsdir  16154  lgsdi  16156  lgsne0  16157  incistruhgr  16331  clwwlkext2edg  16663  clwwlknonex2e  16681