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  3604  suc11g  4593  soinxp  4733  funopg  5292  fnco  5366  dff1o2  5509  fnimapr  5621  fvun1  5627  fvmptt  5653  fnreseql  5672  fvpr1g  5768  fvpr2g  5769  f1elima  5820  f1ocnvfvb  5827  ovexg  5956  oprssov  6065  poxp  6290  smoiso  6360  rdgivallem  6439  nndi  6544  nndir  6548  fnsnsplitdc  6563  nnaord  6567  nnaordr  6568  nnaword  6569  nnawordi  6573  ecopovtrn  6691  ecopovtrng  6694  xpdom3m  6893  mapxpen  6909  findcard  6949  fisseneq  6995  resfnfinfinss  7005  funrnfi  7008  netap  7321  2omotaplemap  7324  ltsopi  7387  addcanpig  7401  addassnqg  7449  distrnqg  7454  ltsonq  7465  ltmnqg  7468  prarloclemarch2  7486  nnanq0  7525  distrnq0  7526  distnq0r  7530  prltlu  7554  prarloclem5  7567  distrlem1prl  7649  distrlem1pru  7650  distrlem5prl  7653  distrlem5pru  7654  ltpopr  7662  ltsopr  7663  ltexprlemm  7667  ltexprlemfl  7676  ltexprlemfu  7678  lttrsr  7829  ltsosr  7831  ltasrg  7837  recexgt0sr  7840  mulextsr1lem  7847  mulextsr1  7848  axpre-mulext  7955  adddir  8017  axltwlin  8094  axlttrn  8095  ltleletr  8108  letr  8109  nnncan1  8262  npncan3  8264  pnpcan2  8266  subdi  8411  subdir  8412  reapcotr  8625  divmulap  8702  div23ap  8718  div13ap  8720  muldivdirap  8734  divsubdirap  8735  divcanap7  8748  ltmul2  8883  lemul2  8884  lemul2a  8886  lediv1  8896  ltmuldiv2  8902  lemuldiv2  8909  squeeze0  8931  nndivtr  9032  bndndx  9248  nn0n0n1ge2  9396  fnn0ind  9442  addlelt  9843  xrletr  9883  xrltne  9888  xleadd2a  9949  xleadd1  9950  xltadd2  9952  iooneg  10063  iccneg  10064  icoshft  10065  icoshftf1o  10066  zltaddlt1le  10082  fztri3or  10114  fzdcel  10115  fzen  10118  uzsubsubfz  10122  fzrevral2  10181  fzshftral  10183  fz0fzdiffz0  10205  elfzmlbp  10207  elfzo  10224  nelfzo  10227  fzoaddel2  10269  fzosubel2  10271  elfzom1p1elfzo  10290  ssfzo12bi  10301  subfzo0  10318  flltdivnn0lt  10394  modqmulnn  10434  modfzo0difsn  10487  expdivap  10682  expubnd  10688  mulbinom2  10748  bernneq2  10753  shftuz  10982  shftval2  10991  abs3dif  11270  xrmaxlesup  11424  xrltmininf  11435  xrlemininf  11436  sin02gt0  11929  dvdsval2  11955  dvdscmul  11983  dvdsmulc  11984  ndvdssub  12095  rpmulgcd  12193  cncongr1  12271  cncongr2  12272  isprm3  12286  coprimeprodsq  12426  pythagtriplem12  12444  pythagtriplem14  12446  pcmul  12470  pcdiv  12471  pcqcl  12475  pcqdiv  12476  pcdvdsb  12489  ercpbl  12974  mgmb1mgm1  13011  grpinvid1  13184  grpinvid2  13185  grpasscan1  13195  grpasscan2  13196  grpinvadd  13210  grpsubf  13211  grpsubrcan  13213  grpinvsub  13214  grpsubeq0  13218  grpsubadd0sub  13219  grppncan  13223  grpnpcan  13224  mulgnn0p1  13263  mulgaddcomlem  13275  mulginvcom  13277  mulginvinv  13278  subgsubcl  13315  subgsub  13316  eqglact  13355  quselbasg  13360  quseccl0g  13361  qussub  13367  ghmsub  13381  subcmnd  13463  srg1zr  13543  dvrcl  13691  unitdvcl  13692  dvrcan1  13696  dvrcan3  13697  dvreq1  13698  subrgdv  13794  lmodvsubval2  13898  lmodprop2d  13904  zndvds  14205  ntrin  14360  elnei  14388  cnrest2  14472  psmetsym  14565  psmetge0  14567  xmetge0  14601  xmetsym  14604  cnmet  14766  rpcxpsub  15144  rpdivcxp  15147  logbleb  15197  logblt  15198  lgsmodeq  15286  lgsmulsqcoprm  15287  gausslemma2dlem1a  15299  2lgsoddprmlem2  15347  bj-peano4  15601