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  3618  frirrg  4410  fcofo  5871  acexmid  5961  rdgon  6490  oawordi  6573  nnmord  6621  nnmword  6622  fidifsnen  6988  dif1en  6997  ac6sfi  7016  difinfsn  7223  2omotaplemap  7399  enq0tr  7577  distrlem4prl  7727  distrlem4pru  7728  ltaprg  7762  lelttr  8191  ltletr  8192  readdcan  8242  addcan  8282  addcan2  8283  ltadd2  8522  divmulassap  8798  xrlelttr  9958  xrltletr  9959  xaddass  10021  xleadd1a  10025  xlesubadd  10035  icoshftf1o  10143  difelfzle  10286  fzo1fzo0n0  10339  modqmuladdim  10544  modqmuladdnn0  10545  modqm1p1mod0  10552  q2submod  10562  modifeq2int  10563  modqaddmulmod  10568  seq1g  10640  seqp1g  10643  ltexp2a  10768  exple1  10772  expnlbnd2  10842  nn0ltexp2  10886  nn0leexp2  10887  mulsubdivbinom2ap  10888  expcan  10893  fiprsshashgt1  10994  fun2dmnop0  11024  ccatass  11097  fzowrddc  11133  swrdclg  11136  ccatopth  11202  maxleastb  11610  maxltsup  11614  xrltmaxsup  11653  xrmaxltsup  11654  xrmaxaddlem  11656  xrmaxadd  11657  addcn2  11706  mulcn2  11708  isumz  11785  dvdsmodexp  12191  modmulconst  12219  dvdsmod  12258  divalglemex  12318  divalg  12320  gcdass  12421  rplpwr  12433  rppwr  12434  nnwodc  12442  uzwodc  12443  rpmulgcd2  12502  rpdvds  12506  rpexp  12560  znege1  12585  prmdiveq  12643  hashgcdlem  12645  coprimeprodsq  12665  coprimeprodsq2  12666  pythagtriplem3  12675  pcdvdsb  12728  pcgcd1  12736  dvdsprmpweq  12743  pcbc  12759  ctinf  12886  nninfdc  12909  isnsgrp  13323  issubmnd  13359  mulgnn0p1  13554  mulgnnsubcl  13555  mulgneg  13561  mulgdirlem  13574  nmzsubg  13631  ghmmulg  13677  ring1eq0  13895  rmodislmod  14198  lspss  14246  2idlcpblrng  14370  neiint  14702  topssnei  14719  cnptopco  14779  cnrest2  14793  cnptoprest  14796  upxp  14829  bldisj  14958  blgt0  14959  bl2in  14960  blss2ps  14963  blss2  14964  xblm  14974  blssps  14984  blss  14985  bdmopn  15061  metcnp2  15070  txmetcnp  15075  cncfmptc  15153  dvcnp2cntop  15256  dvcn  15257  ply1term  15300  dvply1  15322  logdivlti  15438  ltexp2  15498  lgsfvalg  15567  lgsneg  15586  lgsmod  15588  lgsdilem  15589  lgsdirprm  15596  lgsdir  15597  lgsdi  15599  lgsne0  15600  umgrnloopvv  15795  1dom1el  16096