Theorem 3adant3 1012

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 989	. 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 973

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 975

This theorem is referenced by:  stoic4a  1425  stoic4b  1426  vtoclgft  2780  eqeu  2900  tpssi  3744  issod  4302  sotricim  4306  soinxp  4679  funopg  5230  fnco  5304  resasplitss  5375  resdif  5462  fnimapr  5554  ftpg  5677  fsnunfv  5694  fvpr1g  5699  fvpr2g  5700  f1ocnvfvb  5756  f1oiso2  5803  moriotass  5834  f1ofveu  5838  acexmid  5849  ovig  5971  ov6g  5987  ovg  5988  ot1stg  6128  ot2ndg  6129  poxp  6208  brtposg  6230  smores3  6269  smoiso  6278  rdgivallem  6357  frecsuclem  6382  nnaord  6485  nnaword  6487  nnawordex  6504  ecopovtrn  6606  ecopovtrng  6609  xpdom3m  6808  mapxpen  6822  sbthlemi4  6933  djuenun  7176  ltsopi  7269  addcanpig  7283  distrnqg  7336  ltsonq  7347  ltanqg  7349  ltmnqg  7350  nnanq0  7407  distrnq0  7408  distnq0r  7412  prarloclem  7450  genpassl  7473  genpassu  7474  distrlem1prl  7531  distrlem1pru  7532  distrlem5prl  7535  distrlem5pru  7536  1idprl  7539  1idpru  7540  ltpopr  7544  ltsopr  7545  ltexprlemm  7549  ltexprlemfl  7558  ltexprlemfu  7560  addcanprlemu  7564  recexprlem1ssl  7582  recexprlem1ssu  7583  aptipr  7590  lttrsr  7711  ltsosr  7713  ltasrg  7719  recexgt0sr  7722  mulextsr1  7730  axmulass  7822  ltxrlt  7972  axltwlin  7974  axlttrn  7975  axltadd  7976  letr  7989  mul12  8035  add12  8064  subadd  8109  addsub  8117  npncan  8127  nppcan  8128  nnpcan  8129  nppcan3  8130  pnpcan  8145  pnncan  8147  ppncan  8148  subdi  8291  ltaddsub2  8343  leaddsub2  8345  ltaddsublt  8477  apreap  8493  lemul1  8499  reapmul1lem  8500  reapadd1  8502  reapcotr  8504  receuap  8574  divassap  8594  div23ap  8595  divmulassap  8599  divmulasscomap  8600  divcanap4  8603  divsubdirap  8612  divcanap5  8618  divdiv32ap  8624  divdivap2  8628  div2subap  8741  letrp1  8751  ltmulgt12  8768  lediv1  8772  ltdiv2  8790  lediv2  8794  lbinfle  8853  difgtsumgt  9268  xrletr  9752  xrre2  9765  xaddass  9813  ixxdisj  9847  ubioc1  9873  lbico1  9874  elioo5  9877  iccsupr  9910  lbicc2  9928  ubicc2  9929  iccneg  9933  icoshft  9934  icodisj  9936  iccf1o  9948  iccen  9950  zltaddlt1le  9951  fztri3or  9982  fzdcel  9983  fzen  9986  uzsubsubfz  9990  fzrevral2  10049  fzshftral  10051  fz0fzdiffz0  10073  difelfznle  10078  fzo1fzo0n0  10126  fzonmapblen  10130  fzosubel2  10138  ubmelfzo  10143  elfzodifsumelfzo  10144  ssfzo12bi  10168  ubmelm1fzo  10169  subfzo0  10185  ceiqle  10256  modqid2  10294  zmodidfzoimp  10297  addmodidr  10316  modfzo0difsn  10338  addmodlteq  10341  frec2uzf1od  10349  exprecap  10504  expdivap  10514  expubnd  10520  sqdivap  10527  mulbinom2  10579  bernneq2  10584  bcval3  10672  bccmpl  10675  omgadd  10724  shftval2  10777  mulreap  10815  elicc4abs  11045  abssubge0  11053  abssuble0  11054  maxleast  11164  maxltsup  11169  xrmaxltsup  11208  xrmineqinf  11219  xrltmininf  11220  xrlemininf  11221  fsumdifsnconst  11405  prodfap0  11495  prodfrecap  11496  fprodabs  11566  sin01gt0  11711  cos01gt0  11712  sin02gt0  11713  dvdscmul  11767  summodnegmod  11771  modmulconst  11772  dvdsleabs  11792  dvdsleabs2  11793  addmodlteqALT  11806  dvdsexp  11808  mulmoddvds  11810  divalgb  11871  divgcdz  11913  gcdass  11957  mulgcdr  11960  gcddiv  11961  uzwodc  11979  lcmass  12026  coprmdvds  12033  qredeq  12037  qredeu  12038  congr  12041  divgcdcoprm0  12042  divgcdcoprmex  12043  cncongr1  12044  cncongr2  12045  isprm3  12059  dvdsnprmd  12066  euclemma  12087  prmdvdsexpb  12090  prmexpb  12092  rpexp  12094  znege1  12119  modprminv  12190  modprminveq  12191  vfermltl  12192  modprm0  12195  modprmn0modprm0  12197  coprimeprodsq  12198  coprimeprodsq2  12199  pythagtriplem1  12206  pythagtriplem3  12208  pythagtriplem6  12211  pythagtriplem12  12216  pythagtriplem13  12217  pythagtriplem14  12218  pythagtriplem16  12220  pythagtriplem19  12223  pythagtrip  12224  pcmul  12242  pcdiv  12243  pcqcl  12247  pcgcd1  12268  pcgcd  12269  dvdsprmpweq  12275  difsqpwdvds  12278  pcfaclem  12288  unbendc  12396  strle3g  12497  basgen  12833  clsss  12871  ntrin  12877  ntrcls0  12884  neiint  12898  neiss  12903  neipsm  12907  opnssneib  12909  innei  12916  restco  12927  iscnp  12952  cnconst2  12986  txcn  13028  psmetsym  13082  psmetlecl  13087  distspace  13088  xmetlecl  13120  xmetsym  13121  xblcntrps  13166  xblcntr  13167  blssec  13191  blpnfctr  13192  txmetcn  13272  cnmet  13283  dvid  13415  ptolemy  13498  sinq12gt0  13504  sincosq1eq  13513  rpcxpsub  13582  relogbexpap  13629  logbleb  13632  logblt  13633  rplogbcxp  13634  lgsval4  13674  lgsmod  13680  lgsne0  13692  lgsmulsqcoprm  13700