Theorem 3adant1 1018

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 999	. 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 981

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 983

This theorem is referenced by:  3ad2ant2  1022  3ad2ant3  1023  rsp2e  2559  sbciegft  3036  reuhyp  4537  suc11g  4623  soinxp  4763  breldmg  4903  funopg  5324  funimaexglem  5376  fex2  5464  fnreseql  5713  ftpg  5791  mpoeq3ia  6033  funexw  6220  mpofvex  6314  poxp  6341  smores3  6402  tfrlemibxssdm  6436  nndi  6595  nnmass  6596  nndir  6599  fnsnsplitdc  6614  nnaord  6618  nnaordr  6619  nnawordi  6624  nnmord  6626  ecopovtrn  6742  ecopovtrng  6745  ixpf  6830  f1oen4g  6866  f1dom4g  6867  mapxpen  6970  netap  7401  2omotaplemap  7404  ltsopi  7468  addassnqg  7530  ltsonq  7546  ltmnqg  7549  distrnq0  7607  addlocpr  7684  distrlem1prl  7730  distrlem1pru  7731  distrlem4prl  7732  distrlem4pru  7733  ltpopr  7743  ltsopr  7744  addcanprg  7764  lttrsr  7910  ltsosr  7912  ltasrg  7918  recexgt0sr  7921  mulextsr1lem  7928  mulextsr1  7929  axpre-mulext  8036  adddir  8098  axltwlin  8175  axlttrn  8176  ltleletr  8189  letr  8190  mul32  8237  mul31  8238  add32  8266  subsub23  8312  addsubass  8317  subcan2  8332  subsub2  8335  nppcan2  8338  sub32  8341  nnncan  8342  nnncan2  8344  pnpcan2  8347  subdi  8492  subdir  8493  reapcotr  8706  receuap  8777  divmulap3  8785  divrecap  8796  divrecap2  8797  divsubdirap  8816  divdivap1  8831  redivclap  8839  div2negap  8843  ltmul2  8964  lemul2  8965  lemul2a  8967  lediv1  8977  gt0div  8978  ge0div  8979  ltdivmul  8984  ltdivmul2  8986  ledivmul2  8988  uzind2  9520  nn0ind  9522  fnn0ind  9524  uz3m2nn  9729  xrletr  9965  xrre2  9978  xleadd2a  10031  xleadd1  10032  xltadd2  10034  ixxdisj  10060  iooneg  10145  iccneg  10146  icoshft  10147  icoshftf1o  10148  icodisj  10149  fzen  10200  fzrev3  10244  2ffzeq  10298  fzoaddel2  10356  elfzodifsumelfzo  10367  ssfzo12bi  10391  fzoshftral  10404  adddivflid  10472  fldiv4p1lem1div2  10485  modqmulnn  10524  modqeqmodmin  10576  frec2uzf1od  10588  expdivap  10772  ccatval1  11091  ccatass  11102  fzowrddc  11138  swrdval  11139  swrdnd  11150  swrd0g  11151  swrdfv2  11154  pfxsuff1eqwrdeq  11190  swrdswrdlem  11195  pfxccatin12lem2a  11218  pfxccatin12lem1  11219  shftval2  11252  mulreap  11290  absdivap  11496  absdiflt  11518  absdifle  11519  abs3dif  11531  cau3  11541  ltmininf  11661  xrmaxlesup  11685  xrltmininf  11696  xrlemininf  11697  xrminltinf  11698  geoisum1c  11946  dvdsmulc  12245  dvdsmultr1  12257  dvdsmultr2  12259  dvdssub2  12261  oexpneg  12303  divalgb  12351  ndvdsadd  12357  gcdaddm  12420  modgcd  12427  dvdsgcd  12448  dvdsgcdb  12449  gcdass  12451  mulgcd  12452  absmulgcd  12453  rpmulgcd  12462  nn0seqcvgd  12478  algcvga  12488  lcmdvds  12516  lcmdvdsb  12521  lcmass  12522  coprmdvds  12529  coprmdvds2  12530  rpmul  12535  cncongr1  12540  cncongr2  12541  prmgt1  12569  qnumdenbi  12629  coprimeprodsq  12695  pythagtriplem4  12706  pythagtriplem8  12710  pythagtriplem9  12711  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem16  12717  pcpremul  12731  pcgcd  12767  setsvala  12978  setsex  12979  ressval2  13013  isgrpi  13471  grpsubrcan  13528  grpinvsub  13529  grpsubeq0  13533  grpsubadd0sub  13534  grpnpcan  13539  qussub  13688  ghmsub  13702  opprmulg  13948  rrgeq0  14142  lmodvsubval2  14219  rmodislmodlem  14227  rmodislmod  14228  lssintclm  14261  lssincl  14262  rnglidlmmgm  14373  cncrng  14446  unopn  14592  clsss  14705  opnssneib  14743  restabs  14762  upxp  14859  blpnfctr  15026  mscl  15052  xmscl  15053  xmsge0  15054  xmseq0  15055  mpomulcn  15153  rpdivcxp  15498  cxpcom  15525  rplogbreexp  15540  rplogbzexp  15541  rprelogbmulexp  15543  logbleb  15548  logblt  15549  lgsneg  15616  lgsne0  15630  lgsmodeq  15637  lgsmulsqcoprm  15638  gausslemma2dlem1a  15650  funvtxdm2domval  15743  funiedgdm2domval  15744  iedgedgg  15772  bj-peano4  16090