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  2814  eqeu  2934  tpssi  3789  issod  4354  sotricim  4358  soinxp  4733  funopg  5292  fnco  5366  resasplitss  5437  resdif  5526  fnimapr  5621  ftpg  5746  fsnunfv  5763  fvpr1g  5768  fvpr2g  5769  f1ocnvfvb  5827  f1oiso2  5874  moriotass  5906  f1ofveu  5910  acexmid  5921  ovig  6044  ov6g  6061  ovg  6062  ot1stg  6210  ot2ndg  6211  poxp  6290  brtposg  6312  smores3  6351  smoiso  6360  rdgivallem  6439  frecsuclem  6464  nnaord  6567  nnaword  6569  nnawordex  6587  ecopovtrn  6691  ecopovtrng  6694  xpdom3m  6893  mapxpen  6909  sbthlemi4  7026  djuenun  7279  netap  7321  2omotaplemap  7324  ltsopi  7387  addcanpig  7401  distrnqg  7454  ltsonq  7465  ltanqg  7467  ltmnqg  7468  nnanq0  7525  distrnq0  7526  distnq0r  7530  prarloclem  7568  genpassl  7591  genpassu  7592  distrlem1prl  7649  distrlem1pru  7650  distrlem5prl  7653  distrlem5pru  7654  1idprl  7657  1idpru  7658  ltpopr  7662  ltsopr  7663  ltexprlemm  7667  ltexprlemfl  7676  ltexprlemfu  7678  addcanprlemu  7682  recexprlem1ssl  7700  recexprlem1ssu  7701  aptipr  7708  lttrsr  7829  ltsosr  7831  ltasrg  7837  recexgt0sr  7840  mulextsr1  7848  axmulass  7940  ltxrlt  8092  axltwlin  8094  axlttrn  8095  axltadd  8096  letr  8109  mul12  8155  add12  8184  subadd  8229  addsub  8237  npncan  8247  nppcan  8248  nnpcan  8249  nppcan3  8250  pnpcan  8265  pnncan  8267  ppncan  8268  subdi  8411  ltaddsub2  8464  leaddsub2  8466  ltaddsublt  8598  apreap  8614  lemul1  8620  reapmul1lem  8621  reapadd1  8623  reapcotr  8625  receuap  8696  divassap  8717  div23ap  8718  divmulassap  8722  divmulasscomap  8723  divcanap4  8726  divsubdirap  8735  divcanap5  8741  divdiv32ap  8747  divdivap2  8751  div2subap  8864  letrp1  8875  ltmulgt12  8892  lediv1  8896  ltdiv2  8914  lediv2  8918  lbinfle  8977  difgtsumgt  9395  xrletr  9883  xrre2  9896  xaddass  9944  ixxdisj  9978  ubioc1  10004  lbico1  10005  elioo5  10008  iccsupr  10041  lbicc2  10059  ubicc2  10060  iccneg  10064  icoshft  10065  icodisj  10067  iccf1o  10079  iccen  10081  zltaddlt1le  10082  fztri3or  10114  fzdcel  10115  fzen  10118  uzsubsubfz  10122  fzrevral2  10181  fzshftral  10183  fz0fzdiffz0  10205  difelfznle  10210  fzo1fzo0n0  10259  fzonmapblen  10263  fzosubel2  10271  ubmelfzo  10276  elfzodifsumelfzo  10277  ssfzo12bi  10301  ubmelm1fzo  10302  subfzo0  10318  ceiqle  10405  modqid2  10443  zmodidfzoimp  10446  addmodidr  10465  modfzo0difsn  10487  addmodlteq  10490  frec2uzf1od  10498  exprecap  10672  expdivap  10682  expubnd  10688  sqdivap  10695  mulbinom2  10748  bernneq2  10753  mulsubdivbinom2ap  10803  bcval3  10843  bccmpl  10846  omgadd  10894  shftval2  10991  mulreap  11029  elicc4abs  11259  abssubge0  11267  abssuble0  11268  maxleast  11378  maxltsup  11383  xrmaxltsup  11423  xrmineqinf  11434  xrltmininf  11435  xrlemininf  11436  fsumdifsnconst  11620  prodfap0  11710  prodfrecap  11711  fprodabs  11781  sin01gt0  11927  cos01gt0  11928  sin02gt0  11929  dvdscmul  11983  summodnegmod  11987  modmulconst  11988  dvdsleabs  12010  dvdsleabs2  12011  addmodlteqALT  12024  dvdsexp  12026  mulmoddvds  12028  divalgb  12090  divgcdz  12138  gcdass  12182  mulgcdr  12185  gcddiv  12186  uzwodc  12204  lcmass  12253  coprmdvds  12260  qredeq  12264  qredeu  12265  congr  12268  divgcdcoprm0  12269  divgcdcoprmex  12270  cncongr1  12271  cncongr2  12272  isprm3  12286  dvdsnprmd  12293  euclemma  12314  prmdvdsexpb  12317  prmexpb  12319  rpexp  12321  znege1  12346  modprminv  12418  modprminveq  12419  vfermltl  12420  modprm0  12423  modprmn0modprm0  12425  coprimeprodsq  12426  coprimeprodsq2  12427  pythagtriplem1  12434  pythagtriplem3  12436  pythagtriplem6  12439  pythagtriplem12  12444  pythagtriplem13  12445  pythagtriplem14  12446  pythagtriplem16  12448  pythagtriplem19  12451  pythagtrip  12452  pcmul  12470  pcdiv  12471  pcqcl  12475  pcgcd1  12497  pcgcd  12498  dvdsprmpweq  12504  difsqpwdvds  12507  pcfaclem  12518  unbendc  12671  strle3g  12786  ercpbl  12974  grpinvid1  13184  grpinvid2  13185  grpasscan1  13195  grpasscan2  13196  grpidrcan  13197  grpidlcan  13198  grpinvadd  13210  grpsubadd  13220  grppncan  13223  qussub  13367  subcmnd  13463  mulgass2  13614  dvrcan1  13696  dvrcan3  13697  rmodislmodlem  13906  rmodislmod  13907  islssm  13913  lsselg  13917  lspss  13955  lspssp  13959  lsslsp  13985  islidlm  14035  lidlnegcl  14041  lidlsubcl  14043  zndvds  14205  basgen  14316  clsss  14354  ntrin  14360  ntrcls0  14367  neiint  14381  neiss  14386  neipsm  14390  opnssneib  14392  innei  14399  restco  14410  iscnp  14435  cnconst2  14469  txcn  14511  psmetsym  14565  psmetlecl  14570  distspace  14571  xmetlecl  14603  xmetsym  14604  xblcntrps  14649  xblcntr  14650  blssec  14674  blpnfctr  14675  txmetcn  14755  cnmet  14766  dvid  14931  dvidre  14933  dvply1  15001  ptolemy  15060  sinq12gt0  15066  sincosq1eq  15075  rpcxpsub  15144  relogbexpap  15194  logbleb  15197  logblt  15198  rplogbcxp  15199  lgsval4  15261  lgsmod  15267  lgsne0  15279  lgsmulsqcoprm  15287  2lgsoddprmlem1  15346