Theorem simpl3 1029

Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)

Assertion

Ref	Expression
simpl3	|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )

Proof of Theorem simpl3

Step	Hyp	Ref	Expression
1		simp3 1026	. 2 |- ( ( ph /\ ps /\ ch ) -> ch )
2	1	adantr 276	1 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )

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  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  simpll3  1065  simprl3  1071  simp1l3  1119  simp2l3  1125  simp3l3  1131  3anandirs  1385  ifnetruedc  3653  frirrg  4453  fcofo  5935  acexmid  6027  rdgon  6595  oawordi  6680  nnmord  6728  nnmword  6729  1dom1el  7036  fidifsnen  7100  dif1en  7111  ac6sfi  7130  difinfsn  7342  2omotaplemap  7519  enq0tr  7697  distrlem4prl  7847  distrlem4pru  7848  ltaprg  7882  lelttr  8310  ltletr  8311  readdcan  8361  addcan  8401  addcan2  8402  ltadd2  8641  divmulassap  8917  xrlelttr  10085  xrltletr  10086  xaddass  10148  xleadd1a  10152  xlesubadd  10162  icoshftf1o  10270  lincmble  10283  difelfzle  10414  fzo1fzo0n0  10468  modqmuladdim  10675  modqmuladdnn0  10676  modqm1p1mod0  10683  q2submod  10693  modifeq2int  10694  modqaddmulmod  10699  seq1g  10771  seqp1g  10774  ltexp2a  10899  exple1  10903  expnlbnd2  10973  nn0ltexp2  11017  nn0leexp2  11018  mulsubdivbinom2ap  11019  expcan  11024  fiprsshashgt1  11127  hashtpgim  11155  hashtpg  11157  fun2dmnop0  11160  ccatass  11234  fzowrddc  11277  swrdclg  11280  ccatopth  11346  pfxccatin12lem2a  11357  pfxccat3  11364  maxleastb  11837  maxltsup  11841  xrltmaxsup  11880  xrmaxltsup  11881  xrmaxaddlem  11883  xrmaxadd  11884  addcn2  11933  mulcn2  11935  isumz  12013  dvdsmodexp  12419  modmulconst  12447  dvdsmod  12486  divalglemex  12546  divalg  12548  gcdass  12649  rplpwr  12661  rppwr  12662  nnwodc  12670  uzwodc  12671  rpmulgcd2  12730  rpdvds  12734  rpexp  12788  znege1  12813  prmdiveq  12871  hashgcdlem  12873  coprimeprodsq  12893  coprimeprodsq2  12894  pythagtriplem3  12903  pcdvdsb  12956  pcgcd1  12964  dvdsprmpweq  12971  pcbc  12987  ctinf  13114  nninfdc  13137  isnsgrp  13552  issubmnd  13588  mulgnn0p1  13783  mulgnnsubcl  13784  mulgneg  13790  mulgdirlem  13803  nmzsubg  13860  ghmmulg  13906  ring1eq0  14125  rmodislmod  14430  lspss  14478  2idlcpblrng  14602  neiint  14939  topssnei  14956  cnptopco  15016  cnrest2  15030  cnptoprest  15033  upxp  15066  bldisj  15195  blgt0  15196  bl2in  15197  blss2ps  15200  blss2  15201  xblm  15211  blssps  15221  blss  15222  bdmopn  15298  metcnp2  15307  txmetcnp  15312  cncfmptc  15390  dvcnp2cntop  15493  dvcn  15494  ply1term  15537  dvply1  15559  logdivlti  15675  ltexp2  15735  pellexlem2  15775  lgsfvalg  15807  lgsneg  15826  lgsmod  15828  lgsdilem  15829  lgsdirprm  15836  lgsdir  15837  lgsdi  15839  lgsne0  15840  gfsumsn  16797