Theorem 3adant1 1017

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 998	. 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 980

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 982

This theorem is referenced by:  3ad2ant2  1021  3ad2ant3  1022  rsp2e  2548  sbciegft  3020  reuhyp  4507  suc11g  4593  soinxp  4733  breldmg  4872  funopg  5292  funimaexglem  5341  fex2  5426  fnreseql  5672  ftpg  5746  mpoeq3ia  5987  funexw  6169  mpofvex  6263  poxp  6290  smores3  6351  tfrlemibxssdm  6385  nndi  6544  nnmass  6545  nndir  6548  fnsnsplitdc  6563  nnaord  6567  nnaordr  6568  nnawordi  6573  nnmord  6575  ecopovtrn  6691  ecopovtrng  6694  ixpf  6779  mapxpen  6909  netap  7321  2omotaplemap  7324  ltsopi  7387  addassnqg  7449  ltsonq  7465  ltmnqg  7468  distrnq0  7526  addlocpr  7603  distrlem1prl  7649  distrlem1pru  7650  distrlem4prl  7651  distrlem4pru  7652  ltpopr  7662  ltsopr  7663  addcanprg  7683  lttrsr  7829  ltsosr  7831  ltasrg  7837  recexgt0sr  7840  mulextsr1lem  7847  mulextsr1  7848  axpre-mulext  7955  adddir  8017  axltwlin  8094  axlttrn  8095  ltleletr  8108  letr  8109  mul32  8156  mul31  8157  add32  8185  subsub23  8231  addsubass  8236  subcan2  8251  subsub2  8254  nppcan2  8257  sub32  8260  nnncan  8261  nnncan2  8263  pnpcan2  8266  subdi  8411  subdir  8412  reapcotr  8625  receuap  8696  divmulap3  8704  divrecap  8715  divrecap2  8716  divsubdirap  8735  divdivap1  8750  redivclap  8758  div2negap  8762  ltmul2  8883  lemul2  8884  lemul2a  8886  lediv1  8896  gt0div  8897  ge0div  8898  ltdivmul  8903  ltdivmul2  8905  ledivmul2  8907  uzind2  9438  nn0ind  9440  fnn0ind  9442  uz3m2nn  9647  xrletr  9883  xrre2  9896  xleadd2a  9949  xleadd1  9950  xltadd2  9952  ixxdisj  9978  iooneg  10063  iccneg  10064  icoshft  10065  icoshftf1o  10066  icodisj  10067  fzen  10118  fzrev3  10162  2ffzeq  10216  fzoaddel2  10269  elfzodifsumelfzo  10277  ssfzo12bi  10301  fzoshftral  10314  adddivflid  10382  fldiv4p1lem1div2  10395  modqmulnn  10434  modqeqmodmin  10486  frec2uzf1od  10498  expdivap  10682  shftval2  10991  mulreap  11029  absdivap  11235  absdiflt  11257  absdifle  11258  abs3dif  11270  cau3  11280  ltmininf  11400  xrmaxlesup  11424  xrltmininf  11435  xrlemininf  11436  xrminltinf  11437  geoisum1c  11685  dvdsmulc  11984  dvdsmultr1  11996  dvdsmultr2  11998  dvdssub2  12000  oexpneg  12042  divalgb  12090  ndvdsadd  12096  gcdaddm  12151  modgcd  12158  dvdsgcd  12179  dvdsgcdb  12180  gcdass  12182  mulgcd  12183  absmulgcd  12184  rpmulgcd  12193  nn0seqcvgd  12209  algcvga  12219  lcmdvds  12247  lcmdvdsb  12252  lcmass  12253  coprmdvds  12260  coprmdvds2  12261  rpmul  12266  cncongr1  12271  cncongr2  12272  prmgt1  12300  qnumdenbi  12360  coprimeprodsq  12426  pythagtriplem4  12437  pythagtriplem8  12441  pythagtriplem9  12442  pythagtriplem12  12444  pythagtriplem14  12446  pythagtriplem16  12448  pcpremul  12462  pcgcd  12498  setsvala  12709  setsex  12710  ressval2  12744  isgrpi  13156  grpsubrcan  13213  grpinvsub  13214  grpsubeq0  13218  grpsubadd0sub  13219  grpnpcan  13224  qussub  13367  ghmsub  13381  opprmulg  13627  rrgeq0  13821  lmodvsubval2  13898  rmodislmodlem  13906  rmodislmod  13907  lssintclm  13940  lssincl  13941  rnglidlmmgm  14052  cncrng  14125  unopn  14241  clsss  14354  opnssneib  14392  restabs  14411  upxp  14508  blpnfctr  14675  mscl  14701  xmscl  14702  xmsge0  14703  xmseq0  14704  mpomulcn  14802  rpdivcxp  15147  cxpcom  15174  rplogbreexp  15189  rplogbzexp  15190  rprelogbmulexp  15192  logbleb  15197  logblt  15198  lgsneg  15265  lgsne0  15279  lgsmodeq  15286  lgsmulsqcoprm  15287  gausslemma2dlem1a  15299  bj-peano4  15601