Theorem 3adant1 1017

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 998	. 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 104   /\ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  3ad2ant2  1021  3ad2ant3  1022  rsp2e  2545  sbciegft  3017  reuhyp  4504  suc11g  4590  soinxp  4730  breldmg  4869  funopg  5289  funimaexglem  5338  fex2  5423  fnreseql  5669  ftpg  5743  mpoeq3ia  5984  funexw  6166  mpofvex  6260  poxp  6287  smores3  6348  tfrlemibxssdm  6382  nndi  6541  nnmass  6542  nndir  6545  fnsnsplitdc  6560  nnaord  6564  nnaordr  6565  nnawordi  6570  nnmord  6572  ecopovtrn  6688  ecopovtrng  6691  ixpf  6776  mapxpen  6906  netap  7316  2omotaplemap  7319  ltsopi  7382  addassnqg  7444  ltsonq  7460  ltmnqg  7463  distrnq0  7521  addlocpr  7598  distrlem1prl  7644  distrlem1pru  7645  distrlem4prl  7646  distrlem4pru  7647  ltpopr  7657  ltsopr  7658  addcanprg  7678  lttrsr  7824  ltsosr  7826  ltasrg  7832  recexgt0sr  7835  mulextsr1lem  7842  mulextsr1  7843  axpre-mulext  7950  adddir  8012  axltwlin  8089  axlttrn  8090  ltleletr  8103  letr  8104  mul32  8151  mul31  8152  add32  8180  subsub23  8226  addsubass  8231  subcan2  8246  subsub2  8249  nppcan2  8252  sub32  8255  nnncan  8256  nnncan2  8258  pnpcan2  8261  subdi  8406  subdir  8407  reapcotr  8619  receuap  8690  divmulap3  8698  divrecap  8709  divrecap2  8710  divsubdirap  8729  divdivap1  8744  redivclap  8752  div2negap  8756  ltmul2  8877  lemul2  8878  lemul2a  8880  lediv1  8890  gt0div  8891  ge0div  8892  ltdivmul  8897  ltdivmul2  8899  ledivmul2  8901  uzind2  9432  nn0ind  9434  fnn0ind  9436  uz3m2nn  9641  xrletr  9877  xrre2  9890  xleadd2a  9943  xleadd1  9944  xltadd2  9946  ixxdisj  9972  iooneg  10057  iccneg  10058  icoshft  10059  icoshftf1o  10060  icodisj  10061  fzen  10112  fzrev3  10156  2ffzeq  10210  fzoaddel2  10263  elfzodifsumelfzo  10271  ssfzo12bi  10295  fzoshftral  10308  adddivflid  10364  fldiv4p1lem1div2  10377  modqmulnn  10416  modqeqmodmin  10468  frec2uzf1od  10480  expdivap  10664  shftval2  10973  mulreap  11011  absdivap  11217  absdiflt  11239  absdifle  11240  abs3dif  11252  cau3  11262  ltmininf  11381  xrmaxlesup  11405  xrltmininf  11416  xrlemininf  11417  xrminltinf  11418  geoisum1c  11666  dvdsmulc  11965  dvdsmultr1  11977  dvdsmultr2  11979  dvdssub2  11981  oexpneg  12021  divalgb  12069  ndvdsadd  12075  gcdaddm  12124  modgcd  12131  dvdsgcd  12152  dvdsgcdb  12153  gcdass  12155  mulgcd  12156  absmulgcd  12157  rpmulgcd  12166  nn0seqcvgd  12182  algcvga  12192  lcmdvds  12220  lcmdvdsb  12225  lcmass  12226  coprmdvds  12233  coprmdvds2  12234  rpmul  12239  cncongr1  12244  cncongr2  12245  prmgt1  12273  qnumdenbi  12333  coprimeprodsq  12398  pythagtriplem4  12409  pythagtriplem8  12413  pythagtriplem9  12414  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem16  12420  pcpremul  12434  pcgcd  12470  setsvala  12652  setsex  12653  ressval2  12687  isgrpi  13099  grpsubrcan  13156  grpinvsub  13157  grpsubeq0  13161  grpsubadd0sub  13162  grpnpcan  13167  qussub  13310  ghmsub  13324  opprmulg  13570  rrgeq0  13764  lmodvsubval2  13841  rmodislmodlem  13849  rmodislmod  13850  lssintclm  13883  lssincl  13884  rnglidlmmgm  13995  cncrng  14068  unopn  14184  clsss  14297  opnssneib  14335  restabs  14354  upxp  14451  blpnfctr  14618  mscl  14644  xmscl  14645  xmsge0  14646  xmseq0  14647  mpomulcn  14745  rpdivcxp  15087  cxpcom  15112  rplogbreexp  15126  rplogbzexp  15127  rprelogbmulexp  15129  logbleb  15134  logblt  15135  lgsneg  15181  lgsne0  15195  lgsmodeq  15202  lgsmulsqcoprm  15203  gausslemma2dlem1a  15215  bj-peano4  15517