Theorem 3adant3 1043

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 1020	. 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 1004

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 1006

This theorem is referenced by:  stoic4a  1476  stoic4b  1477  vtoclgft  2854  eqeu  2976  ssprsseq  3835  tpssi  3842  issod  4416  sotricim  4420  soinxp  4796  funopg  5360  fnco  5440  resasplitss  5516  resdif  5605  fnimapr  5706  ftpg  5838  fsnunfv  5855  fvpr1g  5860  fvpr2g  5861  f1ocnvfvb  5921  f1oiso2  5968  moriotass  6002  f1ofveu  6006  acexmid  6017  ovig  6143  ov6g  6160  ovg  6161  ot1stg  6315  ot2ndg  6316  poxp  6397  brtposg  6420  smores3  6459  smoiso  6468  rdgivallem  6547  frecsuclem  6572  nnaord  6677  nnaword  6679  nnawordex  6697  ecopovtrn  6801  ecopovtrng  6804  xpdom3m  7018  mapxpen  7034  sbthlemi4  7159  djuenun  7427  netap  7473  2omotaplemap  7476  ltsopi  7540  addcanpig  7554  distrnqg  7607  ltsonq  7618  ltanqg  7620  ltmnqg  7621  nnanq0  7678  distrnq0  7679  distnq0r  7683  prarloclem  7721  genpassl  7744  genpassu  7745  distrlem1prl  7802  distrlem1pru  7803  distrlem5prl  7806  distrlem5pru  7807  1idprl  7810  1idpru  7811  ltpopr  7815  ltsopr  7816  ltexprlemm  7820  ltexprlemfl  7829  ltexprlemfu  7831  addcanprlemu  7835  recexprlem1ssl  7853  recexprlem1ssu  7854  aptipr  7861  lttrsr  7982  ltsosr  7984  ltasrg  7990  recexgt0sr  7993  mulextsr1  8001  axmulass  8093  ltxrlt  8245  axltwlin  8247  axlttrn  8248  axltadd  8249  letr  8262  mul12  8308  add12  8337  subadd  8382  addsub  8390  npncan  8400  nppcan  8401  nnpcan  8402  nppcan3  8403  pnpcan  8418  pnncan  8420  ppncan  8421  subdi  8564  ltaddsub2  8617  leaddsub2  8619  ltaddsublt  8751  apreap  8767  lemul1  8773  reapmul1lem  8774  reapadd1  8776  reapcotr  8778  receuap  8849  divassap  8870  div23ap  8871  divmulassap  8875  divmulasscomap  8876  divcanap4  8879  divsubdirap  8888  divcanap5  8894  divdiv32ap  8900  divdivap2  8904  div2subap  9017  letrp1  9028  ltmulgt12  9045  lediv1  9049  ltdiv2  9067  lediv2  9071  lbinfle  9130  difgtsumgt  9549  xrletr  10043  xrre2  10056  xaddass  10104  ixxdisj  10138  ubioc1  10164  lbico1  10165  elioo5  10168  iccsupr  10201  lbicc2  10219  ubicc2  10220  iccneg  10224  icoshft  10225  icodisj  10227  iccf1o  10239  iccen  10241  zltaddlt1le  10242  fztri3or  10274  fzdcel  10275  fzen  10278  uzsubsubfz  10282  fzrevral2  10341  fzshftral  10343  fz0fzdiffz0  10365  difelfznle  10370  fzo1fzo0n0  10423  fzonmapblen  10427  fzosubel2  10441  ubmelfzo  10446  elfzodifsumelfzo  10447  ssfzo12bi  10471  ubmelm1fzo  10472  subfzo0  10489  ceiqle  10576  modqid2  10614  zmodidfzoimp  10617  addmodidr  10636  modfzo0difsn  10658  addmodlteq  10661  frec2uzf1od  10669  exprecap  10843  expdivap  10853  expubnd  10859  sqdivap  10866  mulbinom2  10919  bernneq2  10924  mulsubdivbinom2ap  10974  bcval3  11014  bccmpl  11017  omgadd  11066  ccatval1  11178  ccatval2  11179  ccatass  11189  lswccatn0lsw  11192  ccatws1lenp1bg  11216  ccatw2s1leng  11219  pfxfv  11269  pfxnd  11274  pfxtrcfv  11278  pfxsuffeqwrdeq  11283  swrdswrd  11290  pfxpfx  11293  ccatopth2  11302  pfxccatin12lem4  11311  pfxccatin12lem1  11313  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  pfxccatpfx1  11321  pfxccatpfx2  11322  s3fv0g  11376  s3fv1g  11377  s3fv2g  11378  shftval2  11404  mulreap  11442  elicc4abs  11672  abssubge0  11680  abssuble0  11681  maxleast  11791  maxltsup  11796  xrmaxltsup  11836  xrmineqinf  11847  xrltmininf  11848  xrlemininf  11849  fsumdifsnconst  12034  prodfap0  12124  prodfrecap  12125  fprodabs  12195  sin01gt0  12341  cos01gt0  12342  sin02gt0  12343  dvdscmul  12397  summodnegmod  12401  modmulconst  12402  dvdsleabs  12424  dvdsleabs2  12425  addmodlteqALT  12438  dvdsexp  12440  mulmoddvds  12442  divalgb  12504  divgcdz  12560  gcdass  12604  mulgcdr  12607  gcddiv  12608  uzwodc  12626  lcmass  12675  coprmdvds  12682  qredeq  12686  qredeu  12687  congr  12690  divgcdcoprm0  12691  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  isprm3  12708  dvdsnprmd  12715  euclemma  12736  prmdvdsexpb  12739  prmexpb  12741  rpexp  12743  znege1  12768  modprminv  12840  modprminveq  12841  vfermltl  12842  modprm0  12845  modprmn0modprm0  12847  coprimeprodsq  12848  coprimeprodsq2  12849  pythagtriplem1  12856  pythagtriplem3  12858  pythagtriplem6  12861  pythagtriplem12  12866  pythagtriplem13  12867  pythagtriplem14  12868  pythagtriplem16  12870  pythagtriplem19  12873  pythagtrip  12874  pcmul  12892  pcdiv  12893  pcqcl  12897  pcgcd1  12919  pcgcd  12920  dvdsprmpweq  12926  difsqpwdvds  12929  pcfaclem  12940  unbendc  13093  strle3g  13209  ercpbl  13432  grpinvid1  13653  grpinvid2  13654  grpasscan1  13664  grpasscan2  13665  grpidrcan  13666  grpidlcan  13667  grpinvadd  13679  grpsubadd  13689  grppncan  13692  pwsinvg  13713  qussub  13842  subcmnd  13938  mulgass2  14090  dvrcan1  14173  dvrcan3  14174  rmodislmodlem  14383  rmodislmod  14384  islssm  14390  lsselg  14394  lspss  14432  lspssp  14436  lsslsp  14462  islidlm  14512  lidlnegcl  14518  lidlsubcl  14520  zndvds  14682  basgen  14823  clsss  14861  ntrin  14867  ntrcls0  14874  neiint  14888  neiss  14893  neipsm  14897  opnssneib  14899  innei  14906  restco  14917  iscnp  14942  cnconst2  14976  txcn  15018  psmetsym  15072  psmetlecl  15077  distspace  15078  xmetlecl  15110  xmetsym  15111  xblcntrps  15156  xblcntr  15157  blssec  15181  blpnfctr  15182  txmetcn  15262  cnmet  15273  dvid  15438  dvidre  15440  dvply1  15508  ptolemy  15567  sinq12gt0  15573  sincosq1eq  15582  rpcxpsub  15651  relogbexpap  15701  logbleb  15704  logblt  15705  rplogbcxp  15706  lgsval4  15768  lgsmod  15774  lgsne0  15786  lgsmulsqcoprm  15794  2lgsoddprmlem1  15853  structiedg0val  15910  lpvtx  15949  upgredg2vtx  16018  upgredgpr  16019  ushgredgedg  16096  ushgredgedgloop  16098  usgr2v1e2w  16116  wlkeq  16224  clwwlkccatlem  16270  clwwlkccat  16271  clwwlkext2edg  16292  clwwlknccat  16293  s2elclwwlknon2  16306  clwwlknonex2lem2  16308