Theorem 3adant3 1002

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 979	. 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 103   /\ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  stoic4a  1409  stoic4b  1410  vtoclgft  2739  eqeu  2858  tpssi  3694  issod  4249  sotricim  4253  soinxp  4617  funopg  5165  fnco  5239  resasplitss  5310  resdif  5397  fnimapr  5489  ftpg  5612  fsnunfv  5629  fvpr1g  5634  fvpr2g  5635  f1ocnvfvb  5689  f1oiso2  5736  moriotass  5766  f1ofveu  5770  acexmid  5781  ovig  5900  ov6g  5916  ovg  5917  ot1stg  6058  ot2ndg  6059  poxp  6137  brtposg  6159  smores3  6198  smoiso  6207  rdgivallem  6286  frecsuclem  6311  nnaord  6413  nnaword  6415  nnawordex  6432  ecopovtrn  6534  ecopovtrng  6537  xpdom3m  6736  mapxpen  6750  sbthlemi4  6856  djuenun  7085  ltsopi  7152  addcanpig  7166  distrnqg  7219  ltsonq  7230  ltanqg  7232  ltmnqg  7233  nnanq0  7290  distrnq0  7291  distnq0r  7295  prarloclem  7333  genpassl  7356  genpassu  7357  distrlem1prl  7414  distrlem1pru  7415  distrlem5prl  7418  distrlem5pru  7419  1idprl  7422  1idpru  7423  ltpopr  7427  ltsopr  7428  ltexprlemm  7432  ltexprlemfl  7441  ltexprlemfu  7443  addcanprlemu  7447  recexprlem1ssl  7465  recexprlem1ssu  7466  aptipr  7473  lttrsr  7594  ltsosr  7596  ltasrg  7602  recexgt0sr  7605  mulextsr1  7613  axmulass  7705  ltxrlt  7854  axltwlin  7856  axlttrn  7857  axltadd  7858  letr  7871  mul12  7915  add12  7944  subadd  7989  addsub  7997  npncan  8007  nppcan  8008  nnpcan  8009  nppcan3  8010  pnpcan  8025  pnncan  8027  ppncan  8028  subdi  8171  ltaddsub2  8223  leaddsub2  8225  ltaddsublt  8357  apreap  8373  lemul1  8379  reapmul1lem  8380  reapadd1  8382  reapcotr  8384  receuap  8454  divassap  8474  div23ap  8475  divmulassap  8479  divmulasscomap  8480  divcanap4  8483  divsubdirap  8492  divcanap5  8498  divdiv32ap  8504  divdivap2  8508  div2subap  8620  letrp1  8630  ltmulgt12  8647  lediv1  8651  ltdiv2  8669  lediv2  8673  lbinfle  8732  xrletr  9621  xrre2  9634  xaddass  9682  ixxdisj  9716  ubioc1  9742  lbico1  9743  elioo5  9746  iccsupr  9779  lbicc2  9797  ubicc2  9798  iccneg  9802  icoshft  9803  icodisj  9805  iccf1o  9817  iccen  9819  zltaddlt1le  9820  fztri3or  9850  fzdcel  9851  fzen  9854  uzsubsubfz  9858  fzrevral2  9917  fzshftral  9919  fz0fzdiffz0  9938  difelfznle  9943  fzo1fzo0n0  9991  fzonmapblen  9995  fzosubel2  10003  ubmelfzo  10008  elfzodifsumelfzo  10009  ssfzo12bi  10033  ubmelm1fzo  10034  subfzo0  10050  ceiqle  10117  modqid2  10155  zmodidfzoimp  10158  addmodidr  10177  modfzo0difsn  10199  addmodlteq  10202  frec2uzf1od  10210  exprecap  10365  expdivap  10375  expubnd  10381  sqdivap  10388  mulbinom2  10439  bernneq2  10444  bcval3  10529  bccmpl  10532  omgadd  10580  shftval2  10630  mulreap  10668  elicc4abs  10898  abssubge0  10906  abssuble0  10907  maxleast  11017  maxltsup  11022  xrmaxltsup  11059  xrmineqinf  11070  xrltmininf  11071  xrlemininf  11072  fsumdifsnconst  11256  prodfap0  11346  prodfrecap  11347  sin01gt0  11504  cos01gt0  11505  sin02gt0  11506  dvdscmul  11556  summodnegmod  11560  modmulconst  11561  dvdsleabs  11579  dvdsleabs2  11580  addmodlteqALT  11593  dvdsexp  11595  mulmoddvds  11597  divalgb  11658  divgcdz  11696  gcdass  11739  mulgcdr  11742  gcddiv  11743  lcmass  11802  coprmdvds  11809  qredeq  11813  qredeu  11814  congr  11817  divgcdcoprm0  11818  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  isprm3  11835  dvdsnprmd  11842  euclemma  11860  prmdvdsexpb  11863  prmexpb  11865  rpexp  11867  znege1  11892  strle3g  12090  basgen  12288  clsss  12326  ntrin  12332  ntrcls0  12339  neiint  12353  neiss  12358  neipsm  12362  opnssneib  12364  innei  12371  restco  12382  iscnp  12407  cnconst2  12441  txcn  12483  psmetsym  12537  psmetlecl  12542  distspace  12543  xmetlecl  12575  xmetsym  12576  xblcntrps  12621  xblcntr  12622  blssec  12646  blpnfctr  12647  txmetcn  12727  cnmet  12738  dvid  12870  ptolemy  12953  sinq12gt0  12959  sincosq1eq  12968  rpcxpsub  13037  relogbexpap  13083  logbleb  13086  logblt  13087  rplogbcxp  13088