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  2161  vtoclegft  2879  eqeu  2977  ifnebibdc  3655  suc11g  4661  soinxp  4802  funopg  5367  fnco  5447  dff1o2  5597  fnimapr  5715  fvun1  5721  fvmptt  5747  fnreseql  5766  fvpr1g  5868  fvpr2g  5869  f1elima  5924  f1ocnvfvb  5931  ovexg  6062  oprssov  6174  poxp  6406  smoiso  6511  rdgivallem  6590  nndi  6697  nndir  6701  fnsnsplitdc  6716  nnaord  6720  nnaordr  6721  nnaword  6722  nnawordi  6726  ecopovtrn  6844  ecopovtrng  6847  xpdom3m  7061  mapxpen  7077  findcard  7120  fisseneq  7170  resfnfinfinss  7181  funrnfi  7184  netap  7516  2omotaplemap  7519  ltsopi  7583  addcanpig  7597  addassnqg  7645  distrnqg  7650  ltsonq  7661  ltmnqg  7664  prarloclemarch2  7682  nnanq0  7721  distrnq0  7722  distnq0r  7726  prltlu  7750  prarloclem5  7763  distrlem1prl  7845  distrlem1pru  7846  distrlem5prl  7849  distrlem5pru  7850  ltpopr  7858  ltsopr  7859  ltexprlemm  7863  ltexprlemfl  7872  ltexprlemfu  7874  lttrsr  8025  ltsosr  8027  ltasrg  8033  recexgt0sr  8036  mulextsr1lem  8043  mulextsr1  8044  axpre-mulext  8151  adddir  8213  axltwlin  8289  axlttrn  8290  ltleletr  8303  letr  8304  nnncan1  8457  npncan3  8459  pnpcan2  8461  subdi  8606  subdir  8607  reapcotr  8820  divmulap  8897  div23ap  8913  div13ap  8915  muldivdirap  8929  divsubdirap  8930  divcanap7  8943  ltmul2  9078  lemul2  9079  lemul2a  9081  lediv1  9091  ltmuldiv2  9097  lemuldiv2  9104  squeeze0  9126  nndivtr  9227  bndndx  9443  nn0n0n1ge2  9594  fnn0ind  9640  addlelt  10047  xrletr  10087  xrltne  10092  xleadd2a  10153  xleadd1  10154  xltadd2  10156  iooneg  10267  iccneg  10268  icoshft  10269  icoshftf1o  10270  zltaddlt1le  10287  fztri3or  10319  fzdcel  10320  fzen  10323  uzsubsubfz  10327  fzrevral2  10386  fzshftral  10388  fz0fzdiffz0  10410  elfzmlbp  10412  elfzo  10429  nelfzo  10432  fzoaddel2  10481  fzosubel2  10486  elfzom1p1elfzo  10505  ssfzo12bi  10516  subfzo0  10534  flltdivnn0lt  10610  modqmulnn  10650  modfzo0difsn  10703  expdivap  10898  expubnd  10904  mulbinom2  10964  bernneq2  10969  ccatval1  11223  ccatval3  11225  ccatfv0  11229  ccatval1lsw  11230  ccatws1lenp1bg  11261  pfxsuffeqwrdeq  11328  pfxsuff1eqwrdeq  11329  swrdswrd  11335  pfxpfx  11338  wrd2ind  11353  swrdccatin1  11355  pfxccatin12lem1  11358  swrdccatin2  11359  pfxccatin12lem3  11362  swrdccat  11365  pfxccatpfx1  11366  pfxccatpfx2  11367  swrdccat3blem  11369  shftuz  11440  shftval2  11449  abs3dif  11728  xrmaxlesup  11882  xrltmininf  11893  xrlemininf  11894  sin02gt0  12388  dvdsval2  12414  dvdscmul  12442  dvdsmulc  12443  ndvdssub  12554  rpmulgcd  12660  cncongr1  12738  cncongr2  12739  isprm3  12753  coprimeprodsq  12893  pythagtriplem12  12911  pythagtriplem14  12913  pcmul  12937  pcdiv  12938  pcqcl  12942  pcqdiv  12943  pcdvdsb  12956  ercpbl  13477  mgmb1mgm1  13514  grpinvid1  13698  grpinvid2  13699  grpasscan1  13709  grpasscan2  13710  grpinvadd  13724  grpsubf  13725  grpsubrcan  13727  grpinvsub  13728  grpsubeq0  13732  grpsubadd0sub  13733  grppncan  13737  grpnpcan  13738  mulgnn0p1  13783  mulgaddcomlem  13795  mulginvcom  13797  mulginvinv  13798  subgsubcl  13835  subgsub  13836  eqglact  13875  quselbasg  13880  quseccl0g  13881  qussub  13887  ghmsub  13901  subcmnd  13983  srg1zr  14064  dvrcl  14213  unitdvcl  14214  dvrcan1  14218  dvrcan3  14219  dvreq1  14220  subrgdv  14316  lmodvsubval2  14421  lmodprop2d  14427  zndvds  14728  ntrin  14918  elnei  14946  cnrest2  15030  psmetsym  15123  psmetge0  15125  xmetge0  15159  xmetsym  15162  cnmet  15324  rpcxpsub  15702  rpdivcxp  15705  logbleb  15755  logblt  15756  lgsmodeq  15847  lgsmulsqcoprm  15848  gausslemma2dlem1a  15860  2lgsoddprmlem2  15908  upgrpredgv  16070  issubgr2  16182  uhgrissubgr  16185  egrsubgr  16187  upgrwlkvtxedg  16288  clwwlk1loop  16323  clwwlkccatlem  16324  clwwlknonex2lem2  16362  bj-peano4  16654