Theorem simpl3 1004

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

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

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 982

This theorem is referenced by:  simpll3  1040  simprl3  1046  simp1l3  1094  simp2l3  1100  simp3l3  1106  3anandirs  1360  ifnetruedc  3612  frirrg  4396  fcofo  5852  acexmid  5942  rdgon  6471  oawordi  6554  nnmord  6602  nnmword  6603  fidifsnen  6966  dif1en  6975  ac6sfi  6994  difinfsn  7201  2omotaplemap  7368  enq0tr  7546  distrlem4prl  7696  distrlem4pru  7697  ltaprg  7731  lelttr  8160  ltletr  8161  readdcan  8211  addcan  8251  addcan2  8252  ltadd2  8491  divmulassap  8767  xrlelttr  9927  xrltletr  9928  xaddass  9990  xleadd1a  9994  xlesubadd  10004  icoshftf1o  10112  difelfzle  10255  fzo1fzo0n0  10305  modqmuladdim  10510  modqmuladdnn0  10511  modqm1p1mod0  10518  q2submod  10528  modifeq2int  10529  modqaddmulmod  10534  seq1g  10606  seqp1g  10609  ltexp2a  10734  exple1  10738  expnlbnd2  10808  nn0ltexp2  10852  nn0leexp2  10853  mulsubdivbinom2ap  10854  expcan  10859  fiprsshashgt1  10960  fun2dmnop0  10990  ccatass  11062  maxleastb  11467  maxltsup  11471  xrltmaxsup  11510  xrmaxltsup  11511  xrmaxaddlem  11513  xrmaxadd  11514  addcn2  11563  mulcn2  11565  isumz  11642  dvdsmodexp  12048  modmulconst  12076  dvdsmod  12115  divalglemex  12175  divalg  12177  gcdass  12278  rplpwr  12290  rppwr  12291  nnwodc  12299  uzwodc  12300  rpmulgcd2  12359  rpdvds  12363  rpexp  12417  znege1  12442  prmdiveq  12500  hashgcdlem  12502  coprimeprodsq  12522  coprimeprodsq2  12523  pythagtriplem3  12532  pcdvdsb  12585  pcgcd1  12593  dvdsprmpweq  12600  pcbc  12616  ctinf  12743  nninfdc  12766  isnsgrp  13180  issubmnd  13216  mulgnn0p1  13411  mulgnnsubcl  13412  mulgneg  13418  mulgdirlem  13431  nmzsubg  13488  ghmmulg  13534  ring1eq0  13752  rmodislmod  14055  lspss  14103  2idlcpblrng  14227  neiint  14559  topssnei  14576  cnptopco  14636  cnrest2  14650  cnptoprest  14653  upxp  14686  bldisj  14815  blgt0  14816  bl2in  14817  blss2ps  14820  blss2  14821  xblm  14831  blssps  14841  blss  14842  bdmopn  14918  metcnp2  14927  txmetcnp  14932  cncfmptc  15010  dvcnp2cntop  15113  dvcn  15114  ply1term  15157  dvply1  15179  logdivlti  15295  ltexp2  15355  lgsfvalg  15424  lgsneg  15443  lgsmod  15445  lgsdilem  15446  lgsdirprm  15453  lgsdir  15454  lgsdi  15456  lgsne0  15457  1dom1el  15860