Theorem simpl3 1002

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

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

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 980

This theorem is referenced by:  simpll3  1038  simprl3  1044  simp1l3  1092  simp2l3  1098  simp3l3  1104  3anandirs  1348  frirrg  4349  fcofo  5782  acexmid  5871  rdgon  6384  oawordi  6467  nnmord  6515  nnmword  6516  fidifsnen  6867  dif1en  6876  ac6sfi  6895  difinfsn  7096  2omotaplemap  7253  enq0tr  7430  distrlem4prl  7580  distrlem4pru  7581  ltaprg  7615  lelttr  8042  ltletr  8043  readdcan  8093  addcan  8133  addcan2  8134  ltadd2  8372  divmulassap  8648  xrlelttr  9802  xrltletr  9803  xaddass  9865  xleadd1a  9869  xlesubadd  9879  icoshftf1o  9987  difelfzle  10129  fzo1fzo0n0  10178  modqmuladdim  10362  modqmuladdnn0  10363  modqm1p1mod0  10370  q2submod  10380  modifeq2int  10381  modqaddmulmod  10386  ltexp2a  10567  exple1  10571  expnlbnd2  10640  nn0ltexp2  10683  nn0leexp2  10684  expcan  10689  fiprsshashgt1  10790  maxleastb  11216  maxltsup  11220  xrltmaxsup  11258  xrmaxltsup  11259  xrmaxaddlem  11261  xrmaxadd  11262  addcn2  11311  mulcn2  11313  isumz  11390  dvdsmodexp  11795  modmulconst  11823  dvdsmod  11860  divalglemex  11919  divalg  11921  gcdass  12008  rplpwr  12020  rppwr  12021  nnwodc  12029  uzwodc  12030  rpmulgcd2  12087  rpdvds  12091  rpexp  12145  znege1  12170  prmdiveq  12228  hashgcdlem  12230  coprimeprodsq  12249  coprimeprodsq2  12250  pythagtriplem3  12259  pcdvdsb  12311  pcgcd1  12319  dvdsprmpweq  12326  pcbc  12341  ctinf  12423  nninfdc  12446  isnsgrp  12744  issubmnd  12775  mulgnn0p1  12926  mulgnnsubcl  12927  mulgneg  12933  mulgdirlem  12945  nmzsubg  13001  ring1eq0  13156  neiint  13516  topssnei  13533  cnptopco  13593  cnrest2  13607  cnptoprest  13610  upxp  13643  bldisj  13772  blgt0  13773  bl2in  13774  blss2ps  13777  blss2  13778  xblm  13788  blssps  13798  blss  13799  bdmopn  13875  metcnp2  13884  txmetcnp  13889  cncfmptc  13953  dvcnp2cntop  14034  dvcn  14035  logdivlti  14173  ltexp2  14231  lgsfvalg  14277  lgsneg  14296  lgsmod  14298  lgsdilem  14299  lgsdirprm  14306  lgsdir  14307  lgsdi  14309  lgsne0  14310