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  3666  frirrg  4471  fcofo  5957  acexmid  6049  rdgon  6617  oawordi  6702  nnmord  6750  nnmword  6751  1dom1el  7060  mapunen  7104  fidifsnen  7125  dif1en  7136  ac6sfi  7155  fissfi  7216  difinfsn  7391  2omotaplemap  7571  enq0tr  7749  distrlem4prl  7899  distrlem4pru  7900  ltaprg  7934  lelttr  8362  ltletr  8363  readdcan  8413  addcan  8453  addcan2  8454  ltadd2  8693  divmulassap  8969  xrlelttr  10139  xrltletr  10140  xaddass  10202  xleadd1a  10206  xlesubadd  10216  icoshftf1o  10324  lincmble  10337  difelfzle  10468  fzo1fzo0n0  10522  modqmuladdim  10729  modqmuladdnn0  10730  modqm1p1mod0  10737  q2submod  10747  modifeq2int  10748  modqaddmulmod  10753  seq1g  10825  seqp1g  10828  ltexp2a  10953  exple1  10957  expnlbnd2  11027  nn0ltexp2  11071  nn0leexp2  11072  mulsubdivbinom2ap  11073  expcan  11078  fiprsshashgt1  11182  hashtpgim  11217  hashtpg  11219  fun2dmnop0  11222  ccatass  11296  fzowrddc  11339  swrdclg  11342  ccatopth  11408  pfxccatin12lem2a  11419  pfxccat3  11426  maxleastb  11899  maxltsup  11903  xrltmaxsup  11942  xrmaxltsup  11943  xrmaxaddlem  11945  xrmaxadd  11946  addcn2  11995  mulcn2  11997  isumz  12075  dvdsmodexp  12481  modmulconst  12509  dvdsmod  12548  divalglemex  12608  divalg  12610  gcdass  12711  rplpwr  12723  rppwr  12724  nnwodc  12732  uzwodc  12733  rpmulgcd2  12792  rpdvds  12796  rpexp  12850  znege1  12875  prmdiveq  12933  hashgcdlem  12935  coprimeprodsq  12955  coprimeprodsq2  12956  pythagtriplem3  12965  pcdvdsb  13018  pcgcd1  13026  dvdsprmpweq  13033  pcbc  13049  ctinf  13181  nninfdc  13204  isnsgrp  13619  issubmnd  13655  mulgnn0p1  13850  mulgnnsubcl  13851  mulgneg  13857  mulgdirlem  13870  nmzsubg  13927  ghmmulg  13973  ring1eq0  14192  rmodislmod  14499  lspss  14547  2idlcpblrng  14671  neiint  15010  topssnei  15027  cnptopco  15087  cnrest2  15101  cnptoprest  15104  upxp  15137  bldisj  15266  blgt0  15267  bl2in  15268  blss2ps  15271  blss2  15272  xblm  15282  blssps  15292  blss  15293  bdmopn  15369  metcnp2  15378  txmetcnp  15383  cncfmptc  15461  dvcnp2cntop  15564  dvcn  15565  ply1term  15608  dvply1  15630  logdivlti  15746  ltexp2  15806  pellexlem2  15846  lgsfvalg  15878  lgsneg  15897  lgsmod  15899  lgsdilem  15900  lgsdirprm  15907  lgsdir  15908  lgsdi  15910  lgsne0  15911  gfsumsn  16867