Theorem 3adant1 1039

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 1020	. 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 1002

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 1004

This theorem is referenced by:  3ad2ant2  1043  3ad2ant3  1044  rsp2e  2581  sbciegft  3059  reuhyp  4563  suc11g  4649  soinxp  4789  breldmg  4929  funopg  5352  funimaexglem  5404  fex2  5494  fnreseql  5747  ftpg  5827  mpoeq3ia  6075  funexw  6263  mpofvex  6357  poxp  6384  smores3  6445  tfrlemibxssdm  6479  nndi  6640  nnmass  6641  nndir  6644  fnsnsplitdc  6659  nnaord  6663  nnaordr  6664  nnawordi  6669  nnmord  6671  ecopovtrn  6787  ecopovtrng  6790  ixpf  6875  f1oen4g  6911  f1dom4g  6912  mapxpen  7017  netap  7451  2omotaplemap  7454  ltsopi  7518  addassnqg  7580  ltsonq  7596  ltmnqg  7599  distrnq0  7657  addlocpr  7734  distrlem1prl  7780  distrlem1pru  7781  distrlem4prl  7782  distrlem4pru  7783  ltpopr  7793  ltsopr  7794  addcanprg  7814  lttrsr  7960  ltsosr  7962  ltasrg  7968  recexgt0sr  7971  mulextsr1lem  7978  mulextsr1  7979  axpre-mulext  8086  adddir  8148  axltwlin  8225  axlttrn  8226  ltleletr  8239  letr  8240  mul32  8287  mul31  8288  add32  8316  subsub23  8362  addsubass  8367  subcan2  8382  subsub2  8385  nppcan2  8388  sub32  8391  nnncan  8392  nnncan2  8394  pnpcan2  8397  subdi  8542  subdir  8543  reapcotr  8756  receuap  8827  divmulap3  8835  divrecap  8846  divrecap2  8847  divsubdirap  8866  divdivap1  8881  redivclap  8889  div2negap  8893  ltmul2  9014  lemul2  9015  lemul2a  9017  lediv1  9027  gt0div  9028  ge0div  9029  ltdivmul  9034  ltdivmul2  9036  ledivmul2  9038  uzind2  9570  nn0ind  9572  fnn0ind  9574  uz3m2nn  9780  xrletr  10016  xrre2  10029  xleadd2a  10082  xleadd1  10083  xltadd2  10085  ixxdisj  10111  iooneg  10196  iccneg  10197  icoshft  10198  icoshftf1o  10199  icodisj  10200  fzen  10251  fzrev3  10295  2ffzeq  10349  fzoaddel2  10408  elfzodifsumelfzo  10419  ssfzo12bi  10443  fzoshftral  10456  adddivflid  10524  fldiv4p1lem1div2  10537  modqmulnn  10576  modqeqmodmin  10628  frec2uzf1od  10640  expdivap  10824  ccatval1  11145  ccatass  11156  fzowrddc  11195  swrdval  11196  swrdnd  11207  swrd0g  11208  swrdfv2  11211  pfxsuff1eqwrdeq  11247  swrdswrdlem  11252  pfxccatin12lem2a  11275  pfxccatin12lem1  11276  shftval2  11353  mulreap  11391  absdivap  11597  absdiflt  11619  absdifle  11620  abs3dif  11632  cau3  11642  ltmininf  11762  xrmaxlesup  11786  xrltmininf  11797  xrlemininf  11798  xrminltinf  11799  geoisum1c  12047  dvdsmulc  12346  dvdsmultr1  12358  dvdsmultr2  12360  dvdssub2  12362  oexpneg  12404  divalgb  12452  ndvdsadd  12458  gcdaddm  12521  modgcd  12528  dvdsgcd  12549  dvdsgcdb  12550  gcdass  12552  mulgcd  12553  absmulgcd  12554  rpmulgcd  12563  nn0seqcvgd  12579  algcvga  12589  lcmdvds  12617  lcmdvdsb  12622  lcmass  12623  coprmdvds  12630  coprmdvds2  12631  rpmul  12636  cncongr1  12641  cncongr2  12642  prmgt1  12670  qnumdenbi  12730  coprimeprodsq  12796  pythagtriplem4  12807  pythagtriplem8  12811  pythagtriplem9  12812  pythagtriplem12  12814  pythagtriplem14  12816  pythagtriplem16  12818  pcpremul  12832  pcgcd  12868  setsvala  13079  setsex  13080  ressval2  13115  isgrpi  13573  grpsubrcan  13630  grpinvsub  13631  grpsubeq0  13635  grpsubadd0sub  13636  grpnpcan  13641  qussub  13790  ghmsub  13804  opprmulg  14050  rrgeq0  14245  lmodvsubval2  14322  rmodislmodlem  14330  rmodislmod  14331  lssintclm  14364  lssincl  14365  rnglidlmmgm  14476  cncrng  14549  unopn  14695  clsss  14808  opnssneib  14846  restabs  14865  upxp  14962  blpnfctr  15129  mscl  15155  xmscl  15156  xmsge0  15157  xmseq0  15158  mpomulcn  15256  rpdivcxp  15601  cxpcom  15628  rplogbreexp  15643  rplogbzexp  15644  rprelogbmulexp  15646  logbleb  15651  logblt  15652  lgsneg  15719  lgsne0  15733  lgsmodeq  15740  lgsmulsqcoprm  15741  gausslemma2dlem1a  15753  funvtxdm2domval  15846  funiedgdm2domval  15847  iedgedgg  15877  iswlk  16069  uspgr2wlkeq  16111  uspgr2wlkeq2  16112  uspgr2wlkeqi  16113  istrl  16129  clwwlkgt0  16139  bj-peano4  16401