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  2928  brcogw  4905  cocan1  5938  oawordi  6680  nnmord  6728  nnmword  6729  dif1en  7111  ac6sfi  7130  ordiso2  7277  difinfsn  7342  ctssdc  7355  2omotaplemap  7519  enq0tr  7697  distrlem4prl  7847  distrlem4pru  7848  ltaprg  7882  aptiprlemu  7903  lelttr  8310  readdcan  8361  addcan  8401  addcan2  8402  ltadd2  8641  ltmul1a  8813  ltmul1  8814  divmulassap  8917  divmulasscomap  8918  lemul1a  9080  xrlelttr  10085  xleadd1a  10152  xlesubadd  10162  icoshftf1o  10270  lincmb01cmp  10282  lincmble  10283  iccf1o  10284  fztri3or  10319  nn0p1elfzo  10467  fzofzim  10473  ioom  10566  modqmuladdim  10675  modqm1p1mod0  10683  q2submod  10693  modqaddmulmod  10699  ltexp2a  10899  exple1  10903  expnlbnd2  10973  nn0ltexp2  11017  nn0leexp2  11018  expcan  11024  fiprsshashgt1  11127  fimaxq  11137  hashtpgim  11155  hashtpg  11157  fun2dmnop0  11160  ccatass  11234  swrdlen  11282  swrdfv  11283  swrdswrdlem  11334  ccatopth  11346  maxleastb  11837  maxltsup  11841  xrltmaxsup  11880  xrmaxltsup  11881  xrmaxaddlem  11883  addcn2  11933  mulcn2  11935  dvdsmodexp  12419  dvdsadd2b  12464  dvdsmod  12486  oexpneg  12501  divalglemex  12546  divalg  12548  gcdass  12649  rplpwr  12661  rppwr  12662  nnwodc  12670  coprmdvds2  12728  rpmulgcd2  12730  qredeq  12731  rpdvds  12734  cncongr2  12739  rpexp  12788  znege1  12813  prmdiveq  12871  hashgcdlem  12873  odzdvds  12881  modprmn0modprm0  12892  coprimeprodsq2  12894  pythagtriplem3  12903  pcdvdsb  12956  pcgcd1  12964  qexpz  12988  pockthg  12993  ctinf  13114  nninfdc  13137  unbendc  13138  isnsgrp  13552  issubmnd  13588  ress0g  13589  mulgneg  13790  mulgdirlem  13803  submmulg  13816  subgmulg  13838  nmzsubg  13860  ghmmulg  13906  srg1zr  14064  ring1eq0  14125  mulgass2  14135  rhmdvdsr  14253  rmodislmodlem  14429  rmodislmod  14430  lssintclm  14463  rnglidlrng  14577  2idlcpblrng  14602  neiint  14939  topssnei  14956  iscnp4  15012  cnptopco  15016  cnconst2  15027  cnrest2  15030  cnptoprest  15033  cnpdis  15036  bldisj  15195  blgt0  15196  bl2in  15197  blss2ps  15200  blss2  15201  xblm  15211  blssps  15221  blss  15222  xmetresbl  15234  bdbl  15297  metcnp3  15305  metcnp2  15307  cncfmptc  15390  dvcnp2cntop  15493  dvcn  15494  logdivlti  15675  ltexp2  15735  pellexlem2  15775  lgsfcl2  15808  lgsdilem  15829  lgsdirprm  15836  lgsdir  15837  lgsdi  15839  lgsne0  15840  incistruhgr  16014  clwwlkext2edg  16346  clwwlknonex2e  16364