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  4649  soinxp  4789  funopg  5352  fnco  5431  dff1o2  5579  fnimapr  5696  fvun1  5702  fvmptt  5728  fnreseql  5747  fvpr1g  5849  fvpr2g  5850  f1elima  5903  f1ocnvfvb  5910  ovexg  6041  oprssov  6153  poxp  6384  smoiso  6454  rdgivallem  6533  nndi  6640  nndir  6644  fnsnsplitdc  6659  nnaord  6663  nnaordr  6664  nnaword  6665  nnawordi  6669  ecopovtrn  6787  ecopovtrng  6790  xpdom3m  7001  mapxpen  7017  findcard  7058  fisseneq  7107  resfnfinfinss  7117  funrnfi  7120  netap  7451  2omotaplemap  7454  ltsopi  7518  addcanpig  7532  addassnqg  7580  distrnqg  7585  ltsonq  7596  ltmnqg  7599  prarloclemarch2  7617  nnanq0  7656  distrnq0  7657  distnq0r  7661  prltlu  7685  prarloclem5  7698  distrlem1prl  7780  distrlem1pru  7781  distrlem5prl  7784  distrlem5pru  7785  ltpopr  7793  ltsopr  7794  ltexprlemm  7798  ltexprlemfl  7807  ltexprlemfu  7809  lttrsr  7960  ltsosr  7962  ltasrg  7968  recexgt0sr  7971  mulextsr1lem  7978  mulextsr1  7979  axpre-mulext  8086  adddir  8148  axltwlin  8225  axlttrn  8226  ltleletr  8239  letr  8240  nnncan1  8393  npncan3  8395  pnpcan2  8397  subdi  8542  subdir  8543  reapcotr  8756  divmulap  8833  div23ap  8849  div13ap  8851  muldivdirap  8865  divsubdirap  8866  divcanap7  8879  ltmul2  9014  lemul2  9015  lemul2a  9017  lediv1  9027  ltmuldiv2  9033  lemuldiv2  9040  squeeze0  9062  nndivtr  9163  bndndx  9379  nn0n0n1ge2  9528  fnn0ind  9574  addlelt  9976  xrletr  10016  xrltne  10021  xleadd2a  10082  xleadd1  10083  xltadd2  10085  iooneg  10196  iccneg  10197  icoshft  10198  icoshftf1o  10199  zltaddlt1le  10215  fztri3or  10247  fzdcel  10248  fzen  10251  uzsubsubfz  10255  fzrevral2  10314  fzshftral  10316  fz0fzdiffz0  10338  elfzmlbp  10340  elfzo  10357  nelfzo  10360  fzoaddel2  10408  fzosubel2  10413  elfzom1p1elfzo  10432  ssfzo12bi  10443  subfzo0  10460  flltdivnn0lt  10536  modqmulnn  10576  modfzo0difsn  10629  expdivap  10824  expubnd  10830  mulbinom2  10890  bernneq2  10895  ccatval1  11145  ccatval3  11147  ccatfv0  11151  ccatval1lsw  11152  ccatws1lenp1bg  11183  pfxsuffeqwrdeq  11245  pfxsuff1eqwrdeq  11246  swrdswrd  11252  pfxpfx  11255  wrd2ind  11270  swrdccatin1  11272  pfxccatin12lem1  11275  swrdccatin2  11276  pfxccatin12lem3  11279  swrdccat  11282  pfxccatpfx1  11283  pfxccatpfx2  11284  swrdccat3blem  11286  shftuz  11343  shftval2  11352  abs3dif  11631  xrmaxlesup  11785  xrltmininf  11796  xrlemininf  11797  sin02gt0  12290  dvdsval2  12316  dvdscmul  12344  dvdsmulc  12345  ndvdssub  12456  rpmulgcd  12562  cncongr1  12640  cncongr2  12641  isprm3  12655  coprimeprodsq  12795  pythagtriplem12  12813  pythagtriplem14  12815  pcmul  12839  pcdiv  12840  pcqcl  12844  pcqdiv  12845  pcdvdsb  12858  ercpbl  13379  mgmb1mgm1  13416  grpinvid1  13600  grpinvid2  13601  grpasscan1  13611  grpasscan2  13612  grpinvadd  13626  grpsubf  13627  grpsubrcan  13629  grpinvsub  13630  grpsubeq0  13634  grpsubadd0sub  13635  grppncan  13639  grpnpcan  13640  mulgnn0p1  13685  mulgaddcomlem  13697  mulginvcom  13699  mulginvinv  13700  subgsubcl  13737  subgsub  13738  eqglact  13777  quselbasg  13782  quseccl0g  13783  qussub  13789  ghmsub  13803  subcmnd  13885  srg1zr  13965  dvrcl  14114  unitdvcl  14115  dvrcan1  14119  dvrcan3  14120  dvreq1  14121  subrgdv  14217  lmodvsubval2  14321  lmodprop2d  14327  zndvds  14628  ntrin  14813  elnei  14841  cnrest2  14925  psmetsym  15018  psmetge0  15020  xmetge0  15054  xmetsym  15057  cnmet  15219  rpcxpsub  15597  rpdivcxp  15600  logbleb  15650  logblt  15651  lgsmodeq  15739  lgsmulsqcoprm  15740  gausslemma2dlem1a  15752  2lgsoddprmlem2  15800  upgrpredgv  15959  upgrwlkvtxedg  16105  clwwlk1loop  16136  clwwlkccatlem  16137  bj-peano4  16373