Theorem 3adant3 1020

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 997	. 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 981

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 983

This theorem is referenced by:  stoic4a  1452  stoic4b  1453  vtoclgft  2828  eqeu  2950  ssprsseq  3806  tpssi  3813  issod  4384  sotricim  4388  soinxp  4763  funopg  5324  fnco  5403  resasplitss  5477  resdif  5566  fnimapr  5662  ftpg  5791  fsnunfv  5808  fvpr1g  5813  fvpr2g  5814  f1ocnvfvb  5872  f1oiso2  5919  moriotass  5951  f1ofveu  5955  acexmid  5966  ovig  6090  ov6g  6107  ovg  6108  ot1stg  6261  ot2ndg  6262  poxp  6341  brtposg  6363  smores3  6402  smoiso  6411  rdgivallem  6490  frecsuclem  6515  nnaord  6618  nnaword  6620  nnawordex  6638  ecopovtrn  6742  ecopovtrng  6745  xpdom3m  6954  mapxpen  6970  sbthlemi4  7088  djuenun  7355  netap  7401  2omotaplemap  7404  ltsopi  7468  addcanpig  7482  distrnqg  7535  ltsonq  7546  ltanqg  7548  ltmnqg  7549  nnanq0  7606  distrnq0  7607  distnq0r  7611  prarloclem  7649  genpassl  7672  genpassu  7673  distrlem1prl  7730  distrlem1pru  7731  distrlem5prl  7734  distrlem5pru  7735  1idprl  7738  1idpru  7739  ltpopr  7743  ltsopr  7744  ltexprlemm  7748  ltexprlemfl  7757  ltexprlemfu  7759  addcanprlemu  7763  recexprlem1ssl  7781  recexprlem1ssu  7782  aptipr  7789  lttrsr  7910  ltsosr  7912  ltasrg  7918  recexgt0sr  7921  mulextsr1  7929  axmulass  8021  ltxrlt  8173  axltwlin  8175  axlttrn  8176  axltadd  8177  letr  8190  mul12  8236  add12  8265  subadd  8310  addsub  8318  npncan  8328  nppcan  8329  nnpcan  8330  nppcan3  8331  pnpcan  8346  pnncan  8348  ppncan  8349  subdi  8492  ltaddsub2  8545  leaddsub2  8547  ltaddsublt  8679  apreap  8695  lemul1  8701  reapmul1lem  8702  reapadd1  8704  reapcotr  8706  receuap  8777  divassap  8798  div23ap  8799  divmulassap  8803  divmulasscomap  8804  divcanap4  8807  divsubdirap  8816  divcanap5  8822  divdiv32ap  8828  divdivap2  8832  div2subap  8945  letrp1  8956  ltmulgt12  8973  lediv1  8977  ltdiv2  8995  lediv2  8999  lbinfle  9058  difgtsumgt  9477  xrletr  9965  xrre2  9978  xaddass  10026  ixxdisj  10060  ubioc1  10086  lbico1  10087  elioo5  10090  iccsupr  10123  lbicc2  10141  ubicc2  10142  iccneg  10146  icoshft  10147  icodisj  10149  iccf1o  10161  iccen  10163  zltaddlt1le  10164  fztri3or  10196  fzdcel  10197  fzen  10200  uzsubsubfz  10204  fzrevral2  10263  fzshftral  10265  fz0fzdiffz0  10287  difelfznle  10292  fzo1fzo0n0  10344  fzonmapblen  10348  fzosubel2  10361  ubmelfzo  10366  elfzodifsumelfzo  10367  ssfzo12bi  10391  ubmelm1fzo  10392  subfzo0  10408  ceiqle  10495  modqid2  10533  zmodidfzoimp  10536  addmodidr  10555  modfzo0difsn  10577  addmodlteq  10580  frec2uzf1od  10588  exprecap  10762  expdivap  10772  expubnd  10778  sqdivap  10785  mulbinom2  10838  bernneq2  10843  mulsubdivbinom2ap  10893  bcval3  10933  bccmpl  10936  omgadd  10984  ccatval1  11091  ccatval2  11092  ccatass  11102  lswccatn0lsw  11105  ccatws1lenp1bg  11127  pfxfv  11175  pfxnd  11180  pfxtrcfv  11184  pfxsuffeqwrdeq  11189  swrdswrd  11196  pfxpfx  11199  ccatopth2  11208  pfxccatin12lem4  11217  pfxccatin12lem1  11219  pfxccatin12lem2  11222  pfxccatin12lem3  11223  pfxccatin12  11224  pfxccat3  11225  swrdccat  11226  pfxccatpfx1  11227  pfxccatpfx2  11228  shftval2  11252  mulreap  11290  elicc4abs  11520  abssubge0  11528  abssuble0  11529  maxleast  11639  maxltsup  11644  xrmaxltsup  11684  xrmineqinf  11695  xrltmininf  11696  xrlemininf  11697  fsumdifsnconst  11881  prodfap0  11971  prodfrecap  11972  fprodabs  12042  sin01gt0  12188  cos01gt0  12189  sin02gt0  12190  dvdscmul  12244  summodnegmod  12248  modmulconst  12249  dvdsleabs  12271  dvdsleabs2  12272  addmodlteqALT  12285  dvdsexp  12287  mulmoddvds  12289  divalgb  12351  divgcdz  12407  gcdass  12451  mulgcdr  12454  gcddiv  12455  uzwodc  12473  lcmass  12522  coprmdvds  12529  qredeq  12533  qredeu  12534  congr  12537  divgcdcoprm0  12538  divgcdcoprmex  12539  cncongr1  12540  cncongr2  12541  isprm3  12555  dvdsnprmd  12562  euclemma  12583  prmdvdsexpb  12586  prmexpb  12588  rpexp  12590  znege1  12615  modprminv  12687  modprminveq  12688  vfermltl  12689  modprm0  12692  modprmn0modprm0  12694  coprimeprodsq  12695  coprimeprodsq2  12696  pythagtriplem1  12703  pythagtriplem3  12705  pythagtriplem6  12708  pythagtriplem12  12713  pythagtriplem13  12714  pythagtriplem14  12715  pythagtriplem16  12717  pythagtriplem19  12720  pythagtrip  12721  pcmul  12739  pcdiv  12740  pcqcl  12744  pcgcd1  12766  pcgcd  12767  dvdsprmpweq  12773  difsqpwdvds  12776  pcfaclem  12787  unbendc  12940  strle3g  13055  ercpbl  13278  grpinvid1  13499  grpinvid2  13500  grpasscan1  13510  grpasscan2  13511  grpidrcan  13512  grpidlcan  13513  grpinvadd  13525  grpsubadd  13535  grppncan  13538  pwsinvg  13559  qussub  13688  subcmnd  13784  mulgass2  13935  dvrcan1  14017  dvrcan3  14018  rmodislmodlem  14227  rmodislmod  14228  islssm  14234  lsselg  14238  lspss  14276  lspssp  14280  lsslsp  14306  islidlm  14356  lidlnegcl  14362  lidlsubcl  14364  zndvds  14526  basgen  14667  clsss  14705  ntrin  14711  ntrcls0  14718  neiint  14732  neiss  14737  neipsm  14741  opnssneib  14743  innei  14750  restco  14761  iscnp  14786  cnconst2  14820  txcn  14862  psmetsym  14916  psmetlecl  14921  distspace  14922  xmetlecl  14954  xmetsym  14955  xblcntrps  15000  xblcntr  15001  blssec  15025  blpnfctr  15026  txmetcn  15106  cnmet  15117  dvid  15282  dvidre  15284  dvply1  15352  ptolemy  15411  sinq12gt0  15417  sincosq1eq  15426  rpcxpsub  15495  relogbexpap  15545  logbleb  15548  logblt  15549  rplogbcxp  15550  lgsval4  15612  lgsmod  15618  lgsne0  15630  lgsmulsqcoprm  15638  2lgsoddprmlem1  15697  structiedg0val  15754  lpvtx  15790  upgredg2vtx  15852  upgredgpr  15853