Theorem 3adant3 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
3adant3	|- ( ( ph /\ ps /\ th ) -> ch )

Proof of Theorem 3adant3

Step	Hyp	Ref	Expression
1		3simpa 994	. 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 104   /\ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  stoic4a  1432  stoic4b  1433  vtoclgft  2788  eqeu  2908  tpssi  3760  issod  4320  sotricim  4324  soinxp  4697  funopg  5251  fnco  5325  resasplitss  5396  resdif  5484  fnimapr  5577  ftpg  5701  fsnunfv  5718  fvpr1g  5723  fvpr2g  5724  f1ocnvfvb  5781  f1oiso2  5828  moriotass  5859  f1ofveu  5863  acexmid  5874  ovig  5996  ov6g  6012  ovg  6013  ot1stg  6153  ot2ndg  6154  poxp  6233  brtposg  6255  smores3  6294  smoiso  6303  rdgivallem  6382  frecsuclem  6407  nnaord  6510  nnaword  6512  nnawordex  6530  ecopovtrn  6632  ecopovtrng  6635  xpdom3m  6834  mapxpen  6848  sbthlemi4  6959  djuenun  7211  netap  7253  2omotaplemap  7256  ltsopi  7319  addcanpig  7333  distrnqg  7386  ltsonq  7397  ltanqg  7399  ltmnqg  7400  nnanq0  7457  distrnq0  7458  distnq0r  7462  prarloclem  7500  genpassl  7523  genpassu  7524  distrlem1prl  7581  distrlem1pru  7582  distrlem5prl  7585  distrlem5pru  7586  1idprl  7589  1idpru  7590  ltpopr  7594  ltsopr  7595  ltexprlemm  7599  ltexprlemfl  7608  ltexprlemfu  7610  addcanprlemu  7614  recexprlem1ssl  7632  recexprlem1ssu  7633  aptipr  7640  lttrsr  7761  ltsosr  7763  ltasrg  7769  recexgt0sr  7772  mulextsr1  7780  axmulass  7872  ltxrlt  8023  axltwlin  8025  axlttrn  8026  axltadd  8027  letr  8040  mul12  8086  add12  8115  subadd  8160  addsub  8168  npncan  8178  nppcan  8179  nnpcan  8180  nppcan3  8181  pnpcan  8196  pnncan  8198  ppncan  8199  subdi  8342  ltaddsub2  8394  leaddsub2  8396  ltaddsublt  8528  apreap  8544  lemul1  8550  reapmul1lem  8551  reapadd1  8553  reapcotr  8555  receuap  8626  divassap  8647  div23ap  8648  divmulassap  8652  divmulasscomap  8653  divcanap4  8656  divsubdirap  8665  divcanap5  8671  divdiv32ap  8677  divdivap2  8681  div2subap  8794  letrp1  8805  ltmulgt12  8822  lediv1  8826  ltdiv2  8844  lediv2  8848  lbinfle  8907  difgtsumgt  9322  xrletr  9808  xrre2  9821  xaddass  9869  ixxdisj  9903  ubioc1  9929  lbico1  9930  elioo5  9933  iccsupr  9966  lbicc2  9984  ubicc2  9985  iccneg  9989  icoshft  9990  icodisj  9992  iccf1o  10004  iccen  10006  zltaddlt1le  10007  fztri3or  10039  fzdcel  10040  fzen  10043  uzsubsubfz  10047  fzrevral2  10106  fzshftral  10108  fz0fzdiffz0  10130  difelfznle  10135  fzo1fzo0n0  10183  fzonmapblen  10187  fzosubel2  10195  ubmelfzo  10200  elfzodifsumelfzo  10201  ssfzo12bi  10225  ubmelm1fzo  10226  subfzo0  10242  ceiqle  10313  modqid2  10351  zmodidfzoimp  10354  addmodidr  10373  modfzo0difsn  10395  addmodlteq  10398  frec2uzf1od  10406  exprecap  10561  expdivap  10571  expubnd  10577  sqdivap  10584  mulbinom2  10637  bernneq2  10642  mulsubdivbinom2ap  10691  bcval3  10731  bccmpl  10734  omgadd  10782  shftval2  10835  mulreap  10873  elicc4abs  11103  abssubge0  11111  abssuble0  11112  maxleast  11222  maxltsup  11227  xrmaxltsup  11266  xrmineqinf  11277  xrltmininf  11278  xrlemininf  11279  fsumdifsnconst  11463  prodfap0  11553  prodfrecap  11554  fprodabs  11624  sin01gt0  11769  cos01gt0  11770  sin02gt0  11771  dvdscmul  11825  summodnegmod  11829  modmulconst  11830  dvdsleabs  11851  dvdsleabs2  11852  addmodlteqALT  11865  dvdsexp  11867  mulmoddvds  11869  divalgb  11930  divgcdz  11972  gcdass  12016  mulgcdr  12019  gcddiv  12020  uzwodc  12038  lcmass  12085  coprmdvds  12092  qredeq  12096  qredeu  12097  congr  12100  divgcdcoprm0  12101  divgcdcoprmex  12102  cncongr1  12103  cncongr2  12104  isprm3  12118  dvdsnprmd  12125  euclemma  12146  prmdvdsexpb  12149  prmexpb  12151  rpexp  12153  znege1  12178  modprminv  12249  modprminveq  12250  vfermltl  12251  modprm0  12254  modprmn0modprm0  12256  coprimeprodsq  12257  coprimeprodsq2  12258  pythagtriplem1  12265  pythagtriplem3  12267  pythagtriplem6  12270  pythagtriplem12  12275  pythagtriplem13  12276  pythagtriplem14  12277  pythagtriplem16  12279  pythagtriplem19  12282  pythagtrip  12283  pcmul  12301  pcdiv  12302  pcqcl  12306  pcgcd1  12327  pcgcd  12328  dvdsprmpweq  12334  difsqpwdvds  12337  pcfaclem  12347  unbendc  12455  strle3g  12567  ercpbl  12750  grpinvid1  12924  grpinvid2  12925  grpasscan1  12933  grpasscan2  12934  grpidrcan  12935  grpidlcan  12936  grpinvadd  12948  grpsubadd  12958  grppncan  12961  subcmnd  13129  mulgass2  13235  dvrcan1  13309  dvrcan3  13310  rmodislmodlem  13440  rmodislmod  13441  basgen  13583  clsss  13621  ntrin  13627  ntrcls0  13634  neiint  13648  neiss  13653  neipsm  13657  opnssneib  13659  innei  13666  restco  13677  iscnp  13702  cnconst2  13736  txcn  13778  psmetsym  13832  psmetlecl  13837  distspace  13838  xmetlecl  13870  xmetsym  13871  xblcntrps  13916  xblcntr  13917  blssec  13941  blpnfctr  13942  txmetcn  14022  cnmet  14033  dvid  14165  ptolemy  14248  sinq12gt0  14254  sincosq1eq  14263  rpcxpsub  14332  relogbexpap  14379  logbleb  14382  logblt  14383  rplogbcxp  14384  lgsval4  14424  lgsmod  14430  lgsne0  14442  lgsmulsqcoprm  14450  2lgsoddprmlem1  14456