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  2123  vtoclegft  2832  eqeu  2930  ifnebibdc  3600  suc11g  4589  soinxp  4729  funopg  5288  fnco  5362  dff1o2  5505  fnimapr  5617  fvun1  5623  fvmptt  5649  fnreseql  5668  fvpr1g  5764  fvpr2g  5765  f1elima  5816  f1ocnvfvb  5823  ovexg  5952  oprssov  6060  poxp  6285  smoiso  6355  rdgivallem  6434  nndi  6539  nndir  6543  fnsnsplitdc  6558  nnaord  6562  nnaordr  6563  nnaword  6564  nnawordi  6568  ecopovtrn  6686  ecopovtrng  6689  xpdom3m  6888  mapxpen  6904  findcard  6944  fisseneq  6988  resfnfinfinss  6998  funrnfi  7001  netap  7314  2omotaplemap  7317  ltsopi  7380  addcanpig  7394  addassnqg  7442  distrnqg  7447  ltsonq  7458  ltmnqg  7461  prarloclemarch2  7479  nnanq0  7518  distrnq0  7519  distnq0r  7523  prltlu  7547  prarloclem5  7560  distrlem1prl  7642  distrlem1pru  7643  distrlem5prl  7646  distrlem5pru  7647  ltpopr  7655  ltsopr  7656  ltexprlemm  7660  ltexprlemfl  7669  ltexprlemfu  7671  lttrsr  7822  ltsosr  7824  ltasrg  7830  recexgt0sr  7833  mulextsr1lem  7840  mulextsr1  7841  axpre-mulext  7948  adddir  8010  axltwlin  8087  axlttrn  8088  ltleletr  8101  letr  8102  nnncan1  8255  npncan3  8257  pnpcan2  8259  subdi  8404  subdir  8405  reapcotr  8617  divmulap  8694  div23ap  8710  div13ap  8712  muldivdirap  8726  divsubdirap  8727  divcanap7  8740  ltmul2  8875  lemul2  8876  lemul2a  8878  lediv1  8888  ltmuldiv2  8894  lemuldiv2  8901  squeeze0  8923  nndivtr  9024  bndndx  9239  nn0n0n1ge2  9387  fnn0ind  9433  addlelt  9834  xrletr  9874  xrltne  9879  xleadd2a  9940  xleadd1  9941  xltadd2  9943  iooneg  10054  iccneg  10055  icoshft  10056  icoshftf1o  10057  zltaddlt1le  10073  fztri3or  10105  fzdcel  10106  fzen  10109  uzsubsubfz  10113  fzrevral2  10172  fzshftral  10174  fz0fzdiffz0  10196  elfzmlbp  10198  elfzo  10215  nelfzo  10218  fzoaddel2  10260  fzosubel2  10262  elfzom1p1elfzo  10281  ssfzo12bi  10292  subfzo0  10309  flltdivnn0lt  10373  modqmulnn  10413  modfzo0difsn  10466  expdivap  10661  expubnd  10667  mulbinom2  10727  bernneq2  10732  shftuz  10961  shftval2  10970  abs3dif  11249  xrmaxlesup  11402  xrltmininf  11413  xrlemininf  11414  sin02gt0  11907  dvdsval2  11933  dvdscmul  11961  dvdsmulc  11962  ndvdssub  12071  rpmulgcd  12163  cncongr1  12241  cncongr2  12242  isprm3  12256  coprimeprodsq  12395  pythagtriplem12  12413  pythagtriplem14  12415  pcmul  12439  pcdiv  12440  pcqcl  12444  pcqdiv  12445  pcdvdsb  12458  ercpbl  12914  mgmb1mgm1  12951  grpinvid1  13124  grpinvid2  13125  grpasscan1  13135  grpasscan2  13136  grpinvadd  13150  grpsubf  13151  grpsubrcan  13153  grpinvsub  13154  grpsubeq0  13158  grpsubadd0sub  13159  grppncan  13163  grpnpcan  13164  mulgnn0p1  13203  mulgaddcomlem  13215  mulginvcom  13217  mulginvinv  13218  subgsubcl  13255  subgsub  13256  eqglact  13295  quselbasg  13300  quseccl0g  13301  qussub  13307  ghmsub  13321  subcmnd  13403  srg1zr  13483  dvrcl  13631  unitdvcl  13632  dvrcan1  13636  dvrcan3  13637  dvreq1  13638  subrgdv  13734  lmodvsubval2  13838  lmodprop2d  13844  zndvds  14137  ntrin  14292  elnei  14320  cnrest2  14404  psmetsym  14497  psmetge0  14499  xmetge0  14533  xmetsym  14536  cnmet  14698  rpcxpsub  15043  rpdivcxp  15046  logbleb  15093  logblt  15094  lgsmodeq  15161  lgsmulsqcoprm  15162  gausslemma2dlem1a  15174  2lgsoddprmlem2  15194  bj-peano4  15447