Theorem 3adant2 1016

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 995	. 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 978

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 980

This theorem is referenced by:  3ad2ant1  1018  3imp3i2an  1183  eupickb  2107  vtoclegft  2811  eqeu  2909  suc11g  4558  soinxp  4698  funopg  5252  fnco  5326  dff1o2  5468  fnimapr  5578  fvun1  5584  fvmptt  5609  fnreseql  5628  fvpr1g  5724  fvpr2g  5725  f1elima  5776  f1ocnvfvb  5783  ovexg  5911  oprssov  6018  poxp  6235  smoiso  6305  rdgivallem  6384  nndi  6489  nndir  6493  fnsnsplitdc  6508  nnaord  6512  nnaordr  6513  nnaword  6514  nnawordi  6518  ecopovtrn  6634  ecopovtrng  6637  xpdom3m  6836  mapxpen  6850  findcard  6890  fisseneq  6933  resfnfinfinss  6941  funrnfi  6943  netap  7255  2omotaplemap  7258  ltsopi  7321  addcanpig  7335  addassnqg  7383  distrnqg  7388  ltsonq  7399  ltmnqg  7402  prarloclemarch2  7420  nnanq0  7459  distrnq0  7460  distnq0r  7464  prltlu  7488  prarloclem5  7501  distrlem1prl  7583  distrlem1pru  7584  distrlem5prl  7587  distrlem5pru  7588  ltpopr  7596  ltsopr  7597  ltexprlemm  7601  ltexprlemfl  7610  ltexprlemfu  7612  lttrsr  7763  ltsosr  7765  ltasrg  7771  recexgt0sr  7774  mulextsr1lem  7781  mulextsr1  7782  axpre-mulext  7889  adddir  7950  axltwlin  8027  axlttrn  8028  ltleletr  8041  letr  8042  nnncan1  8195  npncan3  8197  pnpcan2  8199  subdi  8344  subdir  8345  reapcotr  8557  divmulap  8634  div23ap  8650  div13ap  8652  muldivdirap  8666  divsubdirap  8667  divcanap7  8680  ltmul2  8815  lemul2  8816  lemul2a  8818  lediv1  8828  ltmuldiv2  8834  lemuldiv2  8841  squeeze0  8863  nndivtr  8963  bndndx  9177  nn0n0n1ge2  9325  fnn0ind  9371  addlelt  9770  xrletr  9810  xrltne  9815  xleadd2a  9876  xleadd1  9877  xltadd2  9879  iooneg  9990  iccneg  9991  icoshft  9992  icoshftf1o  9993  zltaddlt1le  10009  fztri3or  10041  fzdcel  10042  fzen  10045  uzsubsubfz  10049  fzrevral2  10108  fzshftral  10110  fz0fzdiffz0  10132  elfzmlbp  10134  elfzo  10151  fzoaddel2  10195  fzosubel2  10197  elfzom1p1elfzo  10216  ssfzo12bi  10227  subfzo0  10244  flltdivnn0lt  10306  modqmulnn  10344  modfzo0difsn  10397  expdivap  10573  expubnd  10579  mulbinom2  10639  bernneq2  10644  shftuz  10828  shftval2  10837  abs3dif  11116  xrmaxlesup  11269  xrltmininf  11280  xrlemininf  11281  sin02gt0  11773  dvdsval2  11799  dvdscmul  11827  dvdsmulc  11828  ndvdssub  11937  rpmulgcd  12029  cncongr1  12105  cncongr2  12106  isprm3  12120  coprimeprodsq  12259  pythagtriplem12  12277  pythagtriplem14  12279  pcmul  12303  pcdiv  12304  pcqcl  12308  pcqdiv  12309  pcdvdsb  12321  ercpbl  12755  mgmb1mgm1  12792  grpinvid1  12929  grpinvid2  12930  grpasscan1  12938  grpasscan2  12939  grpinvadd  12953  grpsubf  12954  grpsubrcan  12956  grpinvsub  12957  grpsubeq0  12961  grpsubadd0sub  12962  grppncan  12966  grpnpcan  12967  mulgnn0p1  12999  mulgaddcomlem  13011  mulginvcom  13013  mulginvinv  13014  subgsubcl  13050  subgsub  13051  eqglact  13089  subcmnd  13134  srg1zr  13175  dvrcl  13309  unitdvcl  13310  dvrcan1  13314  dvrcan3  13315  dvreq1  13316  subrgdv  13364  lmodvsubval2  13437  lmodprop2d  13443  ntrin  13663  elnei  13691  cnrest2  13775  psmetsym  13868  psmetge0  13870  xmetge0  13904  xmetsym  13907  cnmet  14069  rpcxpsub  14368  rpdivcxp  14371  logbleb  14418  logblt  14419  lgsmodeq  14485  lgsmulsqcoprm  14486  2lgsoddprmlem2  14493  bj-peano4  14746