Theorem 3adant2 1019

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 998	. 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 981

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 983

This theorem is referenced by:  3ad2ant1  1021  3imp3i2an  1186  eupickb  2137  vtoclegft  2852  eqeu  2950  ifnebibdc  3625  suc11g  4623  soinxp  4763  funopg  5324  fnco  5403  dff1o2  5549  fnimapr  5662  fvun1  5668  fvmptt  5694  fnreseql  5713  fvpr1g  5813  fvpr2g  5814  f1elima  5865  f1ocnvfvb  5872  ovexg  6001  oprssov  6111  poxp  6341  smoiso  6411  rdgivallem  6490  nndi  6595  nndir  6599  fnsnsplitdc  6614  nnaord  6618  nnaordr  6619  nnaword  6620  nnawordi  6624  ecopovtrn  6742  ecopovtrng  6745  xpdom3m  6954  mapxpen  6970  findcard  7011  fisseneq  7057  resfnfinfinss  7067  funrnfi  7070  netap  7401  2omotaplemap  7404  ltsopi  7468  addcanpig  7482  addassnqg  7530  distrnqg  7535  ltsonq  7546  ltmnqg  7549  prarloclemarch2  7567  nnanq0  7606  distrnq0  7607  distnq0r  7611  prltlu  7635  prarloclem5  7648  distrlem1prl  7730  distrlem1pru  7731  distrlem5prl  7734  distrlem5pru  7735  ltpopr  7743  ltsopr  7744  ltexprlemm  7748  ltexprlemfl  7757  ltexprlemfu  7759  lttrsr  7910  ltsosr  7912  ltasrg  7918  recexgt0sr  7921  mulextsr1lem  7928  mulextsr1  7929  axpre-mulext  8036  adddir  8098  axltwlin  8175  axlttrn  8176  ltleletr  8189  letr  8190  nnncan1  8343  npncan3  8345  pnpcan2  8347  subdi  8492  subdir  8493  reapcotr  8706  divmulap  8783  div23ap  8799  div13ap  8801  muldivdirap  8815  divsubdirap  8816  divcanap7  8829  ltmul2  8964  lemul2  8965  lemul2a  8967  lediv1  8977  ltmuldiv2  8983  lemuldiv2  8990  squeeze0  9012  nndivtr  9113  bndndx  9329  nn0n0n1ge2  9478  fnn0ind  9524  addlelt  9925  xrletr  9965  xrltne  9970  xleadd2a  10031  xleadd1  10032  xltadd2  10034  iooneg  10145  iccneg  10146  icoshft  10147  icoshftf1o  10148  zltaddlt1le  10164  fztri3or  10196  fzdcel  10197  fzen  10200  uzsubsubfz  10204  fzrevral2  10263  fzshftral  10265  fz0fzdiffz0  10287  elfzmlbp  10289  elfzo  10306  nelfzo  10309  fzoaddel2  10356  fzosubel2  10361  elfzom1p1elfzo  10380  ssfzo12bi  10391  subfzo0  10408  flltdivnn0lt  10484  modqmulnn  10524  modfzo0difsn  10577  expdivap  10772  expubnd  10778  mulbinom2  10838  bernneq2  10843  ccatval1  11091  ccatval3  11093  ccatfv0  11097  ccatval1lsw  11098  ccatws1lenp1bg  11127  pfxsuffeqwrdeq  11189  pfxsuff1eqwrdeq  11190  swrdswrd  11196  pfxpfx  11199  wrd2ind  11214  swrdccatin1  11216  pfxccatin12lem1  11219  swrdccatin2  11220  pfxccatin12lem3  11223  swrdccat  11226  pfxccatpfx1  11227  pfxccatpfx2  11228  swrdccat3blem  11230  shftuz  11243  shftval2  11252  abs3dif  11531  xrmaxlesup  11685  xrltmininf  11696  xrlemininf  11697  sin02gt0  12190  dvdsval2  12216  dvdscmul  12244  dvdsmulc  12245  ndvdssub  12356  rpmulgcd  12462  cncongr1  12540  cncongr2  12541  isprm3  12555  coprimeprodsq  12695  pythagtriplem12  12713  pythagtriplem14  12715  pcmul  12739  pcdiv  12740  pcqcl  12744  pcqdiv  12745  pcdvdsb  12758  ercpbl  13278  mgmb1mgm1  13315  grpinvid1  13499  grpinvid2  13500  grpasscan1  13510  grpasscan2  13511  grpinvadd  13525  grpsubf  13526  grpsubrcan  13528  grpinvsub  13529  grpsubeq0  13533  grpsubadd0sub  13534  grppncan  13538  grpnpcan  13539  mulgnn0p1  13584  mulgaddcomlem  13596  mulginvcom  13598  mulginvinv  13599  subgsubcl  13636  subgsub  13637  eqglact  13676  quselbasg  13681  quseccl0g  13682  qussub  13688  ghmsub  13702  subcmnd  13784  srg1zr  13864  dvrcl  14012  unitdvcl  14013  dvrcan1  14017  dvrcan3  14018  dvreq1  14019  subrgdv  14115  lmodvsubval2  14219  lmodprop2d  14225  zndvds  14526  ntrin  14711  elnei  14739  cnrest2  14823  psmetsym  14916  psmetge0  14918  xmetge0  14952  xmetsym  14955  cnmet  15117  rpcxpsub  15495  rpdivcxp  15498  logbleb  15548  logblt  15549  lgsmodeq  15637  lgsmulsqcoprm  15638  gausslemma2dlem1a  15650  2lgsoddprmlem2  15698  upgrpredgv  15850  bj-peano4  16090