Theorem 3adant2 923

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 902	. 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 97   /\ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  3ad2ant1  925  eupickb  1981  vtoclegft  2625  eqeu  2711  suc11g  4281  soinxp  4410  funopg  4934  fnco  5007  dff1o2  5131  fnimapr  5233  fvun1  5239  fvmptt  5262  fnreseql  5277  fvpr1g  5367  fvpr2g  5368  f1elima  5412  f1ocnvfvb  5420  ovexg  5539  oprssov  5642  poxp  5853  smoiso  5917  rdgivallem  5968  nndi  6065  nndir  6069  nnaord  6082  nnaordr  6083  nnaword  6084  nnawordi  6088  ecopovtrn  6203  ecopovtrng  6206  xpdom3m  6308  findcard  6345  ltsopi  6418  addcanpig  6432  addassnqg  6480  distrnqg  6485  ltsonq  6496  ltmnqg  6499  prarloclemarch2  6517  nnanq0  6556  distrnq0  6557  distnq0r  6561  prltlu  6585  prarloclem5  6598  distrlem1prl  6680  distrlem1pru  6681  distrlem5prl  6684  distrlem5pru  6685  ltpopr  6693  ltsopr  6694  ltexprlemm  6698  ltexprlemfl  6707  ltexprlemfu  6709  lttrsr  6847  ltsosr  6849  ltasrg  6855  recexgt0sr  6858  mulextsr1lem  6864  mulextsr1  6865  axpre-mulext  6962  adddir  7018  axltwlin  7087  axlttrn  7088  ltleletr  7100  letr  7101  nnncan1  7247  npncan3  7249  pnpcan2  7251  subdi  7382  subdir  7383  reapcotr  7589  divmulap  7654  div23ap  7670  div13ap  7672  divsubdirap  7684  divcanap7  7697  ltmul2  7822  lemul2  7823  lemul2a  7825  lediv1  7835  ltmuldiv2  7841  lemuldiv2  7848  squeeze0  7870  nndivtr  7955  bndndx  8180  nn0n0n1ge2  8311  fnn0ind  8354  xrletr  8724  xrltne  8729  iooneg  8856  iccneg  8857  icoshft  8858  icoshftf1o  8859  fztri3or  8903  fzdcel  8904  fzen  8907  uzsubsubfz  8911  fzrevral2  8968  fzshftral  8970  fz0fzdiffz0  8987  elfzmlbmOLD  8989  elfzmlbp  8990  elfzo  9006  fzoaddel2  9049  fzosubel2  9051  elfzom1p1elfzo  9070  ssfzo12bi  9081  subfzo0  9097  flltdivnn0lt  9146  modqmulnn  9184  expdivap  9305  expubnd  9311  bernneq2  9370  shftuz  9418  shftval2  9427  abs3dif  9701  bj-peano4  10080