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  2135  vtoclegft  2845  eqeu  2943  ifnebibdc  3615  suc11g  4605  soinxp  4745  funopg  5305  fnco  5384  dff1o2  5527  fnimapr  5639  fvun1  5645  fvmptt  5671  fnreseql  5690  fvpr1g  5790  fvpr2g  5791  f1elima  5842  f1ocnvfvb  5849  ovexg  5978  oprssov  6088  poxp  6318  smoiso  6388  rdgivallem  6467  nndi  6572  nndir  6576  fnsnsplitdc  6591  nnaord  6595  nnaordr  6596  nnaword  6597  nnawordi  6601  ecopovtrn  6719  ecopovtrng  6722  xpdom3m  6929  mapxpen  6945  findcard  6985  fisseneq  7031  resfnfinfinss  7041  funrnfi  7044  netap  7366  2omotaplemap  7369  ltsopi  7433  addcanpig  7447  addassnqg  7495  distrnqg  7500  ltsonq  7511  ltmnqg  7514  prarloclemarch2  7532  nnanq0  7571  distrnq0  7572  distnq0r  7576  prltlu  7600  prarloclem5  7613  distrlem1prl  7695  distrlem1pru  7696  distrlem5prl  7699  distrlem5pru  7700  ltpopr  7708  ltsopr  7709  ltexprlemm  7713  ltexprlemfl  7722  ltexprlemfu  7724  lttrsr  7875  ltsosr  7877  ltasrg  7883  recexgt0sr  7886  mulextsr1lem  7893  mulextsr1  7894  axpre-mulext  8001  adddir  8063  axltwlin  8140  axlttrn  8141  ltleletr  8154  letr  8155  nnncan1  8308  npncan3  8310  pnpcan2  8312  subdi  8457  subdir  8458  reapcotr  8671  divmulap  8748  div23ap  8764  div13ap  8766  muldivdirap  8780  divsubdirap  8781  divcanap7  8794  ltmul2  8929  lemul2  8930  lemul2a  8932  lediv1  8942  ltmuldiv2  8948  lemuldiv2  8955  squeeze0  8977  nndivtr  9078  bndndx  9294  nn0n0n1ge2  9443  fnn0ind  9489  addlelt  9890  xrletr  9930  xrltne  9935  xleadd2a  9996  xleadd1  9997  xltadd2  9999  iooneg  10110  iccneg  10111  icoshft  10112  icoshftf1o  10113  zltaddlt1le  10129  fztri3or  10161  fzdcel  10162  fzen  10165  uzsubsubfz  10169  fzrevral2  10228  fzshftral  10230  fz0fzdiffz0  10252  elfzmlbp  10254  elfzo  10271  nelfzo  10274  fzoaddel2  10319  fzosubel2  10324  elfzom1p1elfzo  10343  ssfzo12bi  10354  subfzo0  10371  flltdivnn0lt  10447  modqmulnn  10487  modfzo0difsn  10540  expdivap  10735  expubnd  10741  mulbinom2  10801  bernneq2  10806  ccatval1  11053  ccatval3  11055  ccatfv0  11059  ccatval1lsw  11060  ccatws1lenp1bg  11089  shftuz  11128  shftval2  11137  abs3dif  11416  xrmaxlesup  11570  xrltmininf  11581  xrlemininf  11582  sin02gt0  12075  dvdsval2  12101  dvdscmul  12129  dvdsmulc  12130  ndvdssub  12241  rpmulgcd  12347  cncongr1  12425  cncongr2  12426  isprm3  12440  coprimeprodsq  12580  pythagtriplem12  12598  pythagtriplem14  12600  pcmul  12624  pcdiv  12625  pcqcl  12629  pcqdiv  12630  pcdvdsb  12643  ercpbl  13163  mgmb1mgm1  13200  grpinvid1  13384  grpinvid2  13385  grpasscan1  13395  grpasscan2  13396  grpinvadd  13410  grpsubf  13411  grpsubrcan  13413  grpinvsub  13414  grpsubeq0  13418  grpsubadd0sub  13419  grppncan  13423  grpnpcan  13424  mulgnn0p1  13469  mulgaddcomlem  13481  mulginvcom  13483  mulginvinv  13484  subgsubcl  13521  subgsub  13522  eqglact  13561  quselbasg  13566  quseccl0g  13567  qussub  13573  ghmsub  13587  subcmnd  13669  srg1zr  13749  dvrcl  13897  unitdvcl  13898  dvrcan1  13902  dvrcan3  13903  dvreq1  13904  subrgdv  14000  lmodvsubval2  14104  lmodprop2d  14110  zndvds  14411  ntrin  14596  elnei  14624  cnrest2  14708  psmetsym  14801  psmetge0  14803  xmetge0  14837  xmetsym  14840  cnmet  15002  rpcxpsub  15380  rpdivcxp  15383  logbleb  15433  logblt  15434  lgsmodeq  15522  lgsmulsqcoprm  15523  gausslemma2dlem1a  15535  2lgsoddprmlem2  15583  bj-peano4  15891