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

Theorem 3adant2 962
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 941 . 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 102    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  3ad2ant1  964  eupickb  2029  vtoclegft  2691  eqeu  2785  suc11g  4373  soinxp  4508  funopg  5048  fnco  5122  dff1o2  5258  fnimapr  5364  fvun1  5370  fvmptt  5394  fnreseql  5409  fvpr1g  5503  fvpr2g  5504  f1elima  5552  f1ocnvfvb  5559  ovexg  5683  oprssov  5786  poxp  5997  smoiso  6067  rdgivallem  6146  nndi  6247  nndir  6251  nnaord  6266  nnaordr  6267  nnaword  6268  nnawordi  6272  ecopovtrn  6387  ecopovtrng  6390  xpdom3m  6548  mapxpen  6562  findcard  6602  fisseneq  6640  resfnfinfinss  6647  funrnfi  6649  ltsopi  6877  addcanpig  6891  addassnqg  6939  distrnqg  6944  ltsonq  6955  ltmnqg  6958  prarloclemarch2  6976  nnanq0  7015  distrnq0  7016  distnq0r  7020  prltlu  7044  prarloclem5  7057  distrlem1prl  7139  distrlem1pru  7140  distrlem5prl  7143  distrlem5pru  7144  ltpopr  7152  ltsopr  7153  ltexprlemm  7157  ltexprlemfl  7166  ltexprlemfu  7168  lttrsr  7306  ltsosr  7308  ltasrg  7314  recexgt0sr  7317  mulextsr1lem  7323  mulextsr1  7324  axpre-mulext  7421  adddir  7477  axltwlin  7552  axlttrn  7553  ltleletr  7565  letr  7566  nnncan1  7716  npncan3  7718  pnpcan2  7720  subdi  7861  subdir  7862  reapcotr  8073  divmulap  8140  div23ap  8156  div13ap  8158  muldivdirap  8172  divsubdirap  8173  divcanap7  8186  ltmul2  8315  lemul2  8316  lemul2a  8318  lediv1  8328  ltmuldiv2  8334  lemuldiv2  8341  squeeze0  8363  nndivtr  8462  bndndx  8670  nn0n0n1ge2  8815  fnn0ind  8860  addlelt  9237  xrletr  9271  xrltne  9276  iooneg  9403  iccneg  9404  icoshft  9405  icoshftf1o  9406  zltaddlt1le  9421  fztri3or  9451  fzdcel  9452  fzen  9455  uzsubsubfz  9459  fzrevral2  9516  fzshftral  9518  fz0fzdiffz0  9537  elfzmlbp  9539  elfzo  9556  fzoaddel2  9600  fzosubel2  9602  elfzom1p1elfzo  9621  ssfzo12bi  9632  subfzo0  9649  flltdivnn0lt  9707  modqmulnn  9745  modfzo0difsn  9798  expdivap  10002  expubnd  10008  mulbinom2  10066  bernneq2  10071  shftuz  10247  shftval2  10256  abs3dif  10534  sin02gt0  11050  dvdsval2  11073  dvdscmul  11097  dvdsmulc  11098  ndvdssub  11204  rpmulgcd  11289  cncongr1  11359  cncongr2  11360  isprm3  11374  bj-peano4  11805
  Copyright terms: Public domain W3C validator