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  3646  frirrg  4441  fcofo  5914  acexmid  6006  rdgon  6538  oawordi  6623  nnmord  6671  nnmword  6672  fidifsnen  7040  dif1en  7049  ac6sfi  7068  difinfsn  7278  2omotaplemap  7454  enq0tr  7632  distrlem4prl  7782  distrlem4pru  7783  ltaprg  7817  lelttr  8246  ltletr  8247  readdcan  8297  addcan  8337  addcan2  8338  ltadd2  8577  divmulassap  8853  xrlelttr  10014  xrltletr  10015  xaddass  10077  xleadd1a  10081  xlesubadd  10091  icoshftf1o  10199  difelfzle  10342  fzo1fzo0n0  10395  modqmuladdim  10601  modqmuladdnn0  10602  modqm1p1mod0  10609  q2submod  10619  modifeq2int  10620  modqaddmulmod  10625  seq1g  10697  seqp1g  10700  ltexp2a  10825  exple1  10829  expnlbnd2  10899  nn0ltexp2  10943  nn0leexp2  10944  mulsubdivbinom2ap  10945  expcan  10950  fiprsshashgt1  11052  fun2dmnop0  11082  ccatass  11156  fzowrddc  11194  swrdclg  11197  ccatopth  11263  pfxccatin12lem2a  11274  pfxccat3  11281  maxleastb  11740  maxltsup  11744  xrltmaxsup  11783  xrmaxltsup  11784  xrmaxaddlem  11786  xrmaxadd  11787  addcn2  11836  mulcn2  11838  isumz  11915  dvdsmodexp  12321  modmulconst  12349  dvdsmod  12388  divalglemex  12448  divalg  12450  gcdass  12551  rplpwr  12563  rppwr  12564  nnwodc  12572  uzwodc  12573  rpmulgcd2  12632  rpdvds  12636  rpexp  12690  znege1  12715  prmdiveq  12773  hashgcdlem  12775  coprimeprodsq  12795  coprimeprodsq2  12796  pythagtriplem3  12805  pcdvdsb  12858  pcgcd1  12866  dvdsprmpweq  12873  pcbc  12889  ctinf  13016  nninfdc  13039  isnsgrp  13454  issubmnd  13490  mulgnn0p1  13685  mulgnnsubcl  13686  mulgneg  13692  mulgdirlem  13705  nmzsubg  13762  ghmmulg  13808  ring1eq0  14026  rmodislmod  14330  lspss  14378  2idlcpblrng  14502  neiint  14834  topssnei  14851  cnptopco  14911  cnrest2  14925  cnptoprest  14928  upxp  14961  bldisj  15090  blgt0  15091  bl2in  15092  blss2ps  15095  blss2  15096  xblm  15106  blssps  15116  blss  15117  bdmopn  15193  metcnp2  15202  txmetcnp  15207  cncfmptc  15285  dvcnp2cntop  15388  dvcn  15389  ply1term  15432  dvply1  15454  logdivlti  15570  ltexp2  15630  lgsfvalg  15699  lgsneg  15718  lgsmod  15720  lgsdilem  15721  lgsdirprm  15728  lgsdir  15729  lgsdi  15731  lgsne0  15732  1dom1el  16409