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  8456  mul31  8457  add32  8485  subsub23  8531  addsubass  8536  subcan2  8551  subsub2  8554  nppcan2  8557  sub32  8560  nnncan  8561  nnncan2  8563  pnpcan2  8566  subdi  8712  subdir  8713  reapcotr  8926  receuap  8999  divmulap3  9007  divrecap  9018  divrecap2  9019  divsubdirap  9038  divdivap1  9053  redivclap  9061  div2negap  9065  ltmul2  9186  lemul2  9187  lemul2a  9189  lediv1  9199  gt0div  9200  ge0div  9201  ltdivmul  9206  ltdivmul2  9208  ledivmul2  9210  uzind2  9758  nn0ind  9760  fnn0ind  9762  uz3m2nn  9973  xrletr  10210  xrre2  10223  xleadd2a  10276  xleadd1  10277  xltadd2  10279  ixxdisj  10305  iooneg  10390  iccneg  10391  icoshft  10392  icoshftf1o  10393  icodisj  10394  fzen  10447  fzrev3  10494  2ffzeq  10548  fzoaddel2  10608  elfzodifsumelfzo  10619  ssfzo12bi  10643  fzoshftral  10657  adddivflid  10727  fldiv4p1lem1div2  10740  modqmulnn  10779  modqeqmodmin  10831  frec2uzf1od  10843  expdivap  11027  ccatval1  11365  ccatass  11376  fzowrddc  11419  swrdval  11420  swrdnd  11431  swrd0g  11432  swrdfv2  11435  pfxsuff1eqwrdeq  11471  swrdswrdlem  11476  pfxccatin12lem2a  11499  pfxccatin12lem1  11500  shftval2  11591  mulreap  11629  absdivap  11836  absdiflt  11858  absdifle  11859  abs3dif  11871  cau3  11881  ltmininf  12001  xrmaxlesup  12025  xrltmininf  12036  xrlemininf  12037  xrminltinf  12038  geoisum1c  12287  dvdsmulc  12586  dvdsmultr1  12598  dvdsmultr2  12600  dvdssub2  12602  oexpneg  12644  divalgb  12692  ndvdsadd  12698  gcdaddm  12761  modgcd  12768  dvdsgcd  12789  dvdsgcdb  12790  gcdass  12792  mulgcd  12793  absmulgcd  12794  rpmulgcd  12803  nn0seqcvgd  12819  algcvga  12829  lcmdvds  12857  lcmdvdsb  12862  lcmass  12863  coprmdvds  12870  coprmdvds2  12871  rpmul  12876  cncongr1  12881  cncongr2  12882  prmgt1  12910  qnumdenbi  12970  coprimeprodsq  13036  pythagtriplem4  13047  pythagtriplem8  13051  pythagtriplem9  13052  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem16  13058  pcpremul  13072  pcgcd  13108  setsvala  13383  setsex  13384  ressval2  13420  isgrpi  13829  grpsubrcan  13886  grpinvsub  13887  grpsubeq0  13891  grpsubadd0sub  13892  grpnpcan  13897  qussub  14040  ghmsub  14054  opprmulg  14376  rrgeq0  14573  lmodvsubval2  14679  rmodislmodlem  14687  rmodislmod  14688  lssintclm  14721  lssincl  14722  rnglidlmmgm  14833  cncrng  14906  unopn  15106  clsss  15219  opnssneib  15257  restabs  15276  upxp  15373  blpnfctr  15540  mscl  15566  xmscl  15567  xmsge0  15568  xmseq0  15569  mpomulcn  15667  rpdivcxp  16013  cxpcom  16040  rplogbreexp  16055  rplogbzexp  16056  rprelogbmulexp  16058  logbleb  16063  logblt  16064  lgsneg  16143  lgsne0  16157  lgsmodeq  16164  lgsmulsqcoprm  16165  gausslemma2dlem1a  16177  funvtxdm2domval  16270  funiedgdm2domval  16271  iedgedgg  16302  iswlk  16564  uspgr2wlkeq  16606  uspgr2wlkeq2  16607  uspgr2wlkeqi  16608  istrl  16626  clwwlkgt0  16637  iseupth  16688  bj-peano4  16981