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

Theorem 3adant2 922
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1
Assertion
Ref Expression
3adant2

Proof of Theorem 3adant2
StepHypRef Expression
1 3simpb 901 . 2
2 3adant.1 . 2
31, 2syl 14 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  3ad2ant1  924  eupickb  1978  vtoclegft  2619  eqeu  2705  suc11g  4235  soinxp  4353  funopg  4877  fnco  4950  dff1o2  5074  fnimapr  5176  fvun1  5182  fvmptt  5205  fnreseql  5220  fvpr1g  5310  fvpr2g  5311  f1elima  5355  f1ocnvfvb  5363  oprssov  5584  poxp  5794  smoiso  5858  rdgivallem  5908  nndi  6004  nndir  6008  nnaord  6018  nnaordr  6019  nnaword  6020  nnawordi  6024  ecopovtrn  6139  ecopovtrng  6142  xpdom3m  6244  ltsopi  6304  addcanpig  6318  addassnqg  6366  distrnqg  6371  ltsonq  6382  ltmnqg  6385  prarloclemarch2  6402  nnanq0  6441  distrnq0  6442  distnq0r  6446  prltlu  6470  prarloclem5  6483  distrlem1prl  6558  distrlem1pru  6559  distrlem5prl  6562  distrlem5pru  6563  ltpopr  6569  ltsopr  6570  ltexprlemm  6574  ltexprlemfl  6583  ltexprlemfu  6585  lttrsr  6690  ltsosr  6692  ltasrg  6698  recexgt0sr  6701  mulextsr1lem  6706  mulextsr1  6707  axpre-mulext  6772  adddir  6816  axltwlin  6884  axlttrn  6885  ltleletr  6897  letr  6898  nnncan1  7043  npncan3  7045  pnpcan2  7047  subdi  7178  subdir  7179  reapcotr  7382  divmulap  7436  div23ap  7452  div13ap  7454  divsubdirap  7466  divcanap7  7479  ltmul2  7603  lemul2  7604  lemul2a  7606  lediv1  7616  ltmuldiv2  7622  lemuldiv2  7629  squeeze0  7651  nndivtr  7736  bndndx  7956  nn0n0n1ge2  8087  fnn0ind  8130  xrletr  8494  xrltne  8499  iooneg  8626  iccneg  8627  icoshft  8628  icoshftf1o  8629  fztri3or  8673  fzdcel  8674  fzen  8677  uzsubsubfz  8681  fzrevral2  8738  fzshftral  8740  fz0fzdiffz0  8757  elfzmlbmOLD  8759  elfzmlbp  8760  elfzo  8776  fzoaddel2  8819  fzosubel2  8821  elfzom1p1elfzo  8840  ssfzo12bi  8851  expdivap  8959  expubnd  8965  bernneq2  9023  bj-peano4  9415
  Copyright terms: Public domain W3C validator