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

Theorem 3adant2 934
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
3adant2  |-  ( (
ph  /\  th  /\  ps )  ->  ch )

Proof of Theorem 3adant2
StepHypRef Expression
1 3simpb 913 . 2  |-  ( (
ph  /\  th  /\  ps )  ->  ( ph  /\  ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 14 1  |-  ( (
ph  /\  th  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  3ad2ant1  936  eupickb  1997  vtoclegft  2642  eqeu  2734  suc11g  4309  soinxp  4438  funopg  4962  fnco  5035  dff1o2  5159  fnimapr  5261  fvun1  5267  fvmptt  5290  fnreseql  5305  fvpr1g  5395  fvpr2g  5396  f1elima  5440  f1ocnvfvb  5448  ovexg  5567  oprssov  5670  poxp  5881  smoiso  5948  rdgivallem  5999  nndi  6096  nndir  6100  nnaord  6113  nnaordr  6114  nnaword  6115  nnawordi  6119  ecopovtrn  6234  ecopovtrng  6237  xpdom3m  6339  findcard  6376  ltsopi  6476  addcanpig  6490  addassnqg  6538  distrnqg  6543  ltsonq  6554  ltmnqg  6557  prarloclemarch2  6575  nnanq0  6614  distrnq0  6615  distnq0r  6619  prltlu  6643  prarloclem5  6656  distrlem1prl  6738  distrlem1pru  6739  distrlem5prl  6742  distrlem5pru  6743  ltpopr  6751  ltsopr  6752  ltexprlemm  6756  ltexprlemfl  6765  ltexprlemfu  6767  lttrsr  6905  ltsosr  6907  ltasrg  6913  recexgt0sr  6916  mulextsr1lem  6922  mulextsr1  6923  axpre-mulext  7020  adddir  7076  axltwlin  7146  axlttrn  7147  ltleletr  7159  letr  7160  nnncan1  7310  npncan3  7312  pnpcan2  7314  subdi  7454  subdir  7455  reapcotr  7663  divmulap  7728  div23ap  7744  div13ap  7746  muldivdirap  7758  divsubdirap  7759  divcanap7  7772  ltmul2  7897  lemul2  7898  lemul2a  7900  lediv1  7910  ltmuldiv2  7916  lemuldiv2  7923  squeeze0  7945  nndivtr  8031  bndndx  8238  nn0n0n1ge2  8369  fnn0ind  8413  addlelt  8786  xrletr  8825  xrltne  8830  iooneg  8957  iccneg  8958  icoshft  8959  icoshftf1o  8960  zltaddlt1le  8975  fztri3or  9005  fzdcel  9006  fzen  9009  uzsubsubfz  9013  fzrevral2  9070  fzshftral  9072  fz0fzdiffz0  9089  elfzmlbmOLD  9091  elfzmlbp  9092  elfzo  9108  fzoaddel2  9151  fzosubel2  9153  elfzom1p1elfzo  9172  ssfzo12bi  9183  subfzo0  9199  flltdivnn0lt  9254  modqmulnn  9292  modfzo0difsn  9345  expdivap  9471  expubnd  9477  mulbinom2  9533  bernneq2  9538  shftuz  9646  shftval2  9655  abs3dif  9932  dvdsval2  10111  dvdscmul  10134  dvdsmulc  10135  ndvdssub  10242  bj-peano4  10467
  Copyright terms: Public domain W3C validator