Theorem 3adant2 1006

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 985	. 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 103   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  3ad2ant1  1008  3imp3i2an  1173  eupickb  2095  vtoclegft  2797  eqeu  2895  suc11g  4533  soinxp  4673  funopg  5221  fnco  5295  dff1o2  5436  fnimapr  5545  fvun1  5551  fvmptt  5576  fnreseql  5594  fvpr1g  5690  fvpr2g  5691  f1elima  5740  f1ocnvfvb  5747  ovexg  5872  oprssov  5979  poxp  6196  smoiso  6266  rdgivallem  6345  nndi  6450  nndir  6454  fnsnsplitdc  6469  nnaord  6473  nnaordr  6474  nnaword  6475  nnawordi  6479  ecopovtrn  6594  ecopovtrng  6597  xpdom3m  6796  mapxpen  6810  findcard  6850  fisseneq  6893  resfnfinfinss  6901  funrnfi  6903  ltsopi  7257  addcanpig  7271  addassnqg  7319  distrnqg  7324  ltsonq  7335  ltmnqg  7338  prarloclemarch2  7356  nnanq0  7395  distrnq0  7396  distnq0r  7400  prltlu  7424  prarloclem5  7437  distrlem1prl  7519  distrlem1pru  7520  distrlem5prl  7523  distrlem5pru  7524  ltpopr  7532  ltsopr  7533  ltexprlemm  7537  ltexprlemfl  7546  ltexprlemfu  7548  lttrsr  7699  ltsosr  7701  ltasrg  7707  recexgt0sr  7710  mulextsr1lem  7717  mulextsr1  7718  axpre-mulext  7825  adddir  7886  axltwlin  7962  axlttrn  7963  ltleletr  7976  letr  7977  nnncan1  8130  npncan3  8132  pnpcan2  8134  subdi  8279  subdir  8280  reapcotr  8492  divmulap  8567  div23ap  8583  div13ap  8585  muldivdirap  8599  divsubdirap  8600  divcanap7  8613  ltmul2  8747  lemul2  8748  lemul2a  8750  lediv1  8760  ltmuldiv2  8766  lemuldiv2  8773  squeeze0  8795  nndivtr  8895  bndndx  9109  nn0n0n1ge2  9257  fnn0ind  9303  addlelt  9700  xrletr  9740  xrltne  9745  xleadd2a  9806  xleadd1  9807  xltadd2  9809  iooneg  9920  iccneg  9921  icoshft  9922  icoshftf1o  9923  zltaddlt1le  9939  fztri3or  9970  fzdcel  9971  fzen  9974  uzsubsubfz  9978  fzrevral2  10037  fzshftral  10039  fz0fzdiffz0  10061  elfzmlbp  10063  elfzo  10080  fzoaddel2  10124  fzosubel2  10126  elfzom1p1elfzo  10145  ssfzo12bi  10156  subfzo0  10173  flltdivnn0lt  10235  modqmulnn  10273  modfzo0difsn  10326  expdivap  10502  expubnd  10508  mulbinom2  10567  bernneq2  10572  shftuz  10755  shftval2  10764  abs3dif  11043  xrmaxlesup  11196  xrltmininf  11207  xrlemininf  11208  sin02gt0  11700  dvdsval2  11726  dvdscmul  11754  dvdsmulc  11755  ndvdssub  11863  rpmulgcd  11955  cncongr1  12031  cncongr2  12032  isprm3  12046  coprimeprodsq  12185  pythagtriplem12  12203  pythagtriplem14  12205  pcmul  12229  pcdiv  12230  pcqcl  12234  pcqdiv  12235  pcdvdsb  12247  ntrin  12724  elnei  12752  cnrest2  12836  psmetsym  12929  psmetge0  12931  xmetge0  12965  xmetsym  12968  cnmet  13130  rpcxpsub  13429  rpdivcxp  13432  logbleb  13479  logblt  13480  lgsmodeq  13546  lgsmulsqcoprm  13547  bj-peano4  13797