Theorem 3adant3 1019

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

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 982

This theorem is referenced by:  stoic4a  1443  stoic4b  1444  vtoclgft  2810  eqeu  2930  tpssi  3785  issod  4350  sotricim  4354  soinxp  4729  funopg  5288  fnco  5362  resasplitss  5433  resdif  5522  fnimapr  5617  ftpg  5742  fsnunfv  5759  fvpr1g  5764  fvpr2g  5765  f1ocnvfvb  5823  f1oiso2  5870  moriotass  5902  f1ofveu  5906  acexmid  5917  ovig  6040  ov6g  6056  ovg  6057  ot1stg  6205  ot2ndg  6206  poxp  6285  brtposg  6307  smores3  6346  smoiso  6355  rdgivallem  6434  frecsuclem  6459  nnaord  6562  nnaword  6564  nnawordex  6582  ecopovtrn  6686  ecopovtrng  6689  xpdom3m  6888  mapxpen  6904  sbthlemi4  7019  djuenun  7272  netap  7314  2omotaplemap  7317  ltsopi  7380  addcanpig  7394  distrnqg  7447  ltsonq  7458  ltanqg  7460  ltmnqg  7461  nnanq0  7518  distrnq0  7519  distnq0r  7523  prarloclem  7561  genpassl  7584  genpassu  7585  distrlem1prl  7642  distrlem1pru  7643  distrlem5prl  7646  distrlem5pru  7647  1idprl  7650  1idpru  7651  ltpopr  7655  ltsopr  7656  ltexprlemm  7660  ltexprlemfl  7669  ltexprlemfu  7671  addcanprlemu  7675  recexprlem1ssl  7693  recexprlem1ssu  7694  aptipr  7701  lttrsr  7822  ltsosr  7824  ltasrg  7830  recexgt0sr  7833  mulextsr1  7841  axmulass  7933  ltxrlt  8085  axltwlin  8087  axlttrn  8088  axltadd  8089  letr  8102  mul12  8148  add12  8177  subadd  8222  addsub  8230  npncan  8240  nppcan  8241  nnpcan  8242  nppcan3  8243  pnpcan  8258  pnncan  8260  ppncan  8261  subdi  8404  ltaddsub2  8456  leaddsub2  8458  ltaddsublt  8590  apreap  8606  lemul1  8612  reapmul1lem  8613  reapadd1  8615  reapcotr  8617  receuap  8688  divassap  8709  div23ap  8710  divmulassap  8714  divmulasscomap  8715  divcanap4  8718  divsubdirap  8727  divcanap5  8733  divdiv32ap  8739  divdivap2  8743  div2subap  8856  letrp1  8867  ltmulgt12  8884  lediv1  8888  ltdiv2  8906  lediv2  8910  lbinfle  8969  difgtsumgt  9386  xrletr  9874  xrre2  9887  xaddass  9935  ixxdisj  9969  ubioc1  9995  lbico1  9996  elioo5  9999  iccsupr  10032  lbicc2  10050  ubicc2  10051  iccneg  10055  icoshft  10056  icodisj  10058  iccf1o  10070  iccen  10072  zltaddlt1le  10073  fztri3or  10105  fzdcel  10106  fzen  10109  uzsubsubfz  10113  fzrevral2  10172  fzshftral  10174  fz0fzdiffz0  10196  difelfznle  10201  fzo1fzo0n0  10250  fzonmapblen  10254  fzosubel2  10262  ubmelfzo  10267  elfzodifsumelfzo  10268  ssfzo12bi  10292  ubmelm1fzo  10293  subfzo0  10309  ceiqle  10384  modqid2  10422  zmodidfzoimp  10425  addmodidr  10444  modfzo0difsn  10466  addmodlteq  10469  frec2uzf1od  10477  exprecap  10651  expdivap  10661  expubnd  10667  sqdivap  10674  mulbinom2  10727  bernneq2  10732  mulsubdivbinom2ap  10782  bcval3  10822  bccmpl  10825  omgadd  10873  shftval2  10970  mulreap  11008  elicc4abs  11238  abssubge0  11246  abssuble0  11247  maxleast  11357  maxltsup  11362  xrmaxltsup  11401  xrmineqinf  11412  xrltmininf  11413  xrlemininf  11414  fsumdifsnconst  11598  prodfap0  11688  prodfrecap  11689  fprodabs  11759  sin01gt0  11905  cos01gt0  11906  sin02gt0  11907  dvdscmul  11961  summodnegmod  11965  modmulconst  11966  dvdsleabs  11987  dvdsleabs2  11988  addmodlteqALT  12001  dvdsexp  12003  mulmoddvds  12005  divalgb  12066  divgcdz  12108  gcdass  12152  mulgcdr  12155  gcddiv  12156  uzwodc  12174  lcmass  12223  coprmdvds  12230  qredeq  12234  qredeu  12235  congr  12238  divgcdcoprm0  12239  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  isprm3  12256  dvdsnprmd  12263  euclemma  12284  prmdvdsexpb  12287  prmexpb  12289  rpexp  12291  znege1  12316  modprminv  12387  modprminveq  12388  vfermltl  12389  modprm0  12392  modprmn0modprm0  12394  coprimeprodsq  12395  coprimeprodsq2  12396  pythagtriplem1  12403  pythagtriplem3  12405  pythagtriplem6  12408  pythagtriplem12  12413  pythagtriplem13  12414  pythagtriplem14  12415  pythagtriplem16  12417  pythagtriplem19  12420  pythagtrip  12421  pcmul  12439  pcdiv  12440  pcqcl  12444  pcgcd1  12466  pcgcd  12467  dvdsprmpweq  12473  difsqpwdvds  12476  pcfaclem  12487  unbendc  12611  strle3g  12726  ercpbl  12914  grpinvid1  13124  grpinvid2  13125  grpasscan1  13135  grpasscan2  13136  grpidrcan  13137  grpidlcan  13138  grpinvadd  13150  grpsubadd  13160  grppncan  13163  qussub  13307  subcmnd  13403  mulgass2  13554  dvrcan1  13636  dvrcan3  13637  rmodislmodlem  13846  rmodislmod  13847  islssm  13853  lsselg  13857  lspss  13895  lspssp  13899  lsslsp  13925  islidlm  13975  lidlnegcl  13981  lidlsubcl  13983  zndvds  14137  basgen  14248  clsss  14286  ntrin  14292  ntrcls0  14299  neiint  14313  neiss  14318  neipsm  14322  opnssneib  14324  innei  14331  restco  14342  iscnp  14367  cnconst2  14401  txcn  14443  psmetsym  14497  psmetlecl  14502  distspace  14503  xmetlecl  14535  xmetsym  14536  xblcntrps  14581  xblcntr  14582  blssec  14606  blpnfctr  14607  txmetcn  14687  cnmet  14698  dvid  14847  ptolemy  14959  sinq12gt0  14965  sincosq1eq  14974  rpcxpsub  15043  relogbexpap  15090  logbleb  15093  logblt  15094  rplogbcxp  15095  lgsval4  15136  lgsmod  15142  lgsne0  15154  lgsmulsqcoprm  15162  2lgsoddprmlem1  15193