ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3adant3 Unicode version

Theorem 3adant3 984
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
StepHypRef Expression
1 3simpa 961 . 2  |-  ( (
ph  /\  ps  /\  th )  ->  ( ph  /\  ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 14 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 945
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 947
This theorem is referenced by:  stoic4a  1391  stoic4b  1392  vtoclgft  2708  eqeu  2825  tpssi  3654  issod  4209  sotricim  4213  soinxp  4577  funopg  5125  fnco  5199  resasplitss  5270  resdif  5355  fnimapr  5447  ftpg  5570  fsnunfv  5587  fvpr1g  5592  fvpr2g  5593  f1ocnvfvb  5647  f1oiso2  5694  moriotass  5724  f1ofveu  5728  acexmid  5739  ovig  5858  ov6g  5874  ovg  5875  ot1stg  6016  ot2ndg  6017  poxp  6095  brtposg  6117  smores3  6156  smoiso  6165  rdgivallem  6244  frecsuclem  6269  nnaord  6371  nnaword  6373  nnawordex  6390  ecopovtrn  6492  ecopovtrng  6495  xpdom3m  6694  mapxpen  6708  sbthlemi4  6814  djuenun  7032  ltsopi  7092  addcanpig  7106  distrnqg  7159  ltsonq  7170  ltanqg  7172  ltmnqg  7173  nnanq0  7230  distrnq0  7231  distnq0r  7235  prarloclem  7273  genpassl  7296  genpassu  7297  distrlem1prl  7354  distrlem1pru  7355  distrlem5prl  7358  distrlem5pru  7359  1idprl  7362  1idpru  7363  ltpopr  7367  ltsopr  7368  ltexprlemm  7372  ltexprlemfl  7381  ltexprlemfu  7383  addcanprlemu  7387  recexprlem1ssl  7405  recexprlem1ssu  7406  aptipr  7413  lttrsr  7534  ltsosr  7536  ltasrg  7542  recexgt0sr  7545  mulextsr1  7553  axmulass  7645  ltxrlt  7794  axltwlin  7796  axlttrn  7797  axltadd  7798  letr  7811  mul12  7855  add12  7884  subadd  7929  addsub  7937  npncan  7947  nppcan  7948  nnpcan  7949  nppcan3  7950  pnpcan  7965  pnncan  7967  ppncan  7968  subdi  8111  ltaddsub2  8163  leaddsub2  8165  ltaddsublt  8296  apreap  8312  lemul1  8318  reapmul1lem  8319  reapadd1  8321  reapcotr  8323  receuap  8390  divassap  8410  div23ap  8411  divmulassap  8415  divmulasscomap  8416  divcanap4  8419  divsubdirap  8428  divcanap5  8434  divdiv32ap  8440  divdivap2  8444  div2subap  8556  letrp1  8563  ltmulgt12  8580  lediv1  8584  ltdiv2  8602  lediv2  8606  lbinfle  8665  xrletr  9531  xrre2  9544  xaddass  9592  ixxdisj  9626  ubioc1  9652  lbico1  9653  elioo5  9656  iccsupr  9689  lbicc2  9707  ubicc2  9708  iccneg  9712  icoshft  9713  icodisj  9715  iccf1o  9727  zltaddlt1le  9729  fztri3or  9759  fzdcel  9760  fzen  9763  uzsubsubfz  9767  fzrevral2  9826  fzshftral  9828  fz0fzdiffz0  9847  difelfznle  9852  fzo1fzo0n0  9900  fzonmapblen  9904  fzosubel2  9912  ubmelfzo  9917  elfzodifsumelfzo  9918  ssfzo12bi  9942  ubmelm1fzo  9943  subfzo0  9959  ceiqle  10026  modqid2  10064  zmodidfzoimp  10067  addmodidr  10086  modfzo0difsn  10108  addmodlteq  10111  frec2uzf1od  10119  exprecap  10274  expdivap  10284  expubnd  10290  sqdivap  10297  mulbinom2  10348  bernneq2  10353  bcval3  10437  bccmpl  10440  omgadd  10488  shftval2  10538  mulreap  10576  elicc4abs  10806  abssubge0  10814  abssuble0  10815  maxleast  10925  maxltsup  10930  xrmaxltsup  10967  xrmineqinf  10978  xrltmininf  10979  xrlemininf  10980  fsumdifsnconst  11164  sin01gt0  11367  cos01gt0  11368  sin02gt0  11369  dvdscmul  11416  summodnegmod  11420  modmulconst  11421  dvdsleabs  11439  dvdsleabs2  11440  addmodlteqALT  11453  dvdsexp  11455  mulmoddvds  11457  divalgb  11518  divgcdz  11556  gcdass  11599  mulgcdr  11602  gcddiv  11603  lcmass  11662  coprmdvds  11669  qredeq  11673  qredeu  11674  congr  11677  divgcdcoprm0  11678  divgcdcoprmex  11679  cncongr1  11680  cncongr2  11681  isprm3  11695  dvdsnprmd  11702  euclemma  11720  prmdvdsexpb  11723  prmexpb  11725  rpexp  11727  znege1  11751  strle3g  11946  basgen  12144  clsss  12182  ntrin  12188  ntrcls0  12195  neiint  12209  neiss  12214  neipsm  12218  opnssneib  12220  innei  12227  restco  12238  iscnp  12263  cnconst2  12297  txcn  12339  psmetsym  12393  psmetlecl  12398  distspace  12399  xmetlecl  12431  xmetsym  12432  xblcntrps  12477  xblcntr  12478  blssec  12502  blpnfctr  12503  txmetcn  12583  cnmet  12594  dvid  12705
  Copyright terms: Public domain W3C validator