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

Theorem 3adant2 1000
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 979 . 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 103    /\ w3a 962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 964
This theorem is referenced by:  3ad2ant1  1002  eupickb  2080  vtoclegft  2758  eqeu  2854  suc11g  4472  soinxp  4609  funopg  5157  fnco  5231  dff1o2  5372  fnimapr  5481  fvun1  5487  fvmptt  5512  fnreseql  5530  fvpr1g  5626  fvpr2g  5627  f1elima  5674  f1ocnvfvb  5681  ovexg  5805  oprssov  5912  poxp  6129  smoiso  6199  rdgivallem  6278  nndi  6382  nndir  6386  fnsnsplitdc  6401  nnaord  6405  nnaordr  6406  nnaword  6407  nnawordi  6411  ecopovtrn  6526  ecopovtrng  6529  xpdom3m  6728  mapxpen  6742  findcard  6782  fisseneq  6820  resfnfinfinss  6828  funrnfi  6830  ltsopi  7135  addcanpig  7149  addassnqg  7197  distrnqg  7202  ltsonq  7213  ltmnqg  7216  prarloclemarch2  7234  nnanq0  7273  distrnq0  7274  distnq0r  7278  prltlu  7302  prarloclem5  7315  distrlem1prl  7397  distrlem1pru  7398  distrlem5prl  7401  distrlem5pru  7402  ltpopr  7410  ltsopr  7411  ltexprlemm  7415  ltexprlemfl  7424  ltexprlemfu  7426  lttrsr  7577  ltsosr  7579  ltasrg  7585  recexgt0sr  7588  mulextsr1lem  7595  mulextsr1  7596  axpre-mulext  7703  adddir  7764  axltwlin  7839  axlttrn  7840  ltleletr  7853  letr  7854  nnncan1  8005  npncan3  8007  pnpcan2  8009  subdi  8154  subdir  8155  reapcotr  8367  divmulap  8442  div23ap  8458  div13ap  8460  muldivdirap  8474  divsubdirap  8475  divcanap7  8488  ltmul2  8621  lemul2  8622  lemul2a  8624  lediv1  8634  ltmuldiv2  8640  lemuldiv2  8647  squeeze0  8669  nndivtr  8769  bndndx  8983  nn0n0n1ge2  9128  fnn0ind  9174  addlelt  9562  xrletr  9598  xrltne  9603  xleadd2a  9664  xleadd1  9665  xltadd2  9667  iooneg  9778  iccneg  9779  icoshft  9780  icoshftf1o  9781  zltaddlt1le  9796  fztri3or  9826  fzdcel  9827  fzen  9830  uzsubsubfz  9834  fzrevral2  9893  fzshftral  9895  fz0fzdiffz0  9914  elfzmlbp  9916  elfzo  9933  fzoaddel2  9977  fzosubel2  9979  elfzom1p1elfzo  9998  ssfzo12bi  10009  subfzo0  10026  flltdivnn0lt  10084  modqmulnn  10122  modfzo0difsn  10175  expdivap  10351  expubnd  10357  mulbinom2  10415  bernneq2  10420  shftuz  10596  shftval2  10605  abs3dif  10884  xrmaxlesup  11035  xrltmininf  11046  xrlemininf  11047  sin02gt0  11477  dvdsval2  11503  dvdscmul  11527  dvdsmulc  11528  ndvdssub  11634  rpmulgcd  11721  cncongr1  11791  cncongr2  11792  isprm3  11806  ntrin  12303  elnei  12331  cnrest2  12415  psmetsym  12508  psmetge0  12510  xmetge0  12544  xmetsym  12547  cnmet  12709  bj-peano4  13167
  Copyright terms: Public domain W3C validator