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  2825  eqeu  2947  tpssi  3806  issod  4374  sotricim  4378  soinxp  4753  funopg  5314  fnco  5393  resasplitss  5467  resdif  5556  fnimapr  5652  ftpg  5781  fsnunfv  5798  fvpr1g  5803  fvpr2g  5804  f1ocnvfvb  5862  f1oiso2  5909  moriotass  5941  f1ofveu  5945  acexmid  5956  ovig  6080  ov6g  6097  ovg  6098  ot1stg  6251  ot2ndg  6252  poxp  6331  brtposg  6353  smores3  6392  smoiso  6401  rdgivallem  6480  frecsuclem  6505  nnaord  6608  nnaword  6610  nnawordex  6628  ecopovtrn  6732  ecopovtrng  6735  xpdom3m  6944  mapxpen  6960  sbthlemi4  7077  djuenun  7340  netap  7386  2omotaplemap  7389  ltsopi  7453  addcanpig  7467  distrnqg  7520  ltsonq  7531  ltanqg  7533  ltmnqg  7534  nnanq0  7591  distrnq0  7592  distnq0r  7596  prarloclem  7634  genpassl  7657  genpassu  7658  distrlem1prl  7715  distrlem1pru  7716  distrlem5prl  7719  distrlem5pru  7720  1idprl  7723  1idpru  7724  ltpopr  7728  ltsopr  7729  ltexprlemm  7733  ltexprlemfl  7742  ltexprlemfu  7744  addcanprlemu  7748  recexprlem1ssl  7766  recexprlem1ssu  7767  aptipr  7774  lttrsr  7895  ltsosr  7897  ltasrg  7903  recexgt0sr  7906  mulextsr1  7914  axmulass  8006  ltxrlt  8158  axltwlin  8160  axlttrn  8161  axltadd  8162  letr  8175  mul12  8221  add12  8250  subadd  8295  addsub  8303  npncan  8313  nppcan  8314  nnpcan  8315  nppcan3  8316  pnpcan  8331  pnncan  8333  ppncan  8334  subdi  8477  ltaddsub2  8530  leaddsub2  8532  ltaddsublt  8664  apreap  8680  lemul1  8686  reapmul1lem  8687  reapadd1  8689  reapcotr  8691  receuap  8762  divassap  8783  div23ap  8784  divmulassap  8788  divmulasscomap  8789  divcanap4  8792  divsubdirap  8801  divcanap5  8807  divdiv32ap  8813  divdivap2  8817  div2subap  8930  letrp1  8941  ltmulgt12  8958  lediv1  8962  ltdiv2  8980  lediv2  8984  lbinfle  9043  difgtsumgt  9462  xrletr  9950  xrre2  9963  xaddass  10011  ixxdisj  10045  ubioc1  10071  lbico1  10072  elioo5  10075  iccsupr  10108  lbicc2  10126  ubicc2  10127  iccneg  10131  icoshft  10132  icodisj  10134  iccf1o  10146  iccen  10148  zltaddlt1le  10149  fztri3or  10181  fzdcel  10182  fzen  10185  uzsubsubfz  10189  fzrevral2  10248  fzshftral  10250  fz0fzdiffz0  10272  difelfznle  10277  fzo1fzo0n0  10329  fzonmapblen  10333  fzosubel2  10346  ubmelfzo  10351  elfzodifsumelfzo  10352  ssfzo12bi  10376  ubmelm1fzo  10377  subfzo0  10393  ceiqle  10480  modqid2  10518  zmodidfzoimp  10521  addmodidr  10540  modfzo0difsn  10562  addmodlteq  10565  frec2uzf1od  10573  exprecap  10747  expdivap  10757  expubnd  10763  sqdivap  10770  mulbinom2  10823  bernneq2  10828  mulsubdivbinom2ap  10878  bcval3  10918  bccmpl  10921  omgadd  10969  ccatval1  11076  ccatval2  11077  ccatass  11087  lswccatn0lsw  11090  ccatws1lenp1bg  11112  pfxfv  11160  pfxnd  11165  pfxtrcfv  11169  pfxsuffeqwrdeq  11174  swrdswrd  11181  pfxpfx  11184  ccatopth2  11193  shftval2  11212  mulreap  11250  elicc4abs  11480  abssubge0  11488  abssuble0  11489  maxleast  11599  maxltsup  11604  xrmaxltsup  11644  xrmineqinf  11655  xrltmininf  11656  xrlemininf  11657  fsumdifsnconst  11841  prodfap0  11931  prodfrecap  11932  fprodabs  12002  sin01gt0  12148  cos01gt0  12149  sin02gt0  12150  dvdscmul  12204  summodnegmod  12208  modmulconst  12209  dvdsleabs  12231  dvdsleabs2  12232  addmodlteqALT  12245  dvdsexp  12247  mulmoddvds  12249  divalgb  12311  divgcdz  12367  gcdass  12411  mulgcdr  12414  gcddiv  12415  uzwodc  12433  lcmass  12482  coprmdvds  12489  qredeq  12493  qredeu  12494  congr  12497  divgcdcoprm0  12498  divgcdcoprmex  12499  cncongr1  12500  cncongr2  12501  isprm3  12515  dvdsnprmd  12522  euclemma  12543  prmdvdsexpb  12546  prmexpb  12548  rpexp  12550  znege1  12575  modprminv  12647  modprminveq  12648  vfermltl  12649  modprm0  12652  modprmn0modprm0  12654  coprimeprodsq  12655  coprimeprodsq2  12656  pythagtriplem1  12663  pythagtriplem3  12665  pythagtriplem6  12668  pythagtriplem12  12673  pythagtriplem13  12674  pythagtriplem14  12675  pythagtriplem16  12677  pythagtriplem19  12680  pythagtrip  12681  pcmul  12699  pcdiv  12700  pcqcl  12704  pcgcd1  12726  pcgcd  12727  dvdsprmpweq  12733  difsqpwdvds  12736  pcfaclem  12747  unbendc  12900  strle3g  13015  ercpbl  13238  grpinvid1  13459  grpinvid2  13460  grpasscan1  13470  grpasscan2  13471  grpidrcan  13472  grpidlcan  13473  grpinvadd  13485  grpsubadd  13495  grppncan  13498  pwsinvg  13519  qussub  13648  subcmnd  13744  mulgass2  13895  dvrcan1  13977  dvrcan3  13978  rmodislmodlem  14187  rmodislmod  14188  islssm  14194  lsselg  14198  lspss  14236  lspssp  14240  lsslsp  14266  islidlm  14316  lidlnegcl  14322  lidlsubcl  14324  zndvds  14486  basgen  14627  clsss  14665  ntrin  14671  ntrcls0  14678  neiint  14692  neiss  14697  neipsm  14701  opnssneib  14703  innei  14710  restco  14721  iscnp  14746  cnconst2  14780  txcn  14822  psmetsym  14876  psmetlecl  14881  distspace  14882  xmetlecl  14914  xmetsym  14915  xblcntrps  14960  xblcntr  14961  blssec  14985  blpnfctr  14986  txmetcn  15066  cnmet  15077  dvid  15242  dvidre  15244  dvply1  15312  ptolemy  15371  sinq12gt0  15377  sincosq1eq  15386  rpcxpsub  15455  relogbexpap  15505  logbleb  15508  logblt  15509  rplogbcxp  15510  lgsval4  15572  lgsmod  15578  lgsne0  15590  lgsmulsqcoprm  15598  2lgsoddprmlem1  15657  structiedg0val  15714  lpvtx  15750