Theorem 3adant2 963

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 942	. 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 925

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

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

This theorem is referenced by:  3ad2ant1  965  eupickb  2030  vtoclegft  2692  eqeu  2786  suc11g  4386  soinxp  4521  funopg  5061  fnco  5135  dff1o2  5271  fnimapr  5377  fvun1  5383  fvmptt  5407  fnreseql  5423  fvpr1g  5517  fvpr2g  5518  f1elima  5566  f1ocnvfvb  5573  ovexg  5697  oprssov  5800  poxp  6011  smoiso  6081  rdgivallem  6160  nndi  6261  nndir  6265  fnsnsplitdc  6278  nnaord  6282  nnaordr  6283  nnaword  6284  nnawordi  6288  ecopovtrn  6403  ecopovtrng  6406  xpdom3m  6604  mapxpen  6618  findcard  6658  fisseneq  6696  resfnfinfinss  6703  funrnfi  6705  ltsopi  6940  addcanpig  6954  addassnqg  7002  distrnqg  7007  ltsonq  7018  ltmnqg  7021  prarloclemarch2  7039  nnanq0  7078  distrnq0  7079  distnq0r  7083  prltlu  7107  prarloclem5  7120  distrlem1prl  7202  distrlem1pru  7203  distrlem5prl  7206  distrlem5pru  7207  ltpopr  7215  ltsopr  7216  ltexprlemm  7220  ltexprlemfl  7229  ltexprlemfu  7231  lttrsr  7369  ltsosr  7371  ltasrg  7377  recexgt0sr  7380  mulextsr1lem  7386  mulextsr1  7387  axpre-mulext  7484  adddir  7540  axltwlin  7615  axlttrn  7616  ltleletr  7628  letr  7629  nnncan1  7779  npncan3  7781  pnpcan2  7783  subdi  7924  subdir  7925  reapcotr  8136  divmulap  8203  div23ap  8219  div13ap  8221  muldivdirap  8235  divsubdirap  8236  divcanap7  8249  ltmul2  8378  lemul2  8379  lemul2a  8381  lediv1  8391  ltmuldiv2  8397  lemuldiv2  8404  squeeze0  8426  nndivtr  8525  bndndx  8733  nn0n0n1ge2  8878  fnn0ind  8923  addlelt  9300  xrletr  9334  xrltne  9339  iooneg  9466  iccneg  9467  icoshft  9468  icoshftf1o  9469  zltaddlt1le  9484  fztri3or  9514  fzdcel  9515  fzen  9518  uzsubsubfz  9522  fzrevral2  9581  fzshftral  9583  fz0fzdiffz0  9602  elfzmlbp  9604  elfzo  9621  fzoaddel2  9665  fzosubel2  9667  elfzom1p1elfzo  9686  ssfzo12bi  9697  subfzo0  9714  flltdivnn0lt  9772  modqmulnn  9810  modfzo0difsn  9863  expdivap  10067  expubnd  10073  mulbinom2  10131  bernneq2  10136  shftuz  10312  shftval2  10321  abs3dif  10599  sin02gt0  11115  dvdsval2  11138  dvdscmul  11162  dvdsmulc  11163  ndvdssub  11269  rpmulgcd  11354  cncongr1  11424  cncongr2  11425  isprm3  11439  ntrin  11885  bj-peano4  12123