Theorem 3adant2 1018

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adant2

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

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

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 982

This theorem is referenced by:  3ad2ant1  1020  3imp3i2an  1185  eupickb  2126  vtoclegft  2836  eqeu  2934  ifnebibdc  3605  suc11g  4594  soinxp  4734  funopg  5293  fnco  5369  dff1o2  5512  fnimapr  5624  fvun1  5630  fvmptt  5656  fnreseql  5675  fvpr1g  5771  fvpr2g  5772  f1elima  5823  f1ocnvfvb  5830  ovexg  5959  oprssov  6069  poxp  6299  smoiso  6369  rdgivallem  6448  nndi  6553  nndir  6557  fnsnsplitdc  6572  nnaord  6576  nnaordr  6577  nnaword  6578  nnawordi  6582  ecopovtrn  6700  ecopovtrng  6703  xpdom3m  6902  mapxpen  6918  findcard  6958  fisseneq  7004  resfnfinfinss  7014  funrnfi  7017  netap  7339  2omotaplemap  7342  ltsopi  7406  addcanpig  7420  addassnqg  7468  distrnqg  7473  ltsonq  7484  ltmnqg  7487  prarloclemarch2  7505  nnanq0  7544  distrnq0  7545  distnq0r  7549  prltlu  7573  prarloclem5  7586  distrlem1prl  7668  distrlem1pru  7669  distrlem5prl  7672  distrlem5pru  7673  ltpopr  7681  ltsopr  7682  ltexprlemm  7686  ltexprlemfl  7695  ltexprlemfu  7697  lttrsr  7848  ltsosr  7850  ltasrg  7856  recexgt0sr  7859  mulextsr1lem  7866  mulextsr1  7867  axpre-mulext  7974  adddir  8036  axltwlin  8113  axlttrn  8114  ltleletr  8127  letr  8128  nnncan1  8281  npncan3  8283  pnpcan2  8285  subdi  8430  subdir  8431  reapcotr  8644  divmulap  8721  div23ap  8737  div13ap  8739  muldivdirap  8753  divsubdirap  8754  divcanap7  8767  ltmul2  8902  lemul2  8903  lemul2a  8905  lediv1  8915  ltmuldiv2  8921  lemuldiv2  8928  squeeze0  8950  nndivtr  9051  bndndx  9267  nn0n0n1ge2  9415  fnn0ind  9461  addlelt  9862  xrletr  9902  xrltne  9907  xleadd2a  9968  xleadd1  9969  xltadd2  9971  iooneg  10082  iccneg  10083  icoshft  10084  icoshftf1o  10085  zltaddlt1le  10101  fztri3or  10133  fzdcel  10134  fzen  10137  uzsubsubfz  10141  fzrevral2  10200  fzshftral  10202  fz0fzdiffz0  10224  elfzmlbp  10226  elfzo  10243  nelfzo  10246  fzoaddel2  10288  fzosubel2  10290  elfzom1p1elfzo  10309  ssfzo12bi  10320  subfzo0  10337  flltdivnn0lt  10413  modqmulnn  10453  modfzo0difsn  10506  expdivap  10701  expubnd  10707  mulbinom2  10767  bernneq2  10772  shftuz  11001  shftval2  11010  abs3dif  11289  xrmaxlesup  11443  xrltmininf  11454  xrlemininf  11455  sin02gt0  11948  dvdsval2  11974  dvdscmul  12002  dvdsmulc  12003  ndvdssub  12114  rpmulgcd  12220  cncongr1  12298  cncongr2  12299  isprm3  12313  coprimeprodsq  12453  pythagtriplem12  12471  pythagtriplem14  12473  pcmul  12497  pcdiv  12498  pcqcl  12502  pcqdiv  12503  pcdvdsb  12516  ercpbl  13035  mgmb1mgm1  13072  grpinvid1  13256  grpinvid2  13257  grpasscan1  13267  grpasscan2  13268  grpinvadd  13282  grpsubf  13283  grpsubrcan  13285  grpinvsub  13286  grpsubeq0  13290  grpsubadd0sub  13291  grppncan  13295  grpnpcan  13296  mulgnn0p1  13341  mulgaddcomlem  13353  mulginvcom  13355  mulginvinv  13356  subgsubcl  13393  subgsub  13394  eqglact  13433  quselbasg  13438  quseccl0g  13439  qussub  13445  ghmsub  13459  subcmnd  13541  srg1zr  13621  dvrcl  13769  unitdvcl  13770  dvrcan1  13774  dvrcan3  13775  dvreq1  13776  subrgdv  13872  lmodvsubval2  13976  lmodprop2d  13982  zndvds  14283  ntrin  14468  elnei  14496  cnrest2  14580  psmetsym  14673  psmetge0  14675  xmetge0  14709  xmetsym  14712  cnmet  14874  rpcxpsub  15252  rpdivcxp  15255  logbleb  15305  logblt  15306  lgsmodeq  15394  lgsmulsqcoprm  15395  gausslemma2dlem1a  15407  2lgsoddprmlem2  15455  bj-peano4  15709