Theorem 3adant1 1046

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 1027	. 2 |- ( ( th /\ ph /\ ps ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( th /\ ph /\ ps ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3ad2ant2  1050  3ad2ant3  1051  rsp2e  2601  sbciegft  3082  reuhyp  4618  suc11g  4704  soinxp  4845  breldmg  4987  funopg  5411  funimaexglem  5464  fex2  5556  fnreseql  5819  ftpg  5899  mpoeq3ia  6153  funexw  6341  mpofvex  6441  poxp  6468  suppval1  6479  smores3  6564  tfrlemibxssdm  6598  nndi  6759  nnmass  6760  nndir  6763  fnsnsplitdc  6778  nnaord  6782  nnaordr  6783  nnawordi  6788  nnmord  6790  ecopovtrn  6906  ecopovtrng  6909  ixpf  7002  f1oen4g  7038  f1dom4g  7039  mapxpen  7148  funisfsupp  7291  netap  7620  2omotaplemap  7623  ltsopi  7687  addassnqg  7749  ltsonq  7765  ltmnqg  7768  distrnq0  7826  addlocpr  7903  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  ltpopr  7962  ltsopr  7963  addcanprg  7983  lttrsr  8129  ltsosr  8131  ltasrg  8137  recexgt0sr  8140  mulextsr1lem  8147  mulextsr1  8148  axpre-mulext  8255  adddir  8317  axltwlin  8393  axlttrn  8394  ltleletr  8407  letr  8408  mul32  8457  mul31  8458  add32  8486  subsub23  8532  addsubass  8537  subcan2  8552  subsub2  8555  nppcan2  8558  sub32  8561  nnncan  8562  nnncan2  8564  pnpcan2  8567  subdi  8713  subdir  8714  reapcotr  8928  receuap  9001  divmulap3  9009  divrecap  9020  divrecap2  9021  divsubdirap  9040  divdivap1  9055  redivclap  9063  div2negap  9067  ltmul2  9188  lemul2  9189  lemul2a  9191  lediv1  9201  gt0div  9202  ge0div  9203  ltdivmul  9208  ltdivmul2  9210  ledivmul2  9212  uzind2  9762  nn0ind  9764  fnn0ind  9766  uz3m2nn  9982  xrletr  10220  xrre2  10233  xleadd2a  10286  xleadd1  10287  xltadd2  10289  ixxdisj  10315  iooneg  10400  iccneg  10401  icoshft  10402  icoshftf1o  10403  icodisj  10404  fzen  10457  fzrev3  10504  2ffzeq  10558  fzoaddel2  10618  elfzodifsumelfzo  10629  ssfzo12bi  10653  fzoshftral  10667  adddivflid  10740  fldiv4p1lem1div2  10753  modqmulnn  10792  modqeqmodmin  10844  frec2uzf1od  10856  expdivap  11040  ccatval1  11379  ccatass  11390  fzowrddc  11433  swrdval  11434  swrdnd  11445  swrd0g  11446  swrdfv2  11449  pfxsuff1eqwrdeq  11485  swrdswrdlem  11490  pfxccatin12lem2a  11513  pfxccatin12lem1  11514  shftval2  11605  mulreap  11643  absdivap  11850  absdiflt  11873  absdifle  11874  abs3dif  11886  cau3  11896  ltmininf  12016  xrmaxlesup  12041  xrltmininf  12052  xrlemininf  12053  xrminltinf  12054  geoisum1c  12303  dvdsmulc  12602  dvdsmultr1  12614  dvdsmultr2  12616  dvdssub2  12618  oexpneg  12660  divalgb  12708  ndvdsadd  12714  gcdaddm  12777  modgcd  12784  dvdsgcd  12805  dvdsgcdb  12806  gcdass  12808  mulgcd  12809  absmulgcd  12810  rpmulgcd  12819  nn0seqcvgd  12835  algcvga  12845  lcmdvds  12873  lcmdvdsb  12878  lcmass  12879  coprmdvds  12886  coprmdvds2  12887  rpmul  12892  cncongr1  12897  cncongr2  12898  prmgt1  12927  qnumdenbi  12988  coprimeprodsq  13056  pythagtriplem4  13067  pythagtriplem8  13071  pythagtriplem9  13072  pythagtriplem12  13074  pythagtriplem14  13076  pythagtriplem16  13078  pcpremul  13092  pcgcd  13128  setsvala  13432  setsex  13433  ressval2  13469  isgrpi  13878  grpsubrcan  13935  grpinvsub  13936  grpsubeq0  13940  grpsubadd0sub  13941  grpnpcan  13946  qussub  14089  ghmsub  14103  opprmulg  14425  rrgeq0  14622  lmodvsubval2  14728  rmodislmodlem  14736  rmodislmod  14737  lssintclm  14770  lssincl  14771  rnglidlmmgm  14882  cncrng  14955  unopn  15155  clsss  15268  opnssneib  15306  restabs  15325  upxp  15422  blpnfctr  15589  mscl  15615  xmscl  15616  xmsge0  15617  xmseq0  15618  mpomulcn  15716  rpdivcxp  16066  cxpcom  16093  rplogbreexp  16108  rplogbzexp  16109  rprelogbmulexp  16111  logbleb  16116  logblt  16117  lgsneg  16241  lgsne0  16255  lgsmodeq  16262  lgsmulsqcoprm  16263  gausslemma2dlem1a  16275  funvtxdm2domval  16368  funiedgdm2domval  16369  iedgedgg  16400  iswlk  16662  uspgr2wlkeq  16704  uspgr2wlkeq2  16705  uspgr2wlkeqi  16706  istrl  16724  clwwlkgt0  16735  iseupth  16786  bj-peano4  17079