Theorem 3adant2 1040

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 1019	. 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 1002

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 1004

This theorem is referenced by:  3ad2ant1  1042  3imp3i2an  1207  eupickb  2159  vtoclegft  2875  eqeu  2973  ifnebibdc  3648  suc11g  4648  soinxp  4788  funopg  5351  fnco  5430  dff1o2  5576  fnimapr  5693  fvun1  5699  fvmptt  5725  fnreseql  5744  fvpr1g  5844  fvpr2g  5845  f1elima  5896  f1ocnvfvb  5903  ovexg  6034  oprssov  6146  poxp  6376  smoiso  6446  rdgivallem  6525  nndi  6630  nndir  6634  fnsnsplitdc  6649  nnaord  6653  nnaordr  6654  nnaword  6655  nnawordi  6659  ecopovtrn  6777  ecopovtrng  6780  xpdom3m  6989  mapxpen  7005  findcard  7046  fisseneq  7092  resfnfinfinss  7102  funrnfi  7105  netap  7436  2omotaplemap  7439  ltsopi  7503  addcanpig  7517  addassnqg  7565  distrnqg  7570  ltsonq  7581  ltmnqg  7584  prarloclemarch2  7602  nnanq0  7641  distrnq0  7642  distnq0r  7646  prltlu  7670  prarloclem5  7683  distrlem1prl  7765  distrlem1pru  7766  distrlem5prl  7769  distrlem5pru  7770  ltpopr  7778  ltsopr  7779  ltexprlemm  7783  ltexprlemfl  7792  ltexprlemfu  7794  lttrsr  7945  ltsosr  7947  ltasrg  7953  recexgt0sr  7956  mulextsr1lem  7963  mulextsr1  7964  axpre-mulext  8071  adddir  8133  axltwlin  8210  axlttrn  8211  ltleletr  8224  letr  8225  nnncan1  8378  npncan3  8380  pnpcan2  8382  subdi  8527  subdir  8528  reapcotr  8741  divmulap  8818  div23ap  8834  div13ap  8836  muldivdirap  8850  divsubdirap  8851  divcanap7  8864  ltmul2  8999  lemul2  9000  lemul2a  9002  lediv1  9012  ltmuldiv2  9018  lemuldiv2  9025  squeeze0  9047  nndivtr  9148  bndndx  9364  nn0n0n1ge2  9513  fnn0ind  9559  addlelt  9960  xrletr  10000  xrltne  10005  xleadd2a  10066  xleadd1  10067  xltadd2  10069  iooneg  10180  iccneg  10181  icoshft  10182  icoshftf1o  10183  zltaddlt1le  10199  fztri3or  10231  fzdcel  10232  fzen  10235  uzsubsubfz  10239  fzrevral2  10298  fzshftral  10300  fz0fzdiffz0  10322  elfzmlbp  10324  elfzo  10341  nelfzo  10344  fzoaddel2  10391  fzosubel2  10396  elfzom1p1elfzo  10415  ssfzo12bi  10426  subfzo0  10443  flltdivnn0lt  10519  modqmulnn  10559  modfzo0difsn  10612  expdivap  10807  expubnd  10813  mulbinom2  10873  bernneq2  10878  ccatval1  11127  ccatval3  11129  ccatfv0  11133  ccatval1lsw  11134  ccatws1lenp1bg  11163  pfxsuffeqwrdeq  11225  pfxsuff1eqwrdeq  11226  swrdswrd  11232  pfxpfx  11235  wrd2ind  11250  swrdccatin1  11252  pfxccatin12lem1  11255  swrdccatin2  11256  pfxccatin12lem3  11259  swrdccat  11262  pfxccatpfx1  11263  pfxccatpfx2  11264  swrdccat3blem  11266  shftuz  11323  shftval2  11332  abs3dif  11611  xrmaxlesup  11765  xrltmininf  11776  xrlemininf  11777  sin02gt0  12270  dvdsval2  12296  dvdscmul  12324  dvdsmulc  12325  ndvdssub  12436  rpmulgcd  12542  cncongr1  12620  cncongr2  12621  isprm3  12635  coprimeprodsq  12775  pythagtriplem12  12793  pythagtriplem14  12795  pcmul  12819  pcdiv  12820  pcqcl  12824  pcqdiv  12825  pcdvdsb  12838  ercpbl  13359  mgmb1mgm1  13396  grpinvid1  13580  grpinvid2  13581  grpasscan1  13591  grpasscan2  13592  grpinvadd  13606  grpsubf  13607  grpsubrcan  13609  grpinvsub  13610  grpsubeq0  13614  grpsubadd0sub  13615  grppncan  13619  grpnpcan  13620  mulgnn0p1  13665  mulgaddcomlem  13677  mulginvcom  13679  mulginvinv  13680  subgsubcl  13717  subgsub  13718  eqglact  13757  quselbasg  13762  quseccl0g  13763  qussub  13769  ghmsub  13783  subcmnd  13865  srg1zr  13945  dvrcl  14093  unitdvcl  14094  dvrcan1  14098  dvrcan3  14099  dvreq1  14100  subrgdv  14196  lmodvsubval2  14300  lmodprop2d  14306  zndvds  14607  ntrin  14792  elnei  14820  cnrest2  14904  psmetsym  14997  psmetge0  14999  xmetge0  15033  xmetsym  15036  cnmet  15198  rpcxpsub  15576  rpdivcxp  15579  logbleb  15629  logblt  15630  lgsmodeq  15718  lgsmulsqcoprm  15719  gausslemma2dlem1a  15731  2lgsoddprmlem2  15779  upgrpredgv  15938  bj-peano4  16276