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  2584  sbciegft  3063  reuhyp  4575  suc11g  4661  soinxp  4802  breldmg  4943  funopg  5367  funimaexglem  5420  fex2  5511  fnreseql  5766  ftpg  5846  mpoeq3ia  6096  funexw  6283  mpofvex  6379  poxp  6406  suppval1  6417  smores3  6502  tfrlemibxssdm  6536  nndi  6697  nnmass  6698  nndir  6701  fnsnsplitdc  6716  nnaord  6720  nnaordr  6721  nnawordi  6726  nnmord  6728  ecopovtrn  6844  ecopovtrng  6847  ixpf  6932  f1oen4g  6968  f1dom4g  6969  mapxpen  7077  funisfsupp  7216  netap  7533  2omotaplemap  7536  ltsopi  7600  addassnqg  7662  ltsonq  7678  ltmnqg  7681  distrnq0  7739  addlocpr  7816  distrlem1prl  7862  distrlem1pru  7863  distrlem4prl  7864  distrlem4pru  7865  ltpopr  7875  ltsopr  7876  addcanprg  7896  lttrsr  8042  ltsosr  8044  ltasrg  8050  recexgt0sr  8053  mulextsr1lem  8060  mulextsr1  8061  axpre-mulext  8168  adddir  8230  axltwlin  8306  axlttrn  8307  ltleletr  8320  letr  8321  mul32  8368  mul31  8369  add32  8397  subsub23  8443  addsubass  8448  subcan2  8463  subsub2  8466  nppcan2  8469  sub32  8472  nnncan  8473  nnncan2  8475  pnpcan2  8478  subdi  8623  subdir  8624  reapcotr  8837  receuap  8908  divmulap3  8916  divrecap  8927  divrecap2  8928  divsubdirap  8947  divdivap1  8962  redivclap  8970  div2negap  8974  ltmul2  9095  lemul2  9096  lemul2a  9098  lediv1  9108  gt0div  9109  ge0div  9110  ltdivmul  9115  ltdivmul2  9117  ledivmul2  9119  uzind2  9653  nn0ind  9655  fnn0ind  9657  uz3m2nn  9868  xrletr  10104  xrre2  10117  xleadd2a  10170  xleadd1  10171  xltadd2  10173  ixxdisj  10199  iooneg  10284  iccneg  10285  icoshft  10286  icoshftf1o  10287  icodisj  10288  fzen  10340  fzrev3  10384  2ffzeq  10438  fzoaddel2  10498  elfzodifsumelfzo  10509  ssfzo12bi  10533  fzoshftral  10547  adddivflid  10615  fldiv4p1lem1div2  10628  modqmulnn  10667  modqeqmodmin  10719  frec2uzf1od  10731  expdivap  10915  ccatval1  11240  ccatass  11251  fzowrddc  11294  swrdval  11295  swrdnd  11306  swrd0g  11307  swrdfv2  11310  pfxsuff1eqwrdeq  11346  swrdswrdlem  11351  pfxccatin12lem2a  11374  pfxccatin12lem1  11375  shftval2  11466  mulreap  11504  absdivap  11710  absdiflt  11732  absdifle  11733  abs3dif  11745  cau3  11755  ltmininf  11875  xrmaxlesup  11899  xrltmininf  11910  xrlemininf  11911  xrminltinf  11912  geoisum1c  12161  dvdsmulc  12460  dvdsmultr1  12472  dvdsmultr2  12474  dvdssub2  12476  oexpneg  12518  divalgb  12566  ndvdsadd  12572  gcdaddm  12635  modgcd  12642  dvdsgcd  12663  dvdsgcdb  12664  gcdass  12666  mulgcd  12667  absmulgcd  12668  rpmulgcd  12677  nn0seqcvgd  12693  algcvga  12703  lcmdvds  12731  lcmdvdsb  12736  lcmass  12737  coprmdvds  12744  coprmdvds2  12745  rpmul  12750  cncongr1  12755  cncongr2  12756  prmgt1  12784  qnumdenbi  12844  coprimeprodsq  12910  pythagtriplem4  12921  pythagtriplem8  12925  pythagtriplem9  12926  pythagtriplem12  12928  pythagtriplem14  12930  pythagtriplem16  12932  pcpremul  12946  pcgcd  12982  setsvala  13193  setsex  13194  ressval2  13229  isgrpi  13687  grpsubrcan  13744  grpinvsub  13745  grpsubeq0  13749  grpsubadd0sub  13750  grpnpcan  13755  qussub  13904  ghmsub  13918  opprmulg  14165  rrgeq0  14360  lmodvsubval2  14438  rmodislmodlem  14446  rmodislmod  14447  lssintclm  14480  lssincl  14481  rnglidlmmgm  14592  cncrng  14665  unopn  14816  clsss  14929  opnssneib  14967  restabs  14986  upxp  15083  blpnfctr  15250  mscl  15276  xmscl  15277  xmsge0  15278  xmseq0  15279  mpomulcn  15377  rpdivcxp  15722  cxpcom  15749  rplogbreexp  15764  rplogbzexp  15765  rprelogbmulexp  15767  logbleb  15772  logblt  15773  lgsneg  15843  lgsne0  15857  lgsmodeq  15864  lgsmulsqcoprm  15865  gausslemma2dlem1a  15877  funvtxdm2domval  15970  funiedgdm2domval  15971  iedgedgg  16002  iswlk  16264  uspgr2wlkeq  16306  uspgr2wlkeq2  16307  uspgr2wlkeqi  16308  istrl  16326  clwwlkgt0  16337  iseupth  16388  bj-peano4  16671