Theorem 3adant1 980

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 961	. 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 103   /\ w3a 943

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 945

This theorem is referenced by:  3ad2ant2  984  3ad2ant3  985  rsp2e  2455  sbciegft  2905  reuhyp  4351  suc11g  4430  soinxp  4567  breldmg  4703  funopg  5113  funimaexglem  5162  fex2  5247  fnreseql  5482  ftpg  5556  mpoeq3ia  5788  mpofvex  6053  poxp  6081  smores3  6142  tfrlemibxssdm  6176  nndi  6334  nnmass  6335  nndir  6338  fnsnsplitdc  6353  nnaord  6357  nnaordr  6358  nnawordi  6363  nnmord  6365  ecopovtrn  6478  ecopovtrng  6481  ixpf  6566  mapxpen  6693  ltsopi  7070  addassnqg  7132  ltsonq  7148  ltmnqg  7151  distrnq0  7209  addlocpr  7286  distrlem1prl  7332  distrlem1pru  7333  distrlem4prl  7334  distrlem4pru  7335  ltpopr  7345  ltsopr  7346  addcanprg  7366  lttrsr  7499  ltsosr  7501  ltasrg  7507  recexgt0sr  7510  mulextsr1lem  7516  mulextsr1  7517  axpre-mulext  7617  adddir  7675  axltwlin  7750  axlttrn  7751  ltleletr  7763  letr  7764  mul32  7809  mul31  7810  add32  7838  subsub23  7884  addsubass  7889  subcan2  7904  subsub2  7907  nppcan2  7910  sub32  7913  nnncan  7914  nnncan2  7916  pnpcan2  7919  subdi  8060  subdir  8061  reapcotr  8272  receuap  8337  divmulap3  8344  divrecap  8355  divrecap2  8356  divsubdirap  8375  divdivap1  8390  redivclap  8398  div2negap  8402  ltmul2  8518  lemul2  8519  lemul2a  8521  lediv1  8531  gt0div  8532  ge0div  8533  ltdivmul  8538  ltdivmul2  8540  ledivmul2  8542  uzind2  9061  nn0ind  9063  fnn0ind  9065  uz3m2nn  9264  xrletr  9478  xrre2  9491  xleadd2a  9544  xleadd1  9545  xltadd2  9547  ixxdisj  9573  iooneg  9658  iccneg  9659  icoshft  9660  icoshftf1o  9661  icodisj  9662  fzen  9710  fzrev3  9754  2ffzeq  9805  fzoaddel2  9857  elfzodifsumelfzo  9865  ssfzo12bi  9889  fzoshftral  9902  adddivflid  9952  fldiv4p1lem1div2  9965  modqmulnn  10002  modqeqmodmin  10054  frec2uzf1od  10066  expdivap  10231  shftval2  10485  mulreap  10523  absdivap  10728  absdiflt  10750  absdifle  10751  abs3dif  10763  cau3  10773  ltmininf  10892  xrmaxlesup  10914  xrltmininf  10925  xrlemininf  10926  xrminltinf  10927  geoisum1c  11175  dvdsmulc  11363  dvdsmultr1  11373  dvdsmultr2  11375  dvdssub2  11377  oexpneg  11416  divalgb  11464  ndvdsadd  11470  gcdaddm  11514  modgcd  11521  dvdsgcd  11540  dvdsgcdb  11541  gcdass  11543  mulgcd  11544  absmulgcd  11545  rpmulgcd  11554  nn0seqcvgd  11562  algcvga  11572  lcmdvds  11600  lcmdvdsb  11605  lcmass  11606  coprmdvds  11613  coprmdvds2  11614  rpmul  11619  cncongr1  11624  cncongr2  11625  prmgt1  11652  qnumdenbi  11709  setsvala  11827  setsex  11828  unopn  12009  clsss  12124  opnssneib  12162  restabs  12181  upxp  12277  blpnfctr  12422  mscl  12448  xmscl  12449  xmsge0  12450  xmseq0  12451  bj-peano4  12836