Theorem 3adant2 1043

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 1022	. 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 1005

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 1007

This theorem is referenced by:  3ad2ant1  1045  3imp3i2an  1210  eupickb  2164  vtoclegft  2891  eqeu  2990  ifnebibdc  3672  suc11g  4684  soinxp  4825  funopg  5391  fnco  5471  dff1o2  5624  fnimapr  5742  fvun1  5748  fvmptt  5774  fnreseql  5793  fvpr1g  5895  fvpr2g  5896  f1elima  5952  f1ocnvfvb  5959  ovexg  6092  oprssov  6204  poxp  6441  smoiso  6546  rdgivallem  6625  nndi  6732  nndir  6736  fnsnsplitdc  6751  nnaord  6755  nnaordr  6756  nnaword  6757  nnawordi  6761  ecopovtrn  6879  ecopovtrng  6882  mapsnd  6936  xpdom3m  7098  mapxpen  7114  findcard  7158  fisseneq  7208  resfnfinfinss  7219  funrnfi  7222  netap  7584  2omotaplemap  7587  ltsopi  7651  addcanpig  7665  addassnqg  7713  distrnqg  7718  ltsonq  7729  ltmnqg  7732  prarloclemarch2  7750  nnanq0  7789  distrnq0  7790  distnq0r  7794  prltlu  7818  prarloclem5  7831  distrlem1prl  7913  distrlem1pru  7914  distrlem5prl  7917  distrlem5pru  7918  ltpopr  7926  ltsopr  7927  ltexprlemm  7931  ltexprlemfl  7940  ltexprlemfu  7942  lttrsr  8093  ltsosr  8095  ltasrg  8101  recexgt0sr  8104  mulextsr1lem  8111  mulextsr1  8112  axpre-mulext  8219  adddir  8281  axltwlin  8357  axlttrn  8358  ltleletr  8371  letr  8372  nnncan1  8525  npncan3  8527  pnpcan2  8529  subdi  8675  subdir  8676  reapcotr  8889  divmulap  8966  div23ap  8982  div13ap  8984  muldivdirap  8998  divsubdirap  8999  divcanap7  9012  ltmul2  9147  lemul2  9148  lemul2a  9150  lediv1  9160  ltmuldiv2  9166  lemuldiv2  9173  squeeze0  9195  nndivtr  9296  bndndx  9512  nn0n0n1ge2  9665  fnn0ind  9712  addlelt  10119  xrletr  10160  xrltne  10165  xleadd2a  10226  xleadd1  10227  xltadd2  10229  iooneg  10340  iccneg  10341  icoshft  10342  icoshftf1o  10343  zltaddlt1le  10360  fztri3or  10393  fzdcel  10394  fzen  10397  uzsubsubfz  10401  fzrevral2  10462  fzshftral  10464  fz0fzdiffz0  10486  elfzmlbp  10488  elfzo  10505  nelfzo  10508  fzoaddel2  10557  fzosubel2  10562  elfzom1p1elfzo  10581  ssfzo12bi  10592  subfzo0  10610  flltdivnn0lt  10688  modqmulnn  10728  modfzo0difsn  10781  expdivap  10976  expubnd  10982  mulbinom2  11042  bernneq2  11048  ccatval1  11310  ccatval3  11312  ccatfv0  11316  ccatval1lsw  11317  ccatws1lenp1bg  11348  pfxsuffeqwrdeq  11415  pfxsuff1eqwrdeq  11416  swrdswrd  11422  pfxpfx  11425  wrd2ind  11440  swrdccatin1  11442  pfxccatin12lem1  11445  swrdccatin2  11446  pfxccatin12lem3  11449  swrdccat  11452  pfxccatpfx1  11453  pfxccatpfx2  11454  swrdccat3blem  11456  shftuz  11527  shftval2  11536  abs3dif  11815  xrmaxlesup  11969  xrltmininf  11980  xrlemininf  11981  sin02gt0  12475  dvdsval2  12501  dvdscmul  12529  dvdsmulc  12530  ndvdssub  12641  rpmulgcd  12747  cncongr1  12825  cncongr2  12826  isprm3  12840  coprimeprodsq  12980  pythagtriplem12  12998  pythagtriplem14  13000  pcmul  13024  pcdiv  13025  pcqcl  13029  pcqdiv  13030  pcdvdsb  13043  ercpbl  13595  mgmb1mgm1  13631  grpinvid1  13807  grpinvid2  13808  grpasscan1  13818  grpasscan2  13819  grpinvadd  13833  grpsubf  13834  grpsubrcan  13836  grpinvsub  13837  grpsubeq0  13841  grpsubadd0sub  13842  grppncan  13846  grpnpcan  13847  mulgnn0p1  13886  mulgaddcomlem  13898  mulginvcom  13900  mulginvinv  13901  subgsubcl  13938  subgsub  13939  eqglact  13978  quselbasg  13983  quseccl0g  13984  qussub  13990  ghmsub  14004  subcmnd  14086  rng1zrlem  14198  dvrcl  14380  unitdvcl  14381  dvrcan1  14385  dvrcan3  14386  dvreq1  14387  subrgdv  14484  lmodvsubval2  14616  lmodprop2d  14622  zndvds  14923  ntrin  15115  elnei  15143  cnrest2  15227  psmetsym  15320  psmetge0  15322  xmetge0  15356  xmetsym  15359  cnmet  15521  rpcxpsub  15899  rpdivcxp  15902  logbleb  15952  logblt  15953  lgsmodeq  16044  lgsmulsqcoprm  16045  gausslemma2dlem1a  16057  2lgsoddprmlem2  16105  upgrpredgv  16267  issubgr2  16379  uhgrissubgr  16382  egrsubgr  16384  upgrwlkvtxedg  16485  clwwlk1loop  16520  clwwlkccatlem  16521  clwwlknonex2lem2  16559  bj-peano4  16851