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  3790  issod  4355  sotricim  4359  soinxp  4734  funopg  5293  fnco  5369  resasplitss  5440  resdif  5529  fnimapr  5624  ftpg  5749  fsnunfv  5766  fvpr1g  5771  fvpr2g  5772  f1ocnvfvb  5830  f1oiso2  5877  moriotass  5909  f1ofveu  5913  acexmid  5924  ovig  6048  ov6g  6065  ovg  6066  ot1stg  6219  ot2ndg  6220  poxp  6299  brtposg  6321  smores3  6360  smoiso  6369  rdgivallem  6448  frecsuclem  6473  nnaord  6576  nnaword  6578  nnawordex  6596  ecopovtrn  6700  ecopovtrng  6703  xpdom3m  6902  mapxpen  6918  sbthlemi4  7035  djuenun  7295  netap  7337  2omotaplemap  7340  ltsopi  7404  addcanpig  7418  distrnqg  7471  ltsonq  7482  ltanqg  7484  ltmnqg  7485  nnanq0  7542  distrnq0  7543  distnq0r  7547  prarloclem  7585  genpassl  7608  genpassu  7609  distrlem1prl  7666  distrlem1pru  7667  distrlem5prl  7670  distrlem5pru  7671  1idprl  7674  1idpru  7675  ltpopr  7679  ltsopr  7680  ltexprlemm  7684  ltexprlemfl  7693  ltexprlemfu  7695  addcanprlemu  7699  recexprlem1ssl  7717  recexprlem1ssu  7718  aptipr  7725  lttrsr  7846  ltsosr  7848  ltasrg  7854  recexgt0sr  7857  mulextsr1  7865  axmulass  7957  ltxrlt  8109  axltwlin  8111  axlttrn  8112  axltadd  8113  letr  8126  mul12  8172  add12  8201  subadd  8246  addsub  8254  npncan  8264  nppcan  8265  nnpcan  8266  nppcan3  8267  pnpcan  8282  pnncan  8284  ppncan  8285  subdi  8428  ltaddsub2  8481  leaddsub2  8483  ltaddsublt  8615  apreap  8631  lemul1  8637  reapmul1lem  8638  reapadd1  8640  reapcotr  8642  receuap  8713  divassap  8734  div23ap  8735  divmulassap  8739  divmulasscomap  8740  divcanap4  8743  divsubdirap  8752  divcanap5  8758  divdiv32ap  8764  divdivap2  8768  div2subap  8881  letrp1  8892  ltmulgt12  8909  lediv1  8913  ltdiv2  8931  lediv2  8935  lbinfle  8994  difgtsumgt  9412  xrletr  9900  xrre2  9913  xaddass  9961  ixxdisj  9995  ubioc1  10021  lbico1  10022  elioo5  10025  iccsupr  10058  lbicc2  10076  ubicc2  10077  iccneg  10081  icoshft  10082  icodisj  10084  iccf1o  10096  iccen  10098  zltaddlt1le  10099  fztri3or  10131  fzdcel  10132  fzen  10135  uzsubsubfz  10139  fzrevral2  10198  fzshftral  10200  fz0fzdiffz0  10222  difelfznle  10227  fzo1fzo0n0  10276  fzonmapblen  10280  fzosubel2  10288  ubmelfzo  10293  elfzodifsumelfzo  10294  ssfzo12bi  10318  ubmelm1fzo  10319  subfzo0  10335  ceiqle  10422  modqid2  10460  zmodidfzoimp  10463  addmodidr  10482  modfzo0difsn  10504  addmodlteq  10507  frec2uzf1od  10515  exprecap  10689  expdivap  10699  expubnd  10705  sqdivap  10712  mulbinom2  10765  bernneq2  10770  mulsubdivbinom2ap  10820  bcval3  10860  bccmpl  10863  omgadd  10911  shftval2  11008  mulreap  11046  elicc4abs  11276  abssubge0  11284  abssuble0  11285  maxleast  11395  maxltsup  11400  xrmaxltsup  11440  xrmineqinf  11451  xrltmininf  11452  xrlemininf  11453  fsumdifsnconst  11637  prodfap0  11727  prodfrecap  11728  fprodabs  11798  sin01gt0  11944  cos01gt0  11945  sin02gt0  11946  dvdscmul  12000  summodnegmod  12004  modmulconst  12005  dvdsleabs  12027  dvdsleabs2  12028  addmodlteqALT  12041  dvdsexp  12043  mulmoddvds  12045  divalgb  12107  divgcdz  12163  gcdass  12207  mulgcdr  12210  gcddiv  12211  uzwodc  12229  lcmass  12278  coprmdvds  12285  qredeq  12289  qredeu  12290  congr  12293  divgcdcoprm0  12294  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  isprm3  12311  dvdsnprmd  12318  euclemma  12339  prmdvdsexpb  12342  prmexpb  12344  rpexp  12346  znege1  12371  modprminv  12443  modprminveq  12444  vfermltl  12445  modprm0  12448  modprmn0modprm0  12450  coprimeprodsq  12451  coprimeprodsq2  12452  pythagtriplem1  12459  pythagtriplem3  12461  pythagtriplem6  12464  pythagtriplem12  12469  pythagtriplem13  12470  pythagtriplem14  12471  pythagtriplem16  12473  pythagtriplem19  12476  pythagtrip  12477  pcmul  12495  pcdiv  12496  pcqcl  12500  pcgcd1  12522  pcgcd  12523  dvdsprmpweq  12529  difsqpwdvds  12532  pcfaclem  12543  unbendc  12696  strle3g  12811  ercpbl  13033  grpinvid1  13254  grpinvid2  13255  grpasscan1  13265  grpasscan2  13266  grpidrcan  13267  grpidlcan  13268  grpinvadd  13280  grpsubadd  13290  grppncan  13293  pwsinvg  13314  qussub  13443  subcmnd  13539  mulgass2  13690  dvrcan1  13772  dvrcan3  13773  rmodislmodlem  13982  rmodislmod  13983  islssm  13989  lsselg  13993  lspss  14031  lspssp  14035  lsslsp  14061  islidlm  14111  lidlnegcl  14117  lidlsubcl  14119  zndvds  14281  basgen  14400  clsss  14438  ntrin  14444  ntrcls0  14451  neiint  14465  neiss  14470  neipsm  14474  opnssneib  14476  innei  14483  restco  14494  iscnp  14519  cnconst2  14553  txcn  14595  psmetsym  14649  psmetlecl  14654  distspace  14655  xmetlecl  14687  xmetsym  14688  xblcntrps  14733  xblcntr  14734  blssec  14758  blpnfctr  14759  txmetcn  14839  cnmet  14850  dvid  15015  dvidre  15017  dvply1  15085  ptolemy  15144  sinq12gt0  15150  sincosq1eq  15159  rpcxpsub  15228  relogbexpap  15278  logbleb  15281  logblt  15282  rplogbcxp  15283  lgsval4  15345  lgsmod  15351  lgsne0  15363  lgsmulsqcoprm  15371  2lgsoddprmlem1  15430