Theorem simpl3 1033

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpll3  1069  simprl3  1075  simp1l3  1123  simp2l3  1129  simp3l3  1135  3anandirs  1389  ifnetruedc  3684  frirrg  4497  fcofo  5993  acexmid  6087  rdgon  6662  oawordi  6747  nnmord  6795  nnmword  6796  1dom1el  7113  mapunen  7157  fidifsnen  7178  dif1en  7189  ac6sfi  7208  fissfi  7269  difinfsn  7446  2omotaplemap  7629  enq0tr  7807  distrlem4prl  7957  distrlem4pru  7958  ltaprg  7992  lelttr  8420  ltletr  8421  readdcan  8473  addcan  8513  addcan2  8514  ltadd2  8754  divmulassap  9033  indfdc  9307  xrlelttr  10224  xrltletr  10225  xaddass  10287  xleadd1a  10291  xlesubadd  10301  icoshftf1o  10409  lincmble  10422  difelfzle  10557  fzo1fzo0n0  10611  modqmuladdim  10824  modqmuladdnn0  10825  modqm1p1mod0  10832  q2submod  10842  modifeq2int  10843  modqaddmulmod  10848  seq1g  10920  seqp1g  10923  ltexp2a  11048  exple1  11052  expnlbnd2  11123  nn0ltexp2  11168  nn0leexp2  11169  mulsubdivbinom2ap  11170  expcan  11175  fiprsshashgt1  11279  hashtpgim  11318  hashtpg  11320  fun2dmnop0  11323  ccatass  11397  fzowrddc  11440  swrdclg  11443  ccatopth  11509  pfxccatin12lem2a  11520  pfxccat3  11527  maxleastb  12002  maxltsup  12006  xrltmaxsup  12047  xrmaxltsup  12048  xrmaxaddlem  12050  xrmaxadd  12051  addcn2  12100  mulcn2  12102  isumz  12180  dvdsmodexp  12586  modmulconst  12614  dvdsmod  12653  divalglemex  12713  divalg  12715  gcdass  12816  rplpwr  12828  rppwr  12829  nnwodc  12837  uzwodc  12838  rpmulgcd2  12897  rpdvds  12901  rpexp  12956  znege1  12982  prmdiveq  13042  hashgcdlem  13044  coprimeprodsq  13064  coprimeprodsq2  13065  pythagtriplem3  13074  pcdvdsb  13127  pcgcd1  13135  dvdsprmpweq  13142  pcbc  13158  ctinf  13378  nninfdc  13401  isnsgrp  13779  issubmnd  13813  mulgnn0p1  13994  mulgnnsubcl  13995  mulgneg  14001  mulgdirlem  14014  nmzsubg  14071  ghmmulg  14117  gsumsncmn  14245  ring1eq0  14459  rmodislmod  14796  lspss  14844  2idlcpblrng  14968  issubassa  15121  aspss  15127  snifpsrbagfi  15168  neiint  15388  topssnei  15405  cnptopco  15465  cnrest2  15479  cnptoprest  15482  upxp  15515  bldisj  15644  blgt0  15645  bl2in  15646  blss2ps  15649  blss2  15650  xblm  15660  blssps  15670  blss  15671  bdmopn  15747  metcnp2  15756  txmetcnp  15761  cncfmptc  15839  dvcnp2cntop  15942  dvcn  15943  ply1term  15986  dvply1  16008  logdivlti  16128  ltexp2  16194  pellexlem2  16247  bcmono  16321  lgsfvalg  16346  lgsneg  16365  lgsmod  16367  lgsdilem  16368  lgsdirprm  16375  lgsdir  16376  lgsdi  16378  lgsne0  16379