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  5507  resdif  5596  fnimapr  5696  ftpg  5827  fsnunfv  5844  fvpr1g  5849  fvpr2g  5850  f1ocnvfvb  5910  f1oiso2  5957  moriotass  5991  f1ofveu  5995  acexmid  6006  ovig  6132  ov6g  6149  ovg  6150  ot1stg  6304  ot2ndg  6305  poxp  6384  brtposg  6406  smores3  6445  smoiso  6454  rdgivallem  6533  frecsuclem  6558  nnaord  6663  nnaword  6665  nnawordex  6683  ecopovtrn  6787  ecopovtrng  6790  xpdom3m  7001  mapxpen  7017  sbthlemi4  7138  djuenun  7405  netap  7451  2omotaplemap  7454  ltsopi  7518  addcanpig  7532  distrnqg  7585  ltsonq  7596  ltanqg  7598  ltmnqg  7599  nnanq0  7656  distrnq0  7657  distnq0r  7661  prarloclem  7699  genpassl  7722  genpassu  7723  distrlem1prl  7780  distrlem1pru  7781  distrlem5prl  7784  distrlem5pru  7785  1idprl  7788  1idpru  7789  ltpopr  7793  ltsopr  7794  ltexprlemm  7798  ltexprlemfl  7807  ltexprlemfu  7809  addcanprlemu  7813  recexprlem1ssl  7831  recexprlem1ssu  7832  aptipr  7839  lttrsr  7960  ltsosr  7962  ltasrg  7968  recexgt0sr  7971  mulextsr1  7979  axmulass  8071  ltxrlt  8223  axltwlin  8225  axlttrn  8226  axltadd  8227  letr  8240  mul12  8286  add12  8315  subadd  8360  addsub  8368  npncan  8378  nppcan  8379  nnpcan  8380  nppcan3  8381  pnpcan  8396  pnncan  8398  ppncan  8399  subdi  8542  ltaddsub2  8595  leaddsub2  8597  ltaddsublt  8729  apreap  8745  lemul1  8751  reapmul1lem  8752  reapadd1  8754  reapcotr  8756  receuap  8827  divassap  8848  div23ap  8849  divmulassap  8853  divmulasscomap  8854  divcanap4  8857  divsubdirap  8866  divcanap5  8872  divdiv32ap  8878  divdivap2  8882  div2subap  8995  letrp1  9006  ltmulgt12  9023  lediv1  9027  ltdiv2  9045  lediv2  9049  lbinfle  9108  difgtsumgt  9527  xrletr  10016  xrre2  10029  xaddass  10077  ixxdisj  10111  ubioc1  10137  lbico1  10138  elioo5  10141  iccsupr  10174  lbicc2  10192  ubicc2  10193  iccneg  10197  icoshft  10198  icodisj  10200  iccf1o  10212  iccen  10214  zltaddlt1le  10215  fztri3or  10247  fzdcel  10248  fzen  10251  uzsubsubfz  10255  fzrevral2  10314  fzshftral  10316  fz0fzdiffz0  10338  difelfznle  10343  fzo1fzo0n0  10395  fzonmapblen  10399  fzosubel2  10413  ubmelfzo  10418  elfzodifsumelfzo  10419  ssfzo12bi  10443  ubmelm1fzo  10444  subfzo0  10460  ceiqle  10547  modqid2  10585  zmodidfzoimp  10588  addmodidr  10607  modfzo0difsn  10629  addmodlteq  10632  frec2uzf1od  10640  exprecap  10814  expdivap  10824  expubnd  10830  sqdivap  10837  mulbinom2  10890  bernneq2  10895  mulsubdivbinom2ap  10945  bcval3  10985  bccmpl  10988  omgadd  11036  ccatval1  11145  ccatval2  11146  ccatass  11156  lswccatn0lsw  11159  ccatws1lenp1bg  11183  pfxfv  11232  pfxnd  11237  pfxtrcfv  11241  pfxsuffeqwrdeq  11246  swrdswrd  11253  pfxpfx  11256  ccatopth2  11265  pfxccatin12lem4  11274  pfxccatin12lem1  11276  pfxccatin12lem2  11279  pfxccatin12lem3  11280  pfxccatin12  11281  pfxccat3  11282  swrdccat  11283  pfxccatpfx1  11284  pfxccatpfx2  11285  s3fv0g  11339  s3fv1g  11340  shftval2  11353  mulreap  11391  elicc4abs  11621  abssubge0  11629  abssuble0  11630  maxleast  11740  maxltsup  11745  xrmaxltsup  11785  xrmineqinf  11796  xrltmininf  11797  xrlemininf  11798  fsumdifsnconst  11982  prodfap0  12072  prodfrecap  12073  fprodabs  12143  sin01gt0  12289  cos01gt0  12290  sin02gt0  12291  dvdscmul  12345  summodnegmod  12349  modmulconst  12350  dvdsleabs  12372  dvdsleabs2  12373  addmodlteqALT  12386  dvdsexp  12388  mulmoddvds  12390  divalgb  12452  divgcdz  12508  gcdass  12552  mulgcdr  12555  gcddiv  12556  uzwodc  12574  lcmass  12623  coprmdvds  12630  qredeq  12634  qredeu  12635  congr  12638  divgcdcoprm0  12639  divgcdcoprmex  12640  cncongr1  12641  cncongr2  12642  isprm3  12656  dvdsnprmd  12663  euclemma  12684  prmdvdsexpb  12687  prmexpb  12689  rpexp  12691  znege1  12716  modprminv  12788  modprminveq  12789  vfermltl  12790  modprm0  12793  modprmn0modprm0  12795  coprimeprodsq  12796  coprimeprodsq2  12797  pythagtriplem1  12804  pythagtriplem3  12806  pythagtriplem6  12809  pythagtriplem12  12814  pythagtriplem13  12815  pythagtriplem14  12816  pythagtriplem16  12818  pythagtriplem19  12821  pythagtrip  12822  pcmul  12840  pcdiv  12841  pcqcl  12845  pcgcd1  12867  pcgcd  12868  dvdsprmpweq  12874  difsqpwdvds  12877  pcfaclem  12888  unbendc  13041  strle3g  13157  ercpbl  13380  grpinvid1  13601  grpinvid2  13602  grpasscan1  13612  grpasscan2  13613  grpidrcan  13614  grpidlcan  13615  grpinvadd  13627  grpsubadd  13637  grppncan  13640  pwsinvg  13661  qussub  13790  subcmnd  13886  mulgass2  14037  dvrcan1  14120  dvrcan3  14121  rmodislmodlem  14330  rmodislmod  14331  islssm  14337  lsselg  14341  lspss  14379  lspssp  14383  lsslsp  14409  islidlm  14459  lidlnegcl  14465  lidlsubcl  14467  zndvds  14629  basgen  14770  clsss  14808  ntrin  14814  ntrcls0  14821  neiint  14835  neiss  14840  neipsm  14844  opnssneib  14846  innei  14853  restco  14864  iscnp  14889  cnconst2  14923  txcn  14965  psmetsym  15019  psmetlecl  15024  distspace  15025  xmetlecl  15057  xmetsym  15058  xblcntrps  15103  xblcntr  15104  blssec  15128  blpnfctr  15129  txmetcn  15209  cnmet  15220  dvid  15385  dvidre  15387  dvply1  15455  ptolemy  15514  sinq12gt0  15520  sincosq1eq  15529  rpcxpsub  15598  relogbexpap  15648  logbleb  15651  logblt  15652  rplogbcxp  15653  lgsval4  15715  lgsmod  15721  lgsne0  15733  lgsmulsqcoprm  15741  2lgsoddprmlem1  15800  structiedg0val  15857  lpvtx  15895  upgredg2vtx  15962  upgredgpr  15963  ushgredgedg  16040  ushgredgedgloop  16042  wlkeq  16100  clwwlkccatlem  16143  clwwlkccat  16144  clwwlkext2edg  16164  clwwlknccat  16165