Theorem simpl3 1026

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

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

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 1004

This theorem is referenced by:  simpll3  1062  simprl3  1068  simp1l3  1116  simp2l3  1122  simp3l3  1128  3anandirs  1382  ifnetruedc  3647  frirrg  4445  fcofo  5920  acexmid  6012  rdgon  6547  oawordi  6632  nnmord  6680  nnmword  6681  1dom1el  6988  fidifsnen  7052  dif1en  7061  ac6sfi  7080  difinfsn  7290  2omotaplemap  7466  enq0tr  7644  distrlem4prl  7794  distrlem4pru  7795  ltaprg  7829  lelttr  8258  ltletr  8259  readdcan  8309  addcan  8349  addcan2  8350  ltadd2  8589  divmulassap  8865  xrlelttr  10031  xrltletr  10032  xaddass  10094  xleadd1a  10098  xlesubadd  10108  icoshftf1o  10216  difelfzle  10359  fzo1fzo0n0  10412  modqmuladdim  10619  modqmuladdnn0  10620  modqm1p1mod0  10627  q2submod  10637  modifeq2int  10638  modqaddmulmod  10643  seq1g  10715  seqp1g  10718  ltexp2a  10843  exple1  10847  expnlbnd2  10917  nn0ltexp2  10961  nn0leexp2  10962  mulsubdivbinom2ap  10963  expcan  10968  fiprsshashgt1  11071  fun2dmnop0  11101  ccatass  11175  fzowrddc  11218  swrdclg  11221  ccatopth  11287  pfxccatin12lem2a  11298  pfxccat3  11305  maxleastb  11765  maxltsup  11769  xrltmaxsup  11808  xrmaxltsup  11809  xrmaxaddlem  11811  xrmaxadd  11812  addcn2  11861  mulcn2  11863  isumz  11940  dvdsmodexp  12346  modmulconst  12374  dvdsmod  12413  divalglemex  12473  divalg  12475  gcdass  12576  rplpwr  12588  rppwr  12589  nnwodc  12597  uzwodc  12598  rpmulgcd2  12657  rpdvds  12661  rpexp  12715  znege1  12740  prmdiveq  12798  hashgcdlem  12800  coprimeprodsq  12820  coprimeprodsq2  12821  pythagtriplem3  12830  pcdvdsb  12883  pcgcd1  12891  dvdsprmpweq  12898  pcbc  12914  ctinf  13041  nninfdc  13064  isnsgrp  13479  issubmnd  13515  mulgnn0p1  13710  mulgnnsubcl  13711  mulgneg  13717  mulgdirlem  13730  nmzsubg  13787  ghmmulg  13833  ring1eq0  14051  rmodislmod  14355  lspss  14403  2idlcpblrng  14527  neiint  14859  topssnei  14876  cnptopco  14936  cnrest2  14950  cnptoprest  14953  upxp  14986  bldisj  15115  blgt0  15116  bl2in  15117  blss2ps  15120  blss2  15121  xblm  15131  blssps  15141  blss  15142  bdmopn  15218  metcnp2  15227  txmetcnp  15232  cncfmptc  15310  dvcnp2cntop  15413  dvcn  15414  ply1term  15457  dvply1  15479  logdivlti  15595  ltexp2  15655  lgsfvalg  15724  lgsneg  15743  lgsmod  15745  lgsdilem  15746  lgsdirprm  15753  lgsdir  15754  lgsdi  15756  lgsne0  15757