Theorem 3adant1 1015

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 996	. 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 978

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 980

This theorem is referenced by:  3ad2ant2  1019  3ad2ant3  1020  rsp2e  2528  sbciegft  2993  reuhyp  4472  suc11g  4556  soinxp  4696  breldmg  4833  funopg  5250  funimaexglem  5299  fex2  5384  fnreseql  5626  ftpg  5700  mpoeq3ia  5939  funexw  6112  mpofvex  6203  poxp  6232  smores3  6293  tfrlemibxssdm  6327  nndi  6486  nnmass  6487  nndir  6490  fnsnsplitdc  6505  nnaord  6509  nnaordr  6510  nnawordi  6515  nnmord  6517  ecopovtrn  6631  ecopovtrng  6634  ixpf  6719  mapxpen  6847  netap  7252  2omotaplemap  7255  ltsopi  7318  addassnqg  7380  ltsonq  7396  ltmnqg  7399  distrnq0  7457  addlocpr  7534  distrlem1prl  7580  distrlem1pru  7581  distrlem4prl  7582  distrlem4pru  7583  ltpopr  7593  ltsopr  7594  addcanprg  7614  lttrsr  7760  ltsosr  7762  ltasrg  7768  recexgt0sr  7771  mulextsr1lem  7778  mulextsr1  7779  axpre-mulext  7886  adddir  7947  axltwlin  8024  axlttrn  8025  ltleletr  8038  letr  8039  mul32  8086  mul31  8087  add32  8115  subsub23  8161  addsubass  8166  subcan2  8181  subsub2  8184  nppcan2  8187  sub32  8190  nnncan  8191  nnncan2  8193  pnpcan2  8196  subdi  8341  subdir  8342  reapcotr  8554  receuap  8625  divmulap3  8633  divrecap  8644  divrecap2  8645  divsubdirap  8664  divdivap1  8679  redivclap  8687  div2negap  8691  ltmul2  8812  lemul2  8813  lemul2a  8815  lediv1  8825  gt0div  8826  ge0div  8827  ltdivmul  8832  ltdivmul2  8834  ledivmul2  8836  uzind2  9364  nn0ind  9366  fnn0ind  9368  uz3m2nn  9572  xrletr  9807  xrre2  9820  xleadd2a  9873  xleadd1  9874  xltadd2  9876  ixxdisj  9902  iooneg  9987  iccneg  9988  icoshft  9989  icoshftf1o  9990  icodisj  9991  fzen  10042  fzrev3  10086  2ffzeq  10140  fzoaddel2  10192  elfzodifsumelfzo  10200  ssfzo12bi  10224  fzoshftral  10237  adddivflid  10291  fldiv4p1lem1div2  10304  modqmulnn  10341  modqeqmodmin  10393  frec2uzf1od  10405  expdivap  10570  shftval2  10834  mulreap  10872  absdivap  11078  absdiflt  11100  absdifle  11101  abs3dif  11113  cau3  11123  ltmininf  11242  xrmaxlesup  11266  xrltmininf  11277  xrlemininf  11278  xrminltinf  11279  geoisum1c  11527  dvdsmulc  11825  dvdsmultr1  11837  dvdsmultr2  11839  dvdssub2  11841  oexpneg  11881  divalgb  11929  ndvdsadd  11935  gcdaddm  11984  modgcd  11991  dvdsgcd  12012  dvdsgcdb  12013  gcdass  12015  mulgcd  12016  absmulgcd  12017  rpmulgcd  12026  nn0seqcvgd  12040  algcvga  12050  lcmdvds  12078  lcmdvdsb  12083  lcmass  12084  coprmdvds  12091  coprmdvds2  12092  rpmul  12097  cncongr1  12102  cncongr2  12103  prmgt1  12131  qnumdenbi  12191  coprimeprodsq  12256  pythagtriplem4  12267  pythagtriplem8  12271  pythagtriplem9  12272  pythagtriplem12  12274  pythagtriplem14  12276  pythagtriplem16  12278  pcpremul  12292  pcgcd  12327  setsvala  12492  setsex  12493  ressval2  12525  isgrpi  12899  grpsubrcan  12950  grpinvsub  12951  grpsubeq0  12955  grpsubadd0sub  12956  grpnpcan  12961  opprmulg  13241  cncrng  13433  unopn  13475  clsss  13588  opnssneib  13626  restabs  13645  upxp  13742  blpnfctr  13909  mscl  13935  xmscl  13936  xmsge0  13937  xmseq0  13938  rpdivcxp  14302  cxpcom  14327  rplogbreexp  14341  rplogbzexp  14342  rprelogbmulexp  14344  logbleb  14349  logblt  14350  lgsneg  14395  lgsne0  14409  lgsmodeq  14416  lgsmulsqcoprm  14417  bj-peano4  14677