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  2134  vtoclegft  2844  eqeu  2942  ifnebibdc  3614  suc11g  4604  soinxp  4744  funopg  5304  fnco  5383  dff1o2  5526  fnimapr  5638  fvun1  5644  fvmptt  5670  fnreseql  5689  fvpr1g  5789  fvpr2g  5790  f1elima  5841  f1ocnvfvb  5848  ovexg  5977  oprssov  6087  poxp  6317  smoiso  6387  rdgivallem  6466  nndi  6571  nndir  6575  fnsnsplitdc  6590  nnaord  6594  nnaordr  6595  nnaword  6596  nnawordi  6600  ecopovtrn  6718  ecopovtrng  6721  xpdom3m  6928  mapxpen  6944  findcard  6984  fisseneq  7030  resfnfinfinss  7040  funrnfi  7043  netap  7365  2omotaplemap  7368  ltsopi  7432  addcanpig  7446  addassnqg  7494  distrnqg  7499  ltsonq  7510  ltmnqg  7513  prarloclemarch2  7531  nnanq0  7570  distrnq0  7571  distnq0r  7575  prltlu  7599  prarloclem5  7612  distrlem1prl  7694  distrlem1pru  7695  distrlem5prl  7698  distrlem5pru  7699  ltpopr  7707  ltsopr  7708  ltexprlemm  7712  ltexprlemfl  7721  ltexprlemfu  7723  lttrsr  7874  ltsosr  7876  ltasrg  7882  recexgt0sr  7885  mulextsr1lem  7892  mulextsr1  7893  axpre-mulext  8000  adddir  8062  axltwlin  8139  axlttrn  8140  ltleletr  8153  letr  8154  nnncan1  8307  npncan3  8309  pnpcan2  8311  subdi  8456  subdir  8457  reapcotr  8670  divmulap  8747  div23ap  8763  div13ap  8765  muldivdirap  8779  divsubdirap  8780  divcanap7  8793  ltmul2  8928  lemul2  8929  lemul2a  8931  lediv1  8941  ltmuldiv2  8947  lemuldiv2  8954  squeeze0  8976  nndivtr  9077  bndndx  9293  nn0n0n1ge2  9442  fnn0ind  9488  addlelt  9889  xrletr  9929  xrltne  9934  xleadd2a  9995  xleadd1  9996  xltadd2  9998  iooneg  10109  iccneg  10110  icoshft  10111  icoshftf1o  10112  zltaddlt1le  10128  fztri3or  10160  fzdcel  10161  fzen  10164  uzsubsubfz  10168  fzrevral2  10227  fzshftral  10229  fz0fzdiffz0  10251  elfzmlbp  10253  elfzo  10270  nelfzo  10273  fzoaddel2  10317  fzosubel2  10322  elfzom1p1elfzo  10341  ssfzo12bi  10352  subfzo0  10369  flltdivnn0lt  10445  modqmulnn  10485  modfzo0difsn  10538  expdivap  10733  expubnd  10739  mulbinom2  10799  bernneq2  10804  ccatval1  11051  ccatval3  11053  ccatfv0  11057  ccatval1lsw  11058  ccatws1lenp1bg  11087  shftuz  11099  shftval2  11108  abs3dif  11387  xrmaxlesup  11541  xrltmininf  11552  xrlemininf  11553  sin02gt0  12046  dvdsval2  12072  dvdscmul  12100  dvdsmulc  12101  ndvdssub  12212  rpmulgcd  12318  cncongr1  12396  cncongr2  12397  isprm3  12411  coprimeprodsq  12551  pythagtriplem12  12569  pythagtriplem14  12571  pcmul  12595  pcdiv  12596  pcqcl  12600  pcqdiv  12601  pcdvdsb  12614  ercpbl  13134  mgmb1mgm1  13171  grpinvid1  13355  grpinvid2  13356  grpasscan1  13366  grpasscan2  13367  grpinvadd  13381  grpsubf  13382  grpsubrcan  13384  grpinvsub  13385  grpsubeq0  13389  grpsubadd0sub  13390  grppncan  13394  grpnpcan  13395  mulgnn0p1  13440  mulgaddcomlem  13452  mulginvcom  13454  mulginvinv  13455  subgsubcl  13492  subgsub  13493  eqglact  13532  quselbasg  13537  quseccl0g  13538  qussub  13544  ghmsub  13558  subcmnd  13640  srg1zr  13720  dvrcl  13868  unitdvcl  13869  dvrcan1  13873  dvrcan3  13874  dvreq1  13875  subrgdv  13971  lmodvsubval2  14075  lmodprop2d  14081  zndvds  14382  ntrin  14567  elnei  14595  cnrest2  14679  psmetsym  14772  psmetge0  14774  xmetge0  14808  xmetsym  14811  cnmet  14973  rpcxpsub  15351  rpdivcxp  15354  logbleb  15404  logblt  15405  lgsmodeq  15493  lgsmulsqcoprm  15494  gausslemma2dlem1a  15506  2lgsoddprmlem2  15554  bj-peano4  15853