Theorem 3adant2 1016

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 995	. 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 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:  3ad2ant1  1018  3imp3i2an  1183  eupickb  2107  vtoclegft  2809  eqeu  2907  suc11g  4556  soinxp  4696  funopg  5250  fnco  5324  dff1o2  5466  fnimapr  5576  fvun1  5582  fvmptt  5607  fnreseql  5626  fvpr1g  5722  fvpr2g  5723  f1elima  5773  f1ocnvfvb  5780  ovexg  5908  oprssov  6015  poxp  6232  smoiso  6302  rdgivallem  6381  nndi  6486  nndir  6490  fnsnsplitdc  6505  nnaord  6509  nnaordr  6510  nnaword  6511  nnawordi  6515  ecopovtrn  6631  ecopovtrng  6634  xpdom3m  6833  mapxpen  6847  findcard  6887  fisseneq  6930  resfnfinfinss  6938  funrnfi  6940  netap  7252  2omotaplemap  7255  ltsopi  7318  addcanpig  7332  addassnqg  7380  distrnqg  7385  ltsonq  7396  ltmnqg  7399  prarloclemarch2  7417  nnanq0  7456  distrnq0  7457  distnq0r  7461  prltlu  7485  prarloclem5  7498  distrlem1prl  7580  distrlem1pru  7581  distrlem5prl  7584  distrlem5pru  7585  ltpopr  7593  ltsopr  7594  ltexprlemm  7598  ltexprlemfl  7607  ltexprlemfu  7609  lttrsr  7760  ltsosr  7762  ltasrg  7768  recexgt0sr  7771  mulextsr1lem  7778  mulextsr1  7779  axpre-mulext  7886  adddir  7947  axltwlin  8023  axlttrn  8024  ltleletr  8037  letr  8038  nnncan1  8191  npncan3  8193  pnpcan2  8195  subdi  8340  subdir  8341  reapcotr  8553  divmulap  8630  div23ap  8646  div13ap  8648  muldivdirap  8662  divsubdirap  8663  divcanap7  8676  ltmul2  8811  lemul2  8812  lemul2a  8814  lediv1  8824  ltmuldiv2  8830  lemuldiv2  8837  squeeze0  8859  nndivtr  8959  bndndx  9173  nn0n0n1ge2  9321  fnn0ind  9367  addlelt  9766  xrletr  9806  xrltne  9811  xleadd2a  9872  xleadd1  9873  xltadd2  9875  iooneg  9986  iccneg  9987  icoshft  9988  icoshftf1o  9989  zltaddlt1le  10005  fztri3or  10036  fzdcel  10037  fzen  10040  uzsubsubfz  10044  fzrevral2  10103  fzshftral  10105  fz0fzdiffz0  10127  elfzmlbp  10129  elfzo  10146  fzoaddel2  10190  fzosubel2  10192  elfzom1p1elfzo  10211  ssfzo12bi  10222  subfzo0  10239  flltdivnn0lt  10301  modqmulnn  10339  modfzo0difsn  10392  expdivap  10568  expubnd  10574  mulbinom2  10633  bernneq2  10638  shftuz  10821  shftval2  10830  abs3dif  11109  xrmaxlesup  11262  xrltmininf  11273  xrlemininf  11274  sin02gt0  11766  dvdsval2  11792  dvdscmul  11820  dvdsmulc  11821  ndvdssub  11929  rpmulgcd  12021  cncongr1  12097  cncongr2  12098  isprm3  12112  coprimeprodsq  12251  pythagtriplem12  12269  pythagtriplem14  12271  pcmul  12295  pcdiv  12296  pcqcl  12300  pcqdiv  12301  pcdvdsb  12313  ercpbl  12744  mgmb1mgm1  12781  grpinvid1  12918  grpinvid2  12919  grpasscan1  12927  grpasscan2  12928  grpinvadd  12942  grpsubf  12943  grpsubrcan  12945  grpinvsub  12946  grpsubeq0  12950  grpsubadd0sub  12951  grppncan  12955  grpnpcan  12956  mulgnn0p1  12988  mulgaddcomlem  12999  mulginvcom  13001  mulginvinv  13002  subgsubcl  13038  subgsub  13039  eqglact  13077  subcmnd  13122  srg1zr  13163  dvrcl  13297  unitdvcl  13298  dvrcan1  13302  dvrcan3  13303  dvreq1  13304  subrgdv  13359  ntrin  13555  elnei  13583  cnrest2  13667  psmetsym  13760  psmetge0  13762  xmetge0  13796  xmetsym  13799  cnmet  13961  rpcxpsub  14260  rpdivcxp  14263  logbleb  14310  logblt  14311  lgsmodeq  14377  lgsmulsqcoprm  14378  bj-peano4  14627