Theorem 3adant1 1042

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 1023	. 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 1005

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 1007

This theorem is referenced by:  3ad2ant2  1046  3ad2ant3  1047  rsp2e  2595  sbciegft  3075  reuhyp  4595  suc11g  4681  soinxp  4822  breldmg  4964  funopg  5388  funimaexglem  5441  fex2  5533  fnreseql  5790  ftpg  5870  mpoeq3ia  6120  funexw  6307  mpofvex  6403  poxp  6430  suppval1  6441  smores3  6526  tfrlemibxssdm  6560  nndi  6721  nnmass  6722  nndir  6725  fnsnsplitdc  6740  nnaord  6744  nnaordr  6745  nnawordi  6750  nnmord  6752  ecopovtrn  6868  ecopovtrng  6871  ixpf  6957  f1oen4g  6993  f1dom4g  6994  mapxpen  7103  funisfsupp  7246  netap  7570  2omotaplemap  7573  ltsopi  7637  addassnqg  7699  ltsonq  7715  ltmnqg  7718  distrnq0  7776  addlocpr  7853  distrlem1prl  7899  distrlem1pru  7900  distrlem4prl  7901  distrlem4pru  7902  ltpopr  7912  ltsopr  7913  addcanprg  7933  lttrsr  8079  ltsosr  8081  ltasrg  8087  recexgt0sr  8090  mulextsr1lem  8097  mulextsr1  8098  axpre-mulext  8205  adddir  8267  axltwlin  8343  axlttrn  8344  ltleletr  8357  letr  8358  mul32  8405  mul31  8406  add32  8434  subsub23  8480  addsubass  8485  subcan2  8500  subsub2  8503  nppcan2  8506  sub32  8509  nnncan  8510  nnncan2  8512  pnpcan2  8515  subdi  8660  subdir  8661  reapcotr  8874  receuap  8945  divmulap3  8953  divrecap  8964  divrecap2  8965  divsubdirap  8984  divdivap1  8999  redivclap  9007  div2negap  9011  ltmul2  9132  lemul2  9133  lemul2a  9135  lediv1  9145  gt0div  9146  ge0div  9147  ltdivmul  9152  ltdivmul2  9154  ledivmul2  9156  uzind2  9693  nn0ind  9695  fnn0ind  9697  uz3m2nn  9908  xrletr  10144  xrre2  10157  xleadd2a  10210  xleadd1  10211  xltadd2  10213  ixxdisj  10239  iooneg  10324  iccneg  10325  icoshft  10326  icoshftf1o  10327  icodisj  10328  fzen  10380  fzrev3  10425  2ffzeq  10479  fzoaddel2  10539  elfzodifsumelfzo  10550  ssfzo12bi  10574  fzoshftral  10588  adddivflid  10656  fldiv4p1lem1div2  10669  modqmulnn  10708  modqeqmodmin  10760  frec2uzf1od  10772  expdivap  10956  ccatval1  11289  ccatass  11300  fzowrddc  11343  swrdval  11344  swrdnd  11355  swrd0g  11356  swrdfv2  11359  pfxsuff1eqwrdeq  11395  swrdswrdlem  11400  pfxccatin12lem2a  11423  pfxccatin12lem1  11424  shftval2  11515  mulreap  11553  absdivap  11759  absdiflt  11781  absdifle  11782  abs3dif  11794  cau3  11804  ltmininf  11924  xrmaxlesup  11948  xrltmininf  11959  xrlemininf  11960  xrminltinf  11961  geoisum1c  12210  dvdsmulc  12509  dvdsmultr1  12521  dvdsmultr2  12523  dvdssub2  12525  oexpneg  12567  divalgb  12615  ndvdsadd  12621  gcdaddm  12684  modgcd  12691  dvdsgcd  12712  dvdsgcdb  12713  gcdass  12715  mulgcd  12716  absmulgcd  12717  rpmulgcd  12726  nn0seqcvgd  12742  algcvga  12752  lcmdvds  12780  lcmdvdsb  12785  lcmass  12786  coprmdvds  12793  coprmdvds2  12794  rpmul  12799  cncongr1  12804  cncongr2  12805  prmgt1  12833  qnumdenbi  12893  coprimeprodsq  12959  pythagtriplem4  12970  pythagtriplem8  12974  pythagtriplem9  12975  pythagtriplem12  12977  pythagtriplem14  12979  pythagtriplem16  12981  pcpremul  12995  pcgcd  13031  setsvala  13260  setsex  13261  ressval2  13296  isgrpi  13754  grpsubrcan  13811  grpinvsub  13812  grpsubeq0  13816  grpsubadd0sub  13817  grpnpcan  13822  qussub  13971  ghmsub  13985  opprmulg  14232  rrgeq0  14427  lmodvsubval2  14507  rmodislmodlem  14515  rmodislmod  14516  lssintclm  14549  lssincl  14550  rnglidlmmgm  14661  cncrng  14734  unopn  14887  clsss  15000  opnssneib  15038  restabs  15057  upxp  15154  blpnfctr  15321  mscl  15347  xmscl  15348  xmsge0  15349  xmseq0  15350  mpomulcn  15448  rpdivcxp  15793  cxpcom  15820  rplogbreexp  15835  rplogbzexp  15836  rprelogbmulexp  15838  logbleb  15843  logblt  15844  lgsneg  15914  lgsne0  15928  lgsmodeq  15935  lgsmulsqcoprm  15936  gausslemma2dlem1a  15948  funvtxdm2domval  16041  funiedgdm2domval  16042  iedgedgg  16073  iswlk  16335  uspgr2wlkeq  16377  uspgr2wlkeq2  16378  uspgr2wlkeqi  16379  istrl  16397  clwwlkgt0  16408  iseupth  16459  bj-peano4  16742