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  2811  eqeu  2931  tpssi  3786  issod  4351  sotricim  4355  soinxp  4730  funopg  5289  fnco  5363  resasplitss  5434  resdif  5523  fnimapr  5618  ftpg  5743  fsnunfv  5760  fvpr1g  5765  fvpr2g  5766  f1ocnvfvb  5824  f1oiso2  5871  moriotass  5903  f1ofveu  5907  acexmid  5918  ovig  6041  ov6g  6058  ovg  6059  ot1stg  6207  ot2ndg  6208  poxp  6287  brtposg  6309  smores3  6348  smoiso  6357  rdgivallem  6436  frecsuclem  6461  nnaord  6564  nnaword  6566  nnawordex  6584  ecopovtrn  6688  ecopovtrng  6691  xpdom3m  6890  mapxpen  6906  sbthlemi4  7021  djuenun  7274  netap  7316  2omotaplemap  7319  ltsopi  7382  addcanpig  7396  distrnqg  7449  ltsonq  7460  ltanqg  7462  ltmnqg  7463  nnanq0  7520  distrnq0  7521  distnq0r  7525  prarloclem  7563  genpassl  7586  genpassu  7587  distrlem1prl  7644  distrlem1pru  7645  distrlem5prl  7648  distrlem5pru  7649  1idprl  7652  1idpru  7653  ltpopr  7657  ltsopr  7658  ltexprlemm  7662  ltexprlemfl  7671  ltexprlemfu  7673  addcanprlemu  7677  recexprlem1ssl  7695  recexprlem1ssu  7696  aptipr  7703  lttrsr  7824  ltsosr  7826  ltasrg  7832  recexgt0sr  7835  mulextsr1  7843  axmulass  7935  ltxrlt  8087  axltwlin  8089  axlttrn  8090  axltadd  8091  letr  8104  mul12  8150  add12  8179  subadd  8224  addsub  8232  npncan  8242  nppcan  8243  nnpcan  8244  nppcan3  8245  pnpcan  8260  pnncan  8262  ppncan  8263  subdi  8406  ltaddsub2  8458  leaddsub2  8460  ltaddsublt  8592  apreap  8608  lemul1  8614  reapmul1lem  8615  reapadd1  8617  reapcotr  8619  receuap  8690  divassap  8711  div23ap  8712  divmulassap  8716  divmulasscomap  8717  divcanap4  8720  divsubdirap  8729  divcanap5  8735  divdiv32ap  8741  divdivap2  8745  div2subap  8858  letrp1  8869  ltmulgt12  8886  lediv1  8890  ltdiv2  8908  lediv2  8912  lbinfle  8971  difgtsumgt  9389  xrletr  9877  xrre2  9890  xaddass  9938  ixxdisj  9972  ubioc1  9998  lbico1  9999  elioo5  10002  iccsupr  10035  lbicc2  10053  ubicc2  10054  iccneg  10058  icoshft  10059  icodisj  10061  iccf1o  10073  iccen  10075  zltaddlt1le  10076  fztri3or  10108  fzdcel  10109  fzen  10112  uzsubsubfz  10116  fzrevral2  10175  fzshftral  10177  fz0fzdiffz0  10199  difelfznle  10204  fzo1fzo0n0  10253  fzonmapblen  10257  fzosubel2  10265  ubmelfzo  10270  elfzodifsumelfzo  10271  ssfzo12bi  10295  ubmelm1fzo  10296  subfzo0  10312  ceiqle  10387  modqid2  10425  zmodidfzoimp  10428  addmodidr  10447  modfzo0difsn  10469  addmodlteq  10472  frec2uzf1od  10480  exprecap  10654  expdivap  10664  expubnd  10670  sqdivap  10677  mulbinom2  10730  bernneq2  10735  mulsubdivbinom2ap  10785  bcval3  10825  bccmpl  10828  omgadd  10876  shftval2  10973  mulreap  11011  elicc4abs  11241  abssubge0  11249  abssuble0  11250  maxleast  11360  maxltsup  11365  xrmaxltsup  11404  xrmineqinf  11415  xrltmininf  11416  xrlemininf  11417  fsumdifsnconst  11601  prodfap0  11691  prodfrecap  11692  fprodabs  11762  sin01gt0  11908  cos01gt0  11909  sin02gt0  11910  dvdscmul  11964  summodnegmod  11968  modmulconst  11969  dvdsleabs  11990  dvdsleabs2  11991  addmodlteqALT  12004  dvdsexp  12006  mulmoddvds  12008  divalgb  12069  divgcdz  12111  gcdass  12155  mulgcdr  12158  gcddiv  12159  uzwodc  12177  lcmass  12226  coprmdvds  12233  qredeq  12237  qredeu  12238  congr  12241  divgcdcoprm0  12242  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  isprm3  12259  dvdsnprmd  12266  euclemma  12287  prmdvdsexpb  12290  prmexpb  12292  rpexp  12294  znege1  12319  modprminv  12390  modprminveq  12391  vfermltl  12392  modprm0  12395  modprmn0modprm0  12397  coprimeprodsq  12398  coprimeprodsq2  12399  pythagtriplem1  12406  pythagtriplem3  12408  pythagtriplem6  12411  pythagtriplem12  12416  pythagtriplem13  12417  pythagtriplem14  12418  pythagtriplem16  12420  pythagtriplem19  12423  pythagtrip  12424  pcmul  12442  pcdiv  12443  pcqcl  12447  pcgcd1  12469  pcgcd  12470  dvdsprmpweq  12476  difsqpwdvds  12479  pcfaclem  12490  unbendc  12614  strle3g  12729  ercpbl  12917  grpinvid1  13127  grpinvid2  13128  grpasscan1  13138  grpasscan2  13139  grpidrcan  13140  grpidlcan  13141  grpinvadd  13153  grpsubadd  13163  grppncan  13166  qussub  13310  subcmnd  13406  mulgass2  13557  dvrcan1  13639  dvrcan3  13640  rmodislmodlem  13849  rmodislmod  13850  islssm  13856  lsselg  13860  lspss  13898  lspssp  13902  lsslsp  13928  islidlm  13978  lidlnegcl  13984  lidlsubcl  13986  zndvds  14148  basgen  14259  clsss  14297  ntrin  14303  ntrcls0  14310  neiint  14324  neiss  14329  neipsm  14333  opnssneib  14335  innei  14342  restco  14353  iscnp  14378  cnconst2  14412  txcn  14454  psmetsym  14508  psmetlecl  14513  distspace  14514  xmetlecl  14546  xmetsym  14547  xblcntrps  14592  xblcntr  14593  blssec  14617  blpnfctr  14618  txmetcn  14698  cnmet  14709  dvid  14874  dvidre  14876  dvply1  14943  ptolemy  15000  sinq12gt0  15006  sincosq1eq  15015  rpcxpsub  15084  relogbexpap  15131  logbleb  15134  logblt  15135  rplogbcxp  15136  lgsval4  15177  lgsmod  15183  lgsne0  15195  lgsmulsqcoprm  15203  2lgsoddprmlem1  15262