Theorem 3adant3 964

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)

Hypothesis

Ref	Expression
3adant.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
3adant3	|- ( ( ph /\ ps /\ th ) -> ch )

Proof of Theorem 3adant3

Step	Hyp	Ref	Expression
1		3simpa 941	. 2 |- ( ( ph /\ ps /\ th ) -> ( ph /\ ps ) )
2		3adant.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	syl 14	1 |- ( ( ph /\ ps /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 925

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

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

This theorem is referenced by:  stoic4a  1367  stoic4b  1368  vtoclgft  2672  eqeu  2788  tpssi  3611  issod  4157  sotricim  4161  soinxp  4523  funopg  5063  fnco  5137  resasplitss  5205  resdif  5290  fnimapr  5379  ftpg  5497  fsnunfv  5514  fvpr1g  5519  fvpr2g  5520  f1ocnvfvb  5575  f1oiso2  5622  moriotass  5652  f1ofveu  5656  acexmid  5667  ovig  5782  ov6g  5798  ovg  5799  ot1stg  5939  ot2ndg  5940  poxp  6013  brtposg  6035  smores3  6074  smoiso  6083  rdgivallem  6162  frecsuclem  6187  nnaord  6284  nnaword  6286  nnawordex  6303  ecopovtrn  6405  ecopovtrng  6408  xpdom3m  6606  mapxpen  6620  sbthlemi4  6725  ltsopi  6942  addcanpig  6956  distrnqg  7009  ltsonq  7020  ltanqg  7022  ltmnqg  7023  nnanq0  7080  distrnq0  7081  distnq0r  7085  prarloclem  7123  genpassl  7146  genpassu  7147  distrlem1prl  7204  distrlem1pru  7205  distrlem5prl  7208  distrlem5pru  7209  1idprl  7212  1idpru  7213  ltpopr  7217  ltsopr  7218  ltexprlemm  7222  ltexprlemfl  7231  ltexprlemfu  7233  addcanprlemu  7237  recexprlem1ssl  7255  recexprlem1ssu  7256  aptipr  7263  lttrsr  7371  ltsosr  7373  ltasrg  7379  recexgt0sr  7382  mulextsr1  7389  axmulass  7471  ltxrlt  7615  axltwlin  7617  axlttrn  7618  axltadd  7619  letr  7631  mul12  7674  add12  7703  subadd  7748  addsub  7756  npncan  7766  nppcan  7767  nnpcan  7768  nppcan3  7769  pnpcan  7784  pnncan  7786  ppncan  7787  subdi  7926  ltaddsub2  7978  leaddsub2  7980  ltaddsublt  8111  apreap  8127  lemul1  8133  reapmul1lem  8134  reapadd1  8136  reapcotr  8138  receuap  8201  divassap  8220  div23ap  8221  divmulassap  8225  divmulasscomap  8226  divcanap4  8229  divsubdirap  8238  divcanap5  8244  divdiv32ap  8250  divdivap2  8254  div2subap  8365  letrp1  8372  ltmulgt12  8389  lediv1  8393  ltdiv2  8411  lediv2  8415  lbinfle  8474  xrletr  9336  xrre2  9346  ixxdisj  9384  ubioc1  9410  lbico1  9411  elioo5  9414  iccsupr  9447  lbicc2  9464  ubicc2  9465  iccneg  9469  icoshft  9470  icodisj  9472  iccf1o  9484  zltaddlt1le  9486  fztri3or  9516  fzdcel  9517  fzen  9520  uzsubsubfz  9524  fzrevral2  9583  fzshftral  9585  fz0fzdiffz0  9604  difelfznle  9609  fzo1fzo0n0  9657  fzonmapblen  9661  fzosubel2  9669  ubmelfzo  9674  elfzodifsumelfzo  9675  ssfzo12bi  9699  ubmelm1fzo  9700  subfzo0  9716  ceiqle  9783  modqid2  9821  zmodidfzoimp  9824  addmodidr  9843  modfzo0difsn  9865  addmodlteq  9868  frec2uzf1od  9876  exprecap  10059  expdivap  10069  expubnd  10075  sqdivap  10082  mulbinom2  10133  bernneq2  10138  bcval3  10222  bccmpl  10225  omgadd  10273  shftval2  10323  mulreap  10361  elicc4abs  10590  abssubge0  10598  abssuble0  10599  maxleast  10709  maxltsup  10714  fsumdifsnconst  10912  sin01gt0  11115  cos01gt0  11116  sin02gt0  11117  dvdscmul  11164  summodnegmod  11168  modmulconst  11169  dvdsleabs  11187  dvdsleabs2  11188  addmodlteqALT  11201  dvdsexp  11203  mulmoddvds  11205  divalgb  11266  divgcdz  11304  gcdass  11345  mulgcdr  11348  gcddiv  11349  lcmass  11408  coprmdvds  11415  qredeq  11419  qredeu  11420  congr  11423  divgcdcoprm0  11424  divgcdcoprmex  11425  cncongr1  11426  cncongr2  11427  isprm3  11441  dvdsnprmd  11448  euclemma  11466  prmdvdsexpb  11469  prmexpb  11471  rpexp  11473  znege1  11497  strle3g  11649  basgen  11843  clsss  11881  ntrin  11887  ntrcls0  11894  neiint  11908  neiss  11913  neipsm  11917  opnssneib  11919  innei  11926