Theorem 3adant2 1018

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 997	. 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 980

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 982

This theorem is referenced by:  3ad2ant1  1020  3imp3i2an  1185  eupickb  2126  vtoclegft  2836  eqeu  2934  ifnebibdc  3605  suc11g  4594  soinxp  4734  funopg  5293  fnco  5367  dff1o2  5510  fnimapr  5622  fvun1  5628  fvmptt  5654  fnreseql  5673  fvpr1g  5769  fvpr2g  5770  f1elima  5821  f1ocnvfvb  5828  ovexg  5957  oprssov  6066  poxp  6291  smoiso  6361  rdgivallem  6440  nndi  6545  nndir  6549  fnsnsplitdc  6564  nnaord  6568  nnaordr  6569  nnaword  6570  nnawordi  6574  ecopovtrn  6692  ecopovtrng  6695  xpdom3m  6894  mapxpen  6910  findcard  6950  fisseneq  6996  resfnfinfinss  7006  funrnfi  7009  netap  7323  2omotaplemap  7326  ltsopi  7389  addcanpig  7403  addassnqg  7451  distrnqg  7456  ltsonq  7467  ltmnqg  7470  prarloclemarch2  7488  nnanq0  7527  distrnq0  7528  distnq0r  7532  prltlu  7556  prarloclem5  7569  distrlem1prl  7651  distrlem1pru  7652  distrlem5prl  7655  distrlem5pru  7656  ltpopr  7664  ltsopr  7665  ltexprlemm  7669  ltexprlemfl  7678  ltexprlemfu  7680  lttrsr  7831  ltsosr  7833  ltasrg  7839  recexgt0sr  7842  mulextsr1lem  7849  mulextsr1  7850  axpre-mulext  7957  adddir  8019  axltwlin  8096  axlttrn  8097  ltleletr  8110  letr  8111  nnncan1  8264  npncan3  8266  pnpcan2  8268  subdi  8413  subdir  8414  reapcotr  8627  divmulap  8704  div23ap  8720  div13ap  8722  muldivdirap  8736  divsubdirap  8737  divcanap7  8750  ltmul2  8885  lemul2  8886  lemul2a  8888  lediv1  8898  ltmuldiv2  8904  lemuldiv2  8911  squeeze0  8933  nndivtr  9034  bndndx  9250  nn0n0n1ge2  9398  fnn0ind  9444  addlelt  9845  xrletr  9885  xrltne  9890  xleadd2a  9951  xleadd1  9952  xltadd2  9954  iooneg  10065  iccneg  10066  icoshft  10067  icoshftf1o  10068  zltaddlt1le  10084  fztri3or  10116  fzdcel  10117  fzen  10120  uzsubsubfz  10124  fzrevral2  10183  fzshftral  10185  fz0fzdiffz0  10207  elfzmlbp  10209  elfzo  10226  nelfzo  10229  fzoaddel2  10271  fzosubel2  10273  elfzom1p1elfzo  10292  ssfzo12bi  10303  subfzo0  10320  flltdivnn0lt  10396  modqmulnn  10436  modfzo0difsn  10489  expdivap  10684  expubnd  10690  mulbinom2  10750  bernneq2  10755  shftuz  10984  shftval2  10993  abs3dif  11272  xrmaxlesup  11426  xrltmininf  11437  xrlemininf  11438  sin02gt0  11931  dvdsval2  11957  dvdscmul  11985  dvdsmulc  11986  ndvdssub  12097  rpmulgcd  12203  cncongr1  12281  cncongr2  12282  isprm3  12296  coprimeprodsq  12436  pythagtriplem12  12454  pythagtriplem14  12456  pcmul  12480  pcdiv  12481  pcqcl  12485  pcqdiv  12486  pcdvdsb  12499  ercpbl  12984  mgmb1mgm1  13021  grpinvid1  13194  grpinvid2  13195  grpasscan1  13205  grpasscan2  13206  grpinvadd  13220  grpsubf  13221  grpsubrcan  13223  grpinvsub  13224  grpsubeq0  13228  grpsubadd0sub  13229  grppncan  13233  grpnpcan  13234  mulgnn0p1  13273  mulgaddcomlem  13285  mulginvcom  13287  mulginvinv  13288  subgsubcl  13325  subgsub  13326  eqglact  13365  quselbasg  13370  quseccl0g  13371  qussub  13377  ghmsub  13391  subcmnd  13473  srg1zr  13553  dvrcl  13701  unitdvcl  13702  dvrcan1  13706  dvrcan3  13707  dvreq1  13708  subrgdv  13804  lmodvsubval2  13908  lmodprop2d  13914  zndvds  14215  ntrin  14370  elnei  14398  cnrest2  14482  psmetsym  14575  psmetge0  14577  xmetge0  14611  xmetsym  14614  cnmet  14776  rpcxpsub  15154  rpdivcxp  15157  logbleb  15207  logblt  15208  lgsmodeq  15296  lgsmulsqcoprm  15297  gausslemma2dlem1a  15309  2lgsoddprmlem2  15357  bj-peano4  15611