Theorem simpl3 1029

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

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

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 1007

This theorem is referenced by:  simpll3  1065  simprl3  1071  simp1l3  1119  simp2l3  1125  simp3l3  1131  3anandirs  1385  ifnetruedc  3670  frirrg  4476  fcofo  5963  acexmid  6057  rdgon  6630  oawordi  6715  nnmord  6763  nnmword  6764  1dom1el  7073  mapunen  7117  fidifsnen  7138  dif1en  7149  ac6sfi  7168  fissfi  7229  difinfsn  7404  2omotaplemap  7587  enq0tr  7765  distrlem4prl  7915  distrlem4pru  7916  ltaprg  7950  lelttr  8378  ltletr  8379  readdcan  8429  addcan  8469  addcan2  8470  ltadd2  8710  divmulassap  8986  xrlelttr  10158  xrltletr  10159  xaddass  10221  xleadd1a  10225  xlesubadd  10235  icoshftf1o  10343  lincmble  10356  difelfzle  10490  fzo1fzo0n0  10544  modqmuladdim  10753  modqmuladdnn0  10754  modqm1p1mod0  10761  q2submod  10771  modifeq2int  10772  modqaddmulmod  10777  seq1g  10849  seqp1g  10852  ltexp2a  10977  exple1  10981  expnlbnd2  11052  nn0ltexp2  11096  nn0leexp2  11097  mulsubdivbinom2ap  11098  expcan  11103  fiprsshashgt1  11207  hashtpgim  11242  hashtpg  11244  fun2dmnop0  11247  ccatass  11321  fzowrddc  11364  swrdclg  11367  ccatopth  11433  pfxccatin12lem2a  11444  pfxccat3  11451  maxleastb  11924  maxltsup  11928  xrltmaxsup  11967  xrmaxltsup  11968  xrmaxaddlem  11970  xrmaxadd  11971  addcn2  12020  mulcn2  12022  isumz  12100  dvdsmodexp  12506  modmulconst  12534  dvdsmod  12573  divalglemex  12633  divalg  12635  gcdass  12736  rplpwr  12748  rppwr  12749  nnwodc  12757  uzwodc  12758  rpmulgcd2  12817  rpdvds  12821  rpexp  12875  znege1  12900  prmdiveq  12958  hashgcdlem  12960  coprimeprodsq  12980  coprimeprodsq2  12981  pythagtriplem3  12990  pcdvdsb  13043  pcgcd1  13051  dvdsprmpweq  13058  pcbc  13074  ctinf  13265  nninfdc  13288  isnsgrp  13669  issubmnd  13703  mulgnn0p1  13886  mulgnnsubcl  13887  mulgneg  13893  mulgdirlem  13906  nmzsubg  13963  ghmmulg  14009  gfsumsn  14107  ring1eq0  14291  rmodislmod  14625  lspss  14673  2idlcpblrng  14797  neiint  15136  topssnei  15153  cnptopco  15213  cnrest2  15227  cnptoprest  15230  upxp  15263  bldisj  15392  blgt0  15393  bl2in  15394  blss2ps  15397  blss2  15398  xblm  15408  blssps  15418  blss  15419  bdmopn  15495  metcnp2  15504  txmetcnp  15509  cncfmptc  15587  dvcnp2cntop  15690  dvcn  15691  ply1term  15734  dvply1  15756  logdivlti  15872  ltexp2  15932  pellexlem2  15972  lgsfvalg  16004  lgsneg  16023  lgsmod  16025  lgsdilem  16026  lgsdirprm  16033  lgsdir  16034  lgsdi  16036  lgsne0  16037