Theorem 3adant1 956

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
3adant1	|- ( ( th /\ ph /\ ps ) -> ch )

Proof of Theorem 3adant1

Step	Hyp	Ref	Expression
1		3simpc 937	. 2 |- ( ( th /\ ph /\ ps ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( th /\ ph /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  3ad2ant2  960  3ad2ant3  961  rsp2e  2414  sbciegft  2844  reuhyp  4222  suc11g  4300  soinxp  4428  breldmg  4559  funopg  4954  funimaexglem  5002  fex2  5079  fnreseql  5298  ftpg  5368  mpt2eq3ia  5590  mpt2fvex  5849  poxp  5873  smores3  5931  tfrlemibxssdm  5964  nndi  6088  nnmass  6089  nndir  6092  nnaord  6105  nnaordr  6106  nnawordi  6111  nnmord  6113  ecopovtrn  6226  ecopovtrng  6229  ltsopi  6510  addassnqg  6572  ltsonq  6588  ltmnqg  6591  distrnq0  6649  addlocpr  6726  distrlem1prl  6772  distrlem1pru  6773  distrlem4prl  6774  distrlem4pru  6775  ltpopr  6785  ltsopr  6786  addcanprg  6806  lttrsr  6939  ltsosr  6941  ltasrg  6947  recexgt0sr  6950  mulextsr1lem  6956  mulextsr1  6957  axpre-mulext  7054  adddir  7110  axltwlin  7180  axlttrn  7181  ltleletr  7193  letr  7194  mul32  7238  mul31  7239  add32  7267  subsub23  7313  addsubass  7318  subcan2  7333  subsub2  7336  nppcan2  7339  sub32  7342  nnncan  7343  nnncan2  7345  pnpcan2  7348  subdi  7489  subdir  7490  reapcotr  7698  receuap  7759  divmulap3  7765  divrecap  7776  divrecap2  7777  divsubdirap  7796  divdivap1  7811  redivclap  7819  div2negap  7823  ltmul2  7934  lemul2  7935  lemul2a  7937  lediv1  7947  gt0div  7948  ge0div  7949  ltdivmul  7954  ltdivmul2  7956  ledivmul2  7958  uzind2  8459  nn0ind  8461  fnn0ind  8463  uz3m2nn  8661  xrletr  8878  xrre2  8888  ixxdisj  8926  iooneg  9010  iccneg  9011  icoshft  9012  icoshftf1o  9013  icodisj  9014  fzen  9062  fzrev3  9104  2ffzeq  9151  fzoaddel2  9202  elfzodifsumelfzo  9210  ssfzo12bi  9234  fzoshftral  9247  adddivflid  9294  fldiv4p1lem1div2  9307  modqmulnn  9344  modqeqmodmin  9396  frec2uzf1od  9408  expdivap  9527  shftval2  9714  mulreap  9751  absdivap  9956  absdiflt  9978  absdifle  9979  abs3dif  9991  cau3  10001  ltmininf  10116  dvdsmulc  10223  dvdsmultr1  10233  dvdsmultr2  10235  dvdssub2  10237  oexpneg  10276  divalgb  10325  ndvdsadd  10331  gcdaddm  10375  modgcd  10382  dvdsgcd  10401  dvdsgcdb  10402  gcdass  10404  mulgcd  10405  absmulgcd  10406  rpmulgcd  10415  nn0seqcvgd  10423  ialgcvga  10433  lcmdvds  10461  lcmdvdsb  10466  lcmass  10467  coprmdvds  10474  coprmdvds2  10475  rpmul  10480  cncongr1  10485  cncongr2  10486  prmgt1  10513  bj-peano4  10750