Theorem 3adant3 1041

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 1018	. 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 1002

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 1004

This theorem is referenced by:  stoic4a  1474  stoic4b  1475  vtoclgft  2851  eqeu  2973  ssprsseq  3830  tpssi  3837  issod  4410  sotricim  4414  soinxp  4789  funopg  5352  fnco  5431  resasplitss  5505  resdif  5594  fnimapr  5694  ftpg  5823  fsnunfv  5840  fvpr1g  5845  fvpr2g  5846  f1ocnvfvb  5904  f1oiso2  5951  moriotass  5985  f1ofveu  5989  acexmid  6000  ovig  6126  ov6g  6143  ovg  6144  ot1stg  6298  ot2ndg  6299  poxp  6378  brtposg  6400  smores3  6439  smoiso  6448  rdgivallem  6527  frecsuclem  6552  nnaord  6655  nnaword  6657  nnawordex  6675  ecopovtrn  6779  ecopovtrng  6782  xpdom3m  6993  mapxpen  7009  sbthlemi4  7127  djuenun  7394  netap  7440  2omotaplemap  7443  ltsopi  7507  addcanpig  7521  distrnqg  7574  ltsonq  7585  ltanqg  7587  ltmnqg  7588  nnanq0  7645  distrnq0  7646  distnq0r  7650  prarloclem  7688  genpassl  7711  genpassu  7712  distrlem1prl  7769  distrlem1pru  7770  distrlem5prl  7773  distrlem5pru  7774  1idprl  7777  1idpru  7778  ltpopr  7782  ltsopr  7783  ltexprlemm  7787  ltexprlemfl  7796  ltexprlemfu  7798  addcanprlemu  7802  recexprlem1ssl  7820  recexprlem1ssu  7821  aptipr  7828  lttrsr  7949  ltsosr  7951  ltasrg  7957  recexgt0sr  7960  mulextsr1  7968  axmulass  8060  ltxrlt  8212  axltwlin  8214  axlttrn  8215  axltadd  8216  letr  8229  mul12  8275  add12  8304  subadd  8349  addsub  8357  npncan  8367  nppcan  8368  nnpcan  8369  nppcan3  8370  pnpcan  8385  pnncan  8387  ppncan  8388  subdi  8531  ltaddsub2  8584  leaddsub2  8586  ltaddsublt  8718  apreap  8734  lemul1  8740  reapmul1lem  8741  reapadd1  8743  reapcotr  8745  receuap  8816  divassap  8837  div23ap  8838  divmulassap  8842  divmulasscomap  8843  divcanap4  8846  divsubdirap  8855  divcanap5  8861  divdiv32ap  8867  divdivap2  8871  div2subap  8984  letrp1  8995  ltmulgt12  9012  lediv1  9016  ltdiv2  9034  lediv2  9038  lbinfle  9097  difgtsumgt  9516  xrletr  10004  xrre2  10017  xaddass  10065  ixxdisj  10099  ubioc1  10125  lbico1  10126  elioo5  10129  iccsupr  10162  lbicc2  10180  ubicc2  10181  iccneg  10185  icoshft  10186  icodisj  10188  iccf1o  10200  iccen  10202  zltaddlt1le  10203  fztri3or  10235  fzdcel  10236  fzen  10239  uzsubsubfz  10243  fzrevral2  10302  fzshftral  10304  fz0fzdiffz0  10326  difelfznle  10331  fzo1fzo0n0  10383  fzonmapblen  10387  fzosubel2  10401  ubmelfzo  10406  elfzodifsumelfzo  10407  ssfzo12bi  10431  ubmelm1fzo  10432  subfzo0  10448  ceiqle  10535  modqid2  10573  zmodidfzoimp  10576  addmodidr  10595  modfzo0difsn  10617  addmodlteq  10620  frec2uzf1od  10628  exprecap  10802  expdivap  10812  expubnd  10818  sqdivap  10825  mulbinom2  10878  bernneq2  10883  mulsubdivbinom2ap  10933  bcval3  10973  bccmpl  10976  omgadd  11024  ccatval1  11132  ccatval2  11133  ccatass  11143  lswccatn0lsw  11146  ccatws1lenp1bg  11168  pfxfv  11216  pfxnd  11221  pfxtrcfv  11225  pfxsuffeqwrdeq  11230  swrdswrd  11237  pfxpfx  11240  ccatopth2  11249  pfxccatin12lem4  11258  pfxccatin12lem1  11260  pfxccatin12lem2  11263  pfxccatin12lem3  11264  pfxccatin12  11265  pfxccat3  11266  swrdccat  11267  pfxccatpfx1  11268  pfxccatpfx2  11269  s3fv0g  11323  s3fv1g  11324  shftval2  11337  mulreap  11375  elicc4abs  11605  abssubge0  11613  abssuble0  11614  maxleast  11724  maxltsup  11729  xrmaxltsup  11769  xrmineqinf  11780  xrltmininf  11781  xrlemininf  11782  fsumdifsnconst  11966  prodfap0  12056  prodfrecap  12057  fprodabs  12127  sin01gt0  12273  cos01gt0  12274  sin02gt0  12275  dvdscmul  12329  summodnegmod  12333  modmulconst  12334  dvdsleabs  12356  dvdsleabs2  12357  addmodlteqALT  12370  dvdsexp  12372  mulmoddvds  12374  divalgb  12436  divgcdz  12492  gcdass  12536  mulgcdr  12539  gcddiv  12540  uzwodc  12558  lcmass  12607  coprmdvds  12614  qredeq  12618  qredeu  12619  congr  12622  divgcdcoprm0  12623  divgcdcoprmex  12624  cncongr1  12625  cncongr2  12626  isprm3  12640  dvdsnprmd  12647  euclemma  12668  prmdvdsexpb  12671  prmexpb  12673  rpexp  12675  znege1  12700  modprminv  12772  modprminveq  12773  vfermltl  12774  modprm0  12777  modprmn0modprm0  12779  coprimeprodsq  12780  coprimeprodsq2  12781  pythagtriplem1  12788  pythagtriplem3  12790  pythagtriplem6  12793  pythagtriplem12  12798  pythagtriplem13  12799  pythagtriplem14  12800  pythagtriplem16  12802  pythagtriplem19  12805  pythagtrip  12806  pcmul  12824  pcdiv  12825  pcqcl  12829  pcgcd1  12851  pcgcd  12852  dvdsprmpweq  12858  difsqpwdvds  12861  pcfaclem  12872  unbendc  13025  strle3g  13141  ercpbl  13364  grpinvid1  13585  grpinvid2  13586  grpasscan1  13596  grpasscan2  13597  grpidrcan  13598  grpidlcan  13599  grpinvadd  13611  grpsubadd  13621  grppncan  13624  pwsinvg  13645  qussub  13774  subcmnd  13870  mulgass2  14021  dvrcan1  14104  dvrcan3  14105  rmodislmodlem  14314  rmodislmod  14315  islssm  14321  lsselg  14325  lspss  14363  lspssp  14367  lsslsp  14393  islidlm  14443  lidlnegcl  14449  lidlsubcl  14451  zndvds  14613  basgen  14754  clsss  14792  ntrin  14798  ntrcls0  14805  neiint  14819  neiss  14824  neipsm  14828  opnssneib  14830  innei  14837  restco  14848  iscnp  14873  cnconst2  14907  txcn  14949  psmetsym  15003  psmetlecl  15008  distspace  15009  xmetlecl  15041  xmetsym  15042  xblcntrps  15087  xblcntr  15088  blssec  15112  blpnfctr  15113  txmetcn  15193  cnmet  15204  dvid  15369  dvidre  15371  dvply1  15439  ptolemy  15498  sinq12gt0  15504  sincosq1eq  15513  rpcxpsub  15582  relogbexpap  15632  logbleb  15635  logblt  15636  rplogbcxp  15637  lgsval4  15699  lgsmod  15705  lgsne0  15717  lgsmulsqcoprm  15725  2lgsoddprmlem1  15784  structiedg0val  15841  lpvtx  15879  upgredg2vtx  15946  upgredgpr  15947  ushgredgedg  16024  ushgredgedgloop  16026  wlkeq  16065