Theorem 3adant1 1000

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 981	. 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 103   /\ w3a 963

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 965

This theorem is referenced by:  3ad2ant2  1004  3ad2ant3  1005  rsp2e  2508  sbciegft  2967  reuhyp  4430  suc11g  4514  soinxp  4653  breldmg  4789  funopg  5201  funimaexglem  5250  fex2  5335  fnreseql  5574  ftpg  5648  mpoeq3ia  5880  mpofvex  6145  poxp  6173  smores3  6234  tfrlemibxssdm  6268  nndi  6426  nnmass  6427  nndir  6430  fnsnsplitdc  6445  nnaord  6449  nnaordr  6450  nnawordi  6455  nnmord  6457  ecopovtrn  6570  ecopovtrng  6573  ixpf  6658  mapxpen  6786  ltsopi  7223  addassnqg  7285  ltsonq  7301  ltmnqg  7304  distrnq0  7362  addlocpr  7439  distrlem1prl  7485  distrlem1pru  7486  distrlem4prl  7487  distrlem4pru  7488  ltpopr  7498  ltsopr  7499  addcanprg  7519  lttrsr  7665  ltsosr  7667  ltasrg  7673  recexgt0sr  7676  mulextsr1lem  7683  mulextsr1  7684  axpre-mulext  7791  adddir  7852  axltwlin  7928  axlttrn  7929  ltleletr  7942  letr  7943  mul32  7988  mul31  7989  add32  8017  subsub23  8063  addsubass  8068  subcan2  8083  subsub2  8086  nppcan2  8089  sub32  8092  nnncan  8093  nnncan2  8095  pnpcan2  8098  subdi  8243  subdir  8244  reapcotr  8456  receuap  8526  divmulap3  8533  divrecap  8544  divrecap2  8545  divsubdirap  8564  divdivap1  8579  redivclap  8587  div2negap  8591  ltmul2  8710  lemul2  8711  lemul2a  8713  lediv1  8723  gt0div  8724  ge0div  8725  ltdivmul  8730  ltdivmul2  8732  ledivmul2  8734  uzind2  9259  nn0ind  9261  fnn0ind  9263  uz3m2nn  9467  xrletr  9694  xrre2  9707  xleadd2a  9760  xleadd1  9761  xltadd2  9763  ixxdisj  9789  iooneg  9874  iccneg  9875  icoshft  9876  icoshftf1o  9877  icodisj  9878  fzen  9927  fzrev3  9971  2ffzeq  10022  fzoaddel2  10074  elfzodifsumelfzo  10082  ssfzo12bi  10106  fzoshftral  10119  adddivflid  10173  fldiv4p1lem1div2  10186  modqmulnn  10223  modqeqmodmin  10275  frec2uzf1od  10287  expdivap  10452  shftval2  10708  mulreap  10746  absdivap  10952  absdiflt  10974  absdifle  10975  abs3dif  10987  cau3  10997  ltmininf  11116  xrmaxlesup  11138  xrltmininf  11149  xrlemininf  11150  xrminltinf  11151  geoisum1c  11399  dvdsmulc  11696  dvdsmultr1  11706  dvdsmultr2  11708  dvdssub2  11710  oexpneg  11749  divalgb  11797  ndvdsadd  11803  gcdaddm  11848  modgcd  11855  dvdsgcd  11876  dvdsgcdb  11877  gcdass  11879  mulgcd  11880  absmulgcd  11881  rpmulgcd  11890  nn0seqcvgd  11898  algcvga  11908  lcmdvds  11936  lcmdvdsb  11941  lcmass  11942  coprmdvds  11949  coprmdvds2  11950  rpmul  11955  cncongr1  11960  cncongr2  11961  prmgt1  11988  qnumdenbi  12046  setsvala  12181  setsex  12182  unopn  12363  clsss  12478  opnssneib  12516  restabs  12535  upxp  12632  blpnfctr  12799  mscl  12825  xmscl  12826  xmsge0  12827  xmseq0  12828  rpdivcxp  13192  cxpcom  13217  rplogbreexp  13230  rplogbzexp  13231  rprelogbmulexp  13233  logbleb  13238  logblt  13239  bj-peano4  13489