Theorem simpl3 1028

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

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

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 1006

This theorem is referenced by:  simpll3  1064  simprl3  1070  simp1l3  1118  simp2l3  1124  simp3l3  1130  3anandirs  1384  ifnetruedc  3649  frirrg  4447  fcofo  5924  acexmid  6016  rdgon  6551  oawordi  6636  nnmord  6684  nnmword  6685  1dom1el  6992  fidifsnen  7056  dif1en  7067  ac6sfi  7086  difinfsn  7298  2omotaplemap  7475  enq0tr  7653  distrlem4prl  7803  distrlem4pru  7804  ltaprg  7838  lelttr  8267  ltletr  8268  readdcan  8318  addcan  8358  addcan2  8359  ltadd2  8598  divmulassap  8874  xrlelttr  10040  xrltletr  10041  xaddass  10103  xleadd1a  10107  xlesubadd  10117  icoshftf1o  10225  difelfzle  10368  fzo1fzo0n0  10421  modqmuladdim  10628  modqmuladdnn0  10629  modqm1p1mod0  10636  q2submod  10646  modifeq2int  10647  modqaddmulmod  10652  seq1g  10724  seqp1g  10727  ltexp2a  10852  exple1  10856  expnlbnd2  10926  nn0ltexp2  10970  nn0leexp2  10971  mulsubdivbinom2ap  10972  expcan  10977  fiprsshashgt1  11080  fun2dmnop0  11110  ccatass  11184  fzowrddc  11227  swrdclg  11230  ccatopth  11296  pfxccatin12lem2a  11307  pfxccat3  11314  maxleastb  11774  maxltsup  11778  xrltmaxsup  11817  xrmaxltsup  11818  xrmaxaddlem  11820  xrmaxadd  11821  addcn2  11870  mulcn2  11872  isumz  11949  dvdsmodexp  12355  modmulconst  12383  dvdsmod  12422  divalglemex  12482  divalg  12484  gcdass  12585  rplpwr  12597  rppwr  12598  nnwodc  12606  uzwodc  12607  rpmulgcd2  12666  rpdvds  12670  rpexp  12724  znege1  12749  prmdiveq  12807  hashgcdlem  12809  coprimeprodsq  12829  coprimeprodsq2  12830  pythagtriplem3  12839  pcdvdsb  12892  pcgcd1  12900  dvdsprmpweq  12907  pcbc  12923  ctinf  13050  nninfdc  13073  isnsgrp  13488  issubmnd  13524  mulgnn0p1  13719  mulgnnsubcl  13720  mulgneg  13726  mulgdirlem  13739  nmzsubg  13796  ghmmulg  13842  ring1eq0  14060  rmodislmod  14364  lspss  14412  2idlcpblrng  14536  neiint  14868  topssnei  14885  cnptopco  14945  cnrest2  14959  cnptoprest  14962  upxp  14995  bldisj  15124  blgt0  15125  bl2in  15126  blss2ps  15129  blss2  15130  xblm  15140  blssps  15150  blss  15151  bdmopn  15227  metcnp2  15236  txmetcnp  15241  cncfmptc  15319  dvcnp2cntop  15422  dvcn  15423  ply1term  15466  dvply1  15488  logdivlti  15604  ltexp2  15664  lgsfvalg  15733  lgsneg  15752  lgsmod  15754  lgsdilem  15755  lgsdirprm  15762  lgsdir  15763  lgsdi  15765  lgsne0  15766