Theorem 3adant3 1007

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 984	. 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 968

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 970

This theorem is referenced by:  stoic4a  1420  stoic4b  1421  vtoclgft  2776  eqeu  2896  tpssi  3739  issod  4297  sotricim  4301  soinxp  4674  funopg  5222  fnco  5296  resasplitss  5367  resdif  5454  fnimapr  5546  ftpg  5669  fsnunfv  5686  fvpr1g  5691  fvpr2g  5692  f1ocnvfvb  5748  f1oiso2  5795  moriotass  5826  f1ofveu  5830  acexmid  5841  ovig  5963  ov6g  5979  ovg  5980  ot1stg  6120  ot2ndg  6121  poxp  6200  brtposg  6222  smores3  6261  smoiso  6270  rdgivallem  6349  frecsuclem  6374  nnaord  6477  nnaword  6479  nnawordex  6496  ecopovtrn  6598  ecopovtrng  6601  xpdom3m  6800  mapxpen  6814  sbthlemi4  6925  djuenun  7168  ltsopi  7261  addcanpig  7275  distrnqg  7328  ltsonq  7339  ltanqg  7341  ltmnqg  7342  nnanq0  7399  distrnq0  7400  distnq0r  7404  prarloclem  7442  genpassl  7465  genpassu  7466  distrlem1prl  7523  distrlem1pru  7524  distrlem5prl  7527  distrlem5pru  7528  1idprl  7531  1idpru  7532  ltpopr  7536  ltsopr  7537  ltexprlemm  7541  ltexprlemfl  7550  ltexprlemfu  7552  addcanprlemu  7556  recexprlem1ssl  7574  recexprlem1ssu  7575  aptipr  7582  lttrsr  7703  ltsosr  7705  ltasrg  7711  recexgt0sr  7714  mulextsr1  7722  axmulass  7814  ltxrlt  7964  axltwlin  7966  axlttrn  7967  axltadd  7968  letr  7981  mul12  8027  add12  8056  subadd  8101  addsub  8109  npncan  8119  nppcan  8120  nnpcan  8121  nppcan3  8122  pnpcan  8137  pnncan  8139  ppncan  8140  subdi  8283  ltaddsub2  8335  leaddsub2  8337  ltaddsublt  8469  apreap  8485  lemul1  8491  reapmul1lem  8492  reapadd1  8494  reapcotr  8496  receuap  8566  divassap  8586  div23ap  8587  divmulassap  8591  divmulasscomap  8592  divcanap4  8595  divsubdirap  8604  divcanap5  8610  divdiv32ap  8616  divdivap2  8620  div2subap  8733  letrp1  8743  ltmulgt12  8760  lediv1  8764  ltdiv2  8782  lediv2  8786  lbinfle  8845  difgtsumgt  9260  xrletr  9744  xrre2  9757  xaddass  9805  ixxdisj  9839  ubioc1  9865  lbico1  9866  elioo5  9869  iccsupr  9902  lbicc2  9920  ubicc2  9921  iccneg  9925  icoshft  9926  icodisj  9928  iccf1o  9940  iccen  9942  zltaddlt1le  9943  fztri3or  9974  fzdcel  9975  fzen  9978  uzsubsubfz  9982  fzrevral2  10041  fzshftral  10043  fz0fzdiffz0  10065  difelfznle  10070  fzo1fzo0n0  10118  fzonmapblen  10122  fzosubel2  10130  ubmelfzo  10135  elfzodifsumelfzo  10136  ssfzo12bi  10160  ubmelm1fzo  10161  subfzo0  10177  ceiqle  10248  modqid2  10286  zmodidfzoimp  10289  addmodidr  10308  modfzo0difsn  10330  addmodlteq  10333  frec2uzf1od  10341  exprecap  10496  expdivap  10506  expubnd  10512  sqdivap  10519  mulbinom2  10571  bernneq2  10576  bcval3  10664  bccmpl  10667  omgadd  10715  shftval2  10768  mulreap  10806  elicc4abs  11036  abssubge0  11044  abssuble0  11045  maxleast  11155  maxltsup  11160  xrmaxltsup  11199  xrmineqinf  11210  xrltmininf  11211  xrlemininf  11212  fsumdifsnconst  11396  prodfap0  11486  prodfrecap  11487  fprodabs  11557  sin01gt0  11702  cos01gt0  11703  sin02gt0  11704  dvdscmul  11758  summodnegmod  11762  modmulconst  11763  dvdsleabs  11783  dvdsleabs2  11784  addmodlteqALT  11797  dvdsexp  11799  mulmoddvds  11801  divalgb  11862  divgcdz  11904  gcdass  11948  mulgcdr  11951  gcddiv  11952  uzwodc  11970  lcmass  12017  coprmdvds  12024  qredeq  12028  qredeu  12029  congr  12032  divgcdcoprm0  12033  divgcdcoprmex  12034  cncongr1  12035  cncongr2  12036  isprm3  12050  dvdsnprmd  12057  euclemma  12078  prmdvdsexpb  12081  prmexpb  12083  rpexp  12085  znege1  12110  modprminv  12181  modprminveq  12182  vfermltl  12183  modprm0  12186  modprmn0modprm0  12188  coprimeprodsq  12189  coprimeprodsq2  12190  pythagtriplem1  12197  pythagtriplem3  12199  pythagtriplem6  12202  pythagtriplem12  12207  pythagtriplem13  12208  pythagtriplem14  12209  pythagtriplem16  12211  pythagtriplem19  12214  pythagtrip  12215  pcmul  12233  pcdiv  12234  pcqcl  12238  pcgcd1  12259  pcgcd  12260  dvdsprmpweq  12266  difsqpwdvds  12269  pcfaclem  12279  unbendc  12387  strle3g  12487  basgen  12720  clsss  12758  ntrin  12764  ntrcls0  12771  neiint  12785  neiss  12790  neipsm  12794  opnssneib  12796  innei  12803  restco  12814  iscnp  12839  cnconst2  12873  txcn  12915  psmetsym  12969  psmetlecl  12974  distspace  12975  xmetlecl  13007  xmetsym  13008  xblcntrps  13053  xblcntr  13054  blssec  13078  blpnfctr  13079  txmetcn  13159  cnmet  13170  dvid  13302  ptolemy  13385  sinq12gt0  13391  sincosq1eq  13400  rpcxpsub  13469  relogbexpap  13516  logbleb  13519  logblt  13520  rplogbcxp  13521  lgsval4  13561  lgsmod  13567  lgsne0  13579  lgsmulsqcoprm  13587