Theorem 3adant1 1015

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
3adant1	|- ( ( th /\ ph /\ ps ) -> ch )

Proof of Theorem 3adant1

Step	Hyp	Ref	Expression
1		3simpc 996	. 2 |- ( ( th /\ ph /\ ps ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( th /\ ph /\ ps ) -> ch )

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

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 980

This theorem is referenced by:  3ad2ant2  1019  3ad2ant3  1020  rsp2e  2528  sbciegft  2994  reuhyp  4473  suc11g  4557  soinxp  4697  breldmg  4834  funopg  5251  funimaexglem  5300  fex2  5385  fnreseql  5627  ftpg  5701  mpoeq3ia  5940  funexw  6113  mpofvex  6204  poxp  6233  smores3  6294  tfrlemibxssdm  6328  nndi  6487  nnmass  6488  nndir  6491  fnsnsplitdc  6506  nnaord  6510  nnaordr  6511  nnawordi  6516  nnmord  6518  ecopovtrn  6632  ecopovtrng  6635  ixpf  6720  mapxpen  6848  netap  7253  2omotaplemap  7256  ltsopi  7319  addassnqg  7381  ltsonq  7397  ltmnqg  7400  distrnq0  7458  addlocpr  7535  distrlem1prl  7581  distrlem1pru  7582  distrlem4prl  7583  distrlem4pru  7584  ltpopr  7594  ltsopr  7595  addcanprg  7615  lttrsr  7761  ltsosr  7763  ltasrg  7769  recexgt0sr  7772  mulextsr1lem  7779  mulextsr1  7780  axpre-mulext  7887  adddir  7948  axltwlin  8025  axlttrn  8026  ltleletr  8039  letr  8040  mul32  8087  mul31  8088  add32  8116  subsub23  8162  addsubass  8167  subcan2  8182  subsub2  8185  nppcan2  8188  sub32  8191  nnncan  8192  nnncan2  8194  pnpcan2  8197  subdi  8342  subdir  8343  reapcotr  8555  receuap  8626  divmulap3  8634  divrecap  8645  divrecap2  8646  divsubdirap  8665  divdivap1  8680  redivclap  8688  div2negap  8692  ltmul2  8813  lemul2  8814  lemul2a  8816  lediv1  8826  gt0div  8827  ge0div  8828  ltdivmul  8833  ltdivmul2  8835  ledivmul2  8837  uzind2  9365  nn0ind  9367  fnn0ind  9369  uz3m2nn  9573  xrletr  9808  xrre2  9821  xleadd2a  9874  xleadd1  9875  xltadd2  9877  ixxdisj  9903  iooneg  9988  iccneg  9989  icoshft  9990  icoshftf1o  9991  icodisj  9992  fzen  10043  fzrev3  10087  2ffzeq  10141  fzoaddel2  10193  elfzodifsumelfzo  10201  ssfzo12bi  10225  fzoshftral  10238  adddivflid  10292  fldiv4p1lem1div2  10305  modqmulnn  10342  modqeqmodmin  10394  frec2uzf1od  10406  expdivap  10571  shftval2  10835  mulreap  10873  absdivap  11079  absdiflt  11101  absdifle  11102  abs3dif  11114  cau3  11124  ltmininf  11243  xrmaxlesup  11267  xrltmininf  11278  xrlemininf  11279  xrminltinf  11280  geoisum1c  11528  dvdsmulc  11826  dvdsmultr1  11838  dvdsmultr2  11840  dvdssub2  11842  oexpneg  11882  divalgb  11930  ndvdsadd  11936  gcdaddm  11985  modgcd  11992  dvdsgcd  12013  dvdsgcdb  12014  gcdass  12016  mulgcd  12017  absmulgcd  12018  rpmulgcd  12027  nn0seqcvgd  12041  algcvga  12051  lcmdvds  12079  lcmdvdsb  12084  lcmass  12085  coprmdvds  12092  coprmdvds2  12093  rpmul  12098  cncongr1  12103  cncongr2  12104  prmgt1  12132  qnumdenbi  12192  coprimeprodsq  12257  pythagtriplem4  12268  pythagtriplem8  12272  pythagtriplem9  12273  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem16  12279  pcpremul  12293  pcgcd  12328  setsvala  12493  setsex  12494  ressval2  12526  isgrpi  12900  grpsubrcan  12951  grpinvsub  12952  grpsubeq0  12956  grpsubadd0sub  12957  grpnpcan  12962  opprmulg  13243  lmodvsubval2  13432  rmodislmodlem  13440  rmodislmod  13441  cncrng  13466  unopn  13508  clsss  13621  opnssneib  13659  restabs  13678  upxp  13775  blpnfctr  13942  mscl  13968  xmscl  13969  xmsge0  13970  xmseq0  13971  rpdivcxp  14335  cxpcom  14360  rplogbreexp  14374  rplogbzexp  14375  rprelogbmulexp  14377  logbleb  14382  logblt  14383  lgsneg  14428  lgsne0  14442  lgsmodeq  14449  lgsmulsqcoprm  14450  bj-peano4  14710