Theorem 3adant2 1001

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 980	. 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 103   /\ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  3ad2ant1  1003  eupickb  2081  vtoclegft  2761  eqeu  2858  suc11g  4480  soinxp  4617  funopg  5165  fnco  5239  dff1o2  5380  fnimapr  5489  fvun1  5495  fvmptt  5520  fnreseql  5538  fvpr1g  5634  fvpr2g  5635  f1elima  5682  f1ocnvfvb  5689  ovexg  5813  oprssov  5920  poxp  6137  smoiso  6207  rdgivallem  6286  nndi  6390  nndir  6394  fnsnsplitdc  6409  nnaord  6413  nnaordr  6414  nnaword  6415  nnawordi  6419  ecopovtrn  6534  ecopovtrng  6537  xpdom3m  6736  mapxpen  6750  findcard  6790  fisseneq  6828  resfnfinfinss  6836  funrnfi  6838  ltsopi  7152  addcanpig  7166  addassnqg  7214  distrnqg  7219  ltsonq  7230  ltmnqg  7233  prarloclemarch2  7251  nnanq0  7290  distrnq0  7291  distnq0r  7295  prltlu  7319  prarloclem5  7332  distrlem1prl  7414  distrlem1pru  7415  distrlem5prl  7418  distrlem5pru  7419  ltpopr  7427  ltsopr  7428  ltexprlemm  7432  ltexprlemfl  7441  ltexprlemfu  7443  lttrsr  7594  ltsosr  7596  ltasrg  7602  recexgt0sr  7605  mulextsr1lem  7612  mulextsr1  7613  axpre-mulext  7720  adddir  7781  axltwlin  7856  axlttrn  7857  ltleletr  7870  letr  7871  nnncan1  8022  npncan3  8024  pnpcan2  8026  subdi  8171  subdir  8172  reapcotr  8384  divmulap  8459  div23ap  8475  div13ap  8477  muldivdirap  8491  divsubdirap  8492  divcanap7  8505  ltmul2  8638  lemul2  8639  lemul2a  8641  lediv1  8651  ltmuldiv2  8657  lemuldiv2  8664  squeeze0  8686  nndivtr  8786  bndndx  9000  nn0n0n1ge2  9145  fnn0ind  9191  addlelt  9585  xrletr  9621  xrltne  9626  xleadd2a  9687  xleadd1  9688  xltadd2  9690  iooneg  9801  iccneg  9802  icoshft  9803  icoshftf1o  9804  zltaddlt1le  9820  fztri3or  9850  fzdcel  9851  fzen  9854  uzsubsubfz  9858  fzrevral2  9917  fzshftral  9919  fz0fzdiffz0  9938  elfzmlbp  9940  elfzo  9957  fzoaddel2  10001  fzosubel2  10003  elfzom1p1elfzo  10022  ssfzo12bi  10033  subfzo0  10050  flltdivnn0lt  10108  modqmulnn  10146  modfzo0difsn  10199  expdivap  10375  expubnd  10381  mulbinom2  10439  bernneq2  10444  shftuz  10621  shftval2  10630  abs3dif  10909  xrmaxlesup  11060  xrltmininf  11071  xrlemininf  11072  sin02gt0  11506  dvdsval2  11532  dvdscmul  11556  dvdsmulc  11557  ndvdssub  11663  rpmulgcd  11750  cncongr1  11820  cncongr2  11821  isprm3  11835  ntrin  12332  elnei  12360  cnrest2  12444  psmetsym  12537  psmetge0  12539  xmetge0  12573  xmetsym  12576  cnmet  12738  rpcxpsub  13037  rpdivcxp  13040  logbleb  13086  logblt  13087  bj-peano4  13324