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  11496  maxltsup  11500  xrltmaxsup  11539  xrmaxltsup  11540  xrmaxaddlem  11542  xrmaxadd  11543  addcn2  11592  mulcn2  11594  isumz  11671  dvdsmodexp  12077  modmulconst  12105  dvdsmod  12144  divalglemex  12204  divalg  12206  gcdass  12307  rplpwr  12319  rppwr  12320  nnwodc  12328  uzwodc  12329  rpmulgcd2  12388  rpdvds  12392  rpexp  12446  znege1  12471  prmdiveq  12529  hashgcdlem  12531  coprimeprodsq  12551  coprimeprodsq2  12552  pythagtriplem3  12561  pcdvdsb  12614  pcgcd1  12622  dvdsprmpweq  12629  pcbc  12645  ctinf  12772  nninfdc  12795  isnsgrp  13209  issubmnd  13245  mulgnn0p1  13440  mulgnnsubcl  13441  mulgneg  13447  mulgdirlem  13460  nmzsubg  13517  ghmmulg  13563  ring1eq0  13781  rmodislmod  14084  lspss  14132  2idlcpblrng  14256  neiint  14588  topssnei  14605  cnptopco  14665  cnrest2  14679  cnptoprest  14682  upxp  14715  bldisj  14844  blgt0  14845  bl2in  14846  blss2ps  14849  blss2  14850  xblm  14860  blssps  14870  blss  14871  bdmopn  14947  metcnp2  14956  txmetcnp  14961  cncfmptc  15039  dvcnp2cntop  15142  dvcn  15143  ply1term  15186  dvply1  15208  logdivlti  15324  ltexp2  15384  lgsfvalg  15453  lgsneg  15472  lgsmod  15474  lgsdilem  15475  lgsdirprm  15482  lgsdir  15483  lgsdi  15485  lgsne0  15486  1dom1el  15889