Theorem 3adant1 1005

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 986	. 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 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:  3ad2ant2  1009  3ad2ant3  1010  rsp2e  2516  sbciegft  2980  reuhyp  4449  suc11g  4533  soinxp  4673  breldmg  4809  funopg  5221  funimaexglem  5270  fex2  5355  fnreseql  5594  ftpg  5668  mpoeq3ia  5903  mpofvex  6168  poxp  6196  smores3  6257  tfrlemibxssdm  6291  nndi  6450  nnmass  6451  nndir  6454  fnsnsplitdc  6469  nnaord  6473  nnaordr  6474  nnawordi  6479  nnmord  6481  ecopovtrn  6594  ecopovtrng  6597  ixpf  6682  mapxpen  6810  ltsopi  7257  addassnqg  7319  ltsonq  7335  ltmnqg  7338  distrnq0  7396  addlocpr  7473  distrlem1prl  7519  distrlem1pru  7520  distrlem4prl  7521  distrlem4pru  7522  ltpopr  7532  ltsopr  7533  addcanprg  7553  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  mul32  8024  mul31  8025  add32  8053  subsub23  8099  addsubass  8104  subcan2  8119  subsub2  8122  nppcan2  8125  sub32  8128  nnncan  8129  nnncan2  8131  pnpcan2  8134  subdi  8279  subdir  8280  reapcotr  8492  receuap  8562  divmulap3  8569  divrecap  8580  divrecap2  8581  divsubdirap  8600  divdivap1  8615  redivclap  8623  div2negap  8627  ltmul2  8747  lemul2  8748  lemul2a  8750  lediv1  8760  gt0div  8761  ge0div  8762  ltdivmul  8767  ltdivmul2  8769  ledivmul2  8771  uzind2  9299  nn0ind  9301  fnn0ind  9303  uz3m2nn  9507  xrletr  9740  xrre2  9753  xleadd2a  9806  xleadd1  9807  xltadd2  9809  ixxdisj  9835  iooneg  9920  iccneg  9921  icoshft  9922  icoshftf1o  9923  icodisj  9924  fzen  9974  fzrev3  10018  2ffzeq  10072  fzoaddel2  10124  elfzodifsumelfzo  10132  ssfzo12bi  10156  fzoshftral  10169  adddivflid  10223  fldiv4p1lem1div2  10236  modqmulnn  10273  modqeqmodmin  10325  frec2uzf1od  10337  expdivap  10502  shftval2  10764  mulreap  10802  absdivap  11008  absdiflt  11030  absdifle  11031  abs3dif  11043  cau3  11053  ltmininf  11172  xrmaxlesup  11196  xrltmininf  11207  xrlemininf  11208  xrminltinf  11209  geoisum1c  11457  dvdsmulc  11755  dvdsmultr1  11767  dvdsmultr2  11769  dvdssub2  11771  oexpneg  11810  divalgb  11858  ndvdsadd  11864  gcdaddm  11913  modgcd  11920  dvdsgcd  11941  dvdsgcdb  11942  gcdass  11944  mulgcd  11945  absmulgcd  11946  rpmulgcd  11955  nn0seqcvgd  11969  algcvga  11979  lcmdvds  12007  lcmdvdsb  12012  lcmass  12013  coprmdvds  12020  coprmdvds2  12021  rpmul  12026  cncongr1  12031  cncongr2  12032  prmgt1  12060  qnumdenbi  12120  coprimeprodsq  12185  pythagtriplem4  12196  pythagtriplem8  12200  pythagtriplem9  12201  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem16  12207  pcpremul  12221  pcgcd  12256  setsvala  12421  setsex  12422  unopn  12603  clsss  12718  opnssneib  12756  restabs  12775  upxp  12872  blpnfctr  13039  mscl  13065  xmscl  13066  xmsge0  13067  xmseq0  13068  rpdivcxp  13432  cxpcom  13457  rplogbreexp  13471  rplogbzexp  13472  rprelogbmulexp  13474  logbleb  13479  logblt  13480  lgsneg  13525  lgsne0  13539  lgsmodeq  13546  lgsmulsqcoprm  13547  bj-peano4  13797