Theorem simpl3 1005

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

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

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 983

This theorem is referenced by:  simpll3  1041  simprl3  1047  simp1l3  1095  simp2l3  1101  simp3l3  1107  3anandirs  1361  ifnetruedc  3613  frirrg  4397  fcofo  5853  acexmid  5943  rdgon  6472  oawordi  6555  nnmord  6603  nnmword  6604  fidifsnen  6967  dif1en  6976  ac6sfi  6995  difinfsn  7202  2omotaplemap  7369  enq0tr  7547  distrlem4prl  7697  distrlem4pru  7698  ltaprg  7732  lelttr  8161  ltletr  8162  readdcan  8212  addcan  8252  addcan2  8253  ltadd2  8492  divmulassap  8768  xrlelttr  9928  xrltletr  9929  xaddass  9991  xleadd1a  9995  xlesubadd  10005  icoshftf1o  10113  difelfzle  10256  fzo1fzo0n0  10307  modqmuladdim  10512  modqmuladdnn0  10513  modqm1p1mod0  10520  q2submod  10530  modifeq2int  10531  modqaddmulmod  10536  seq1g  10608  seqp1g  10611  ltexp2a  10736  exple1  10740  expnlbnd2  10810  nn0ltexp2  10854  nn0leexp2  10855  mulsubdivbinom2ap  10856  expcan  10861  fiprsshashgt1  10962  fun2dmnop0  10992  ccatass  11064  fzowrddc  11100  swrdclg  11103  maxleastb  11525  maxltsup  11529  xrltmaxsup  11568  xrmaxltsup  11569  xrmaxaddlem  11571  xrmaxadd  11572  addcn2  11621  mulcn2  11623  isumz  11700  dvdsmodexp  12106  modmulconst  12134  dvdsmod  12173  divalglemex  12233  divalg  12235  gcdass  12336  rplpwr  12348  rppwr  12349  nnwodc  12357  uzwodc  12358  rpmulgcd2  12417  rpdvds  12421  rpexp  12475  znege1  12500  prmdiveq  12558  hashgcdlem  12560  coprimeprodsq  12580  coprimeprodsq2  12581  pythagtriplem3  12590  pcdvdsb  12643  pcgcd1  12651  dvdsprmpweq  12658  pcbc  12674  ctinf  12801  nninfdc  12824  isnsgrp  13238  issubmnd  13274  mulgnn0p1  13469  mulgnnsubcl  13470  mulgneg  13476  mulgdirlem  13489  nmzsubg  13546  ghmmulg  13592  ring1eq0  13810  rmodislmod  14113  lspss  14161  2idlcpblrng  14285  neiint  14617  topssnei  14634  cnptopco  14694  cnrest2  14708  cnptoprest  14711  upxp  14744  bldisj  14873  blgt0  14874  bl2in  14875  blss2ps  14878  blss2  14879  xblm  14889  blssps  14899  blss  14900  bdmopn  14976  metcnp2  14985  txmetcnp  14990  cncfmptc  15068  dvcnp2cntop  15171  dvcn  15172  ply1term  15215  dvply1  15237  logdivlti  15353  ltexp2  15413  lgsfvalg  15482  lgsneg  15501  lgsmod  15503  lgsdilem  15504  lgsdirprm  15511  lgsdir  15512  lgsdi  15514  lgsne0  15515  1dom1el  15927