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  5492  fnreseql  5745  ftpg  5823  mpoeq3ia  6069  funexw  6257  mpofvex  6351  poxp  6378  smores3  6439  tfrlemibxssdm  6473  nndi  6632  nnmass  6633  nndir  6636  fnsnsplitdc  6651  nnaord  6655  nnaordr  6656  nnawordi  6661  nnmord  6663  ecopovtrn  6779  ecopovtrng  6782  ixpf  6867  f1oen4g  6903  f1dom4g  6904  mapxpen  7009  netap  7440  2omotaplemap  7443  ltsopi  7507  addassnqg  7569  ltsonq  7585  ltmnqg  7588  distrnq0  7646  addlocpr  7723  distrlem1prl  7769  distrlem1pru  7770  distrlem4prl  7771  distrlem4pru  7772  ltpopr  7782  ltsopr  7783  addcanprg  7803  lttrsr  7949  ltsosr  7951  ltasrg  7957  recexgt0sr  7960  mulextsr1lem  7967  mulextsr1  7968  axpre-mulext  8075  adddir  8137  axltwlin  8214  axlttrn  8215  ltleletr  8228  letr  8229  mul32  8276  mul31  8277  add32  8305  subsub23  8351  addsubass  8356  subcan2  8371  subsub2  8374  nppcan2  8377  sub32  8380  nnncan  8381  nnncan2  8383  pnpcan2  8386  subdi  8531  subdir  8532  reapcotr  8745  receuap  8816  divmulap3  8824  divrecap  8835  divrecap2  8836  divsubdirap  8855  divdivap1  8870  redivclap  8878  div2negap  8882  ltmul2  9003  lemul2  9004  lemul2a  9006  lediv1  9016  gt0div  9017  ge0div  9018  ltdivmul  9023  ltdivmul2  9025  ledivmul2  9027  uzind2  9559  nn0ind  9561  fnn0ind  9563  uz3m2nn  9768  xrletr  10004  xrre2  10017  xleadd2a  10070  xleadd1  10071  xltadd2  10073  ixxdisj  10099  iooneg  10184  iccneg  10185  icoshft  10186  icoshftf1o  10187  icodisj  10188  fzen  10239  fzrev3  10283  2ffzeq  10337  fzoaddel2  10396  elfzodifsumelfzo  10407  ssfzo12bi  10431  fzoshftral  10444  adddivflid  10512  fldiv4p1lem1div2  10525  modqmulnn  10564  modqeqmodmin  10616  frec2uzf1od  10628  expdivap  10812  ccatval1  11132  ccatass  11143  fzowrddc  11179  swrdval  11180  swrdnd  11191  swrd0g  11192  swrdfv2  11195  pfxsuff1eqwrdeq  11231  swrdswrdlem  11236  pfxccatin12lem2a  11259  pfxccatin12lem1  11260  shftval2  11337  mulreap  11375  absdivap  11581  absdiflt  11603  absdifle  11604  abs3dif  11616  cau3  11626  ltmininf  11746  xrmaxlesup  11770  xrltmininf  11781  xrlemininf  11782  xrminltinf  11783  geoisum1c  12031  dvdsmulc  12330  dvdsmultr1  12342  dvdsmultr2  12344  dvdssub2  12346  oexpneg  12388  divalgb  12436  ndvdsadd  12442  gcdaddm  12505  modgcd  12512  dvdsgcd  12533  dvdsgcdb  12534  gcdass  12536  mulgcd  12537  absmulgcd  12538  rpmulgcd  12547  nn0seqcvgd  12563  algcvga  12573  lcmdvds  12601  lcmdvdsb  12606  lcmass  12607  coprmdvds  12614  coprmdvds2  12615  rpmul  12620  cncongr1  12625  cncongr2  12626  prmgt1  12654  qnumdenbi  12714  coprimeprodsq  12780  pythagtriplem4  12791  pythagtriplem8  12795  pythagtriplem9  12796  pythagtriplem12  12798  pythagtriplem14  12800  pythagtriplem16  12802  pcpremul  12816  pcgcd  12852  setsvala  13063  setsex  13064  ressval2  13099  isgrpi  13557  grpsubrcan  13614  grpinvsub  13615  grpsubeq0  13619  grpsubadd0sub  13620  grpnpcan  13625  qussub  13774  ghmsub  13788  opprmulg  14034  rrgeq0  14229  lmodvsubval2  14306  rmodislmodlem  14314  rmodislmod  14315  lssintclm  14348  lssincl  14349  rnglidlmmgm  14460  cncrng  14533  unopn  14679  clsss  14792  opnssneib  14830  restabs  14849  upxp  14946  blpnfctr  15113  mscl  15139  xmscl  15140  xmsge0  15141  xmseq0  15142  mpomulcn  15240  rpdivcxp  15585  cxpcom  15612  rplogbreexp  15627  rplogbzexp  15628  rprelogbmulexp  15630  logbleb  15635  logblt  15636  lgsneg  15703  lgsne0  15717  lgsmodeq  15724  lgsmulsqcoprm  15725  gausslemma2dlem1a  15737  funvtxdm2domval  15830  funiedgdm2domval  15831  iedgedgg  15861  iswlk  16036  uspgr2wlkeq  16076  uspgr2wlkeq2  16077  uspgr2wlkeqi  16078  bj-peano4  16318