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  2557  sbciegft  3029  reuhyp  4520  suc11g  4606  soinxp  4746  breldmg  4885  funopg  5306  funimaexglem  5358  fex2  5446  fnreseql  5692  ftpg  5770  mpoeq3ia  6012  funexw  6199  mpofvex  6293  poxp  6320  smores3  6381  tfrlemibxssdm  6415  nndi  6574  nnmass  6575  nndir  6578  fnsnsplitdc  6593  nnaord  6597  nnaordr  6598  nnawordi  6603  nnmord  6605  ecopovtrn  6721  ecopovtrng  6724  ixpf  6809  f1oen4g  6845  f1dom4g  6846  mapxpen  6947  netap  7368  2omotaplemap  7371  ltsopi  7435  addassnqg  7497  ltsonq  7513  ltmnqg  7516  distrnq0  7574  addlocpr  7651  distrlem1prl  7697  distrlem1pru  7698  distrlem4prl  7699  distrlem4pru  7700  ltpopr  7710  ltsopr  7711  addcanprg  7731  lttrsr  7877  ltsosr  7879  ltasrg  7885  recexgt0sr  7888  mulextsr1lem  7895  mulextsr1  7896  axpre-mulext  8003  adddir  8065  axltwlin  8142  axlttrn  8143  ltleletr  8156  letr  8157  mul32  8204  mul31  8205  add32  8233  subsub23  8279  addsubass  8284  subcan2  8299  subsub2  8302  nppcan2  8305  sub32  8308  nnncan  8309  nnncan2  8311  pnpcan2  8314  subdi  8459  subdir  8460  reapcotr  8673  receuap  8744  divmulap3  8752  divrecap  8763  divrecap2  8764  divsubdirap  8783  divdivap1  8798  redivclap  8806  div2negap  8810  ltmul2  8931  lemul2  8932  lemul2a  8934  lediv1  8944  gt0div  8945  ge0div  8946  ltdivmul  8951  ltdivmul2  8953  ledivmul2  8955  uzind2  9487  nn0ind  9489  fnn0ind  9491  uz3m2nn  9696  xrletr  9932  xrre2  9945  xleadd2a  9998  xleadd1  9999  xltadd2  10001  ixxdisj  10027  iooneg  10112  iccneg  10113  icoshft  10114  icoshftf1o  10115  icodisj  10116  fzen  10167  fzrev3  10211  2ffzeq  10265  fzoaddel2  10321  elfzodifsumelfzo  10332  ssfzo12bi  10356  fzoshftral  10369  adddivflid  10437  fldiv4p1lem1div2  10450  modqmulnn  10489  modqeqmodmin  10541  frec2uzf1od  10553  expdivap  10737  ccatval1  11056  ccatass  11067  fzowrddc  11103  swrdval  11104  swrdnd  11115  swrd0g  11116  swrdfv2  11119  pfxsuff1eqwrdeq  11153  shftval2  11170  mulreap  11208  absdivap  11414  absdiflt  11436  absdifle  11437  abs3dif  11449  cau3  11459  ltmininf  11579  xrmaxlesup  11603  xrltmininf  11614  xrlemininf  11615  xrminltinf  11616  geoisum1c  11864  dvdsmulc  12163  dvdsmultr1  12175  dvdsmultr2  12177  dvdssub2  12179  oexpneg  12221  divalgb  12269  ndvdsadd  12275  gcdaddm  12338  modgcd  12345  dvdsgcd  12366  dvdsgcdb  12367  gcdass  12369  mulgcd  12370  absmulgcd  12371  rpmulgcd  12380  nn0seqcvgd  12396  algcvga  12406  lcmdvds  12434  lcmdvdsb  12439  lcmass  12440  coprmdvds  12447  coprmdvds2  12448  rpmul  12453  cncongr1  12458  cncongr2  12459  prmgt1  12487  qnumdenbi  12547  coprimeprodsq  12613  pythagtriplem4  12624  pythagtriplem8  12628  pythagtriplem9  12629  pythagtriplem12  12631  pythagtriplem14  12633  pythagtriplem16  12635  pcpremul  12649  pcgcd  12685  setsvala  12896  setsex  12897  ressval2  12931  isgrpi  13389  grpsubrcan  13446  grpinvsub  13447  grpsubeq0  13451  grpsubadd0sub  13452  grpnpcan  13457  qussub  13606  ghmsub  13620  opprmulg  13866  rrgeq0  14060  lmodvsubval2  14137  rmodislmodlem  14145  rmodislmod  14146  lssintclm  14179  lssincl  14180  rnglidlmmgm  14291  cncrng  14364  unopn  14510  clsss  14623  opnssneib  14661  restabs  14680  upxp  14777  blpnfctr  14944  mscl  14970  xmscl  14971  xmsge0  14972  xmseq0  14973  mpomulcn  15071  rpdivcxp  15416  cxpcom  15443  rplogbreexp  15458  rplogbzexp  15459  rprelogbmulexp  15461  logbleb  15466  logblt  15467  lgsneg  15534  lgsne0  15548  lgsmodeq  15555  lgsmulsqcoprm  15556  gausslemma2dlem1a  15568  funvtxdm2domval  15659  funiedgdm2domval  15660  iedgedgg  15688  bj-peano4  15928