Theorem 3adant2 1047

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 1026	. 2 |- ( ( ph /\ th /\ ps ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( ph /\ th /\ ps ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3ad2ant1  1049  3imp3i2an  1214  eupickb  2168  vtoclegft  2897  eqeu  2996  ifnebibdc  3686  suc11g  4704  soinxp  4845  funopg  5411  fnco  5491  dff1o2  5644  fnimapr  5763  fvun1  5769  fvmptt  5797  fnreseql  5819  fvpr1g  5921  fvpr2g  5922  f1elima  5979  f1ocnvfvb  5986  ovexg  6119  oprssov  6231  poxp  6468  smoiso  6573  rdgivallem  6652  nndi  6759  nndir  6763  fnsnsplitdc  6778  nnaord  6782  nnaordr  6783  nnaword  6784  nnawordi  6788  ecopovtrn  6906  ecopovtrng  6909  mapsnd  6970  xpdom3m  7132  mapxpen  7148  findcard  7192  fisseneq  7242  resfnfinfinss  7253  funrnfi  7256  netap  7620  2omotaplemap  7623  ltsopi  7687  addcanpig  7701  addassnqg  7749  distrnqg  7754  ltsonq  7765  ltmnqg  7768  prarloclemarch2  7786  nnanq0  7825  distrnq0  7826  distnq0r  7830  prltlu  7854  prarloclem5  7867  distrlem1prl  7949  distrlem1pru  7950  distrlem5prl  7953  distrlem5pru  7954  ltpopr  7962  ltsopr  7963  ltexprlemm  7967  ltexprlemfl  7976  ltexprlemfu  7978  lttrsr  8129  ltsosr  8131  ltasrg  8137  recexgt0sr  8140  mulextsr1lem  8147  mulextsr1  8148  axpre-mulext  8255  adddir  8317  axltwlin  8393  axlttrn  8394  ltleletr  8407  letr  8408  nnncan1  8562  npncan3  8564  pnpcan2  8566  subdi  8712  subdir  8713  reapcotr  8926  divmulap  9005  div23ap  9021  div13ap  9023  muldivdirap  9037  divsubdirap  9038  divcanap7  9051  ltmul2  9186  lemul2  9187  lemul2a  9189  lediv1  9199  ltmuldiv2  9205  lemuldiv2  9212  squeeze0  9234  nndivtr  9346  bndndx  9562  nn0n0n1ge2  9715  fnn0ind  9762  addlelt  10169  xrletr  10210  xrltne  10215  xleadd2a  10276  xleadd1  10277  xltadd2  10279  iooneg  10390  iccneg  10391  icoshft  10392  icoshftf1o  10393  zltaddlt1le  10410  fztri3or  10443  fzdcel  10444  fzen  10447  uzsubsubfz  10452  fzrevral2  10513  fzshftral  10515  fz0fzdiffz0  10537  elfzmlbp  10539  elfzo  10556  nelfzo  10559  fzoaddel2  10608  fzosubel2  10613  elfzom1p1elfzo  10632  ssfzo12bi  10643  subfzo0  10661  flltdivnn0lt  10739  modqmulnn  10779  modfzo0difsn  10832  expdivap  11027  expubnd  11033  mulbinom2  11093  bernneq2  11099  ccatval1  11365  ccatval3  11367  ccatfv0  11371  ccatval1lsw  11372  ccatws1lenp1bg  11403  pfxsuffeqwrdeq  11470  pfxsuff1eqwrdeq  11471  swrdswrd  11477  pfxpfx  11480  wrd2ind  11495  swrdccatin1  11497  pfxccatin12lem1  11500  swrdccatin2  11501  pfxccatin12lem3  11504  swrdccat  11507  pfxccatpfx1  11508  pfxccatpfx2  11509  swrdccat3blem  11511  shftuz  11582  shftval2  11591  abs3dif  11871  xrmaxlesup  12025  xrltmininf  12036  xrlemininf  12037  sin02gt0  12531  dvdsval2  12557  dvdscmul  12585  dvdsmulc  12586  ndvdssub  12697  rpmulgcd  12803  cncongr1  12881  cncongr2  12882  isprm3  12896  coprimeprodsq  13036  pythagtriplem12  13054  pythagtriplem14  13056  pcmul  13080  pcdiv  13081  pcqcl  13085  pcqdiv  13086  pcdvdsb  13099  ercpbl  13652  mgmb1mgm1  13688  grpinvid1  13857  grpinvid2  13858  grpasscan1  13868  grpasscan2  13869  grpinvadd  13883  grpsubf  13884  grpsubrcan  13886  grpinvsub  13887  grpsubeq0  13891  grpsubadd0sub  13892  grppncan  13896  grpnpcan  13897  mulgnn0p1  13936  mulgaddcomlem  13948  mulginvcom  13950  mulginvinv  13951  subgsubcl  13988  subgsub  13989  eqglact  14028  quselbasg  14033  quseccl0g  14034  qussub  14040  ghmsub  14054  subcmnd  14137  rng1zrlem  14258  dvrcl  14442  unitdvcl  14443  dvrcan1  14447  dvrcan3  14448  dvreq1  14449  subrgdv  14546  lmodvsubval2  14679  lmodprop2d  14685  zndvds  14984  ascldimul  15031  ntrin  15225  elnei  15253  cnrest2  15337  psmetsym  15430  psmetge0  15432  xmetge0  15466  xmetsym  15469  cnmet  15631  rpcxpsub  16010  rpdivcxp  16013  logbleb  16063  logblt  16064  lgsmodeq  16164  lgsmulsqcoprm  16165  gausslemma2dlem1a  16177  2lgsoddprmlem2  16225  upgrpredgv  16387  issubgr2  16499  uhgrissubgr  16502  egrsubgr  16504  upgrwlkvtxedg  16605  clwwlk1loop  16640  clwwlkccatlem  16641  clwwlknonex2lem2  16679  bj-peano4  16981