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

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

Proof of Theorem 3adant1
StepHypRef Expression
1 3simpc 912 . 2  |-  ( ( th  /\  ph  /\  ps )  ->  ( ph  /\ 
ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 14 1  |-  ( ( th  /\  ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 894
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 896
This theorem is referenced by:  3ad2ant2  935  3ad2ant3  936  rsp2e  2387  sbciegft  2813  reuhyp  4229  suc11g  4306  soinxp  4435  breldmg  4566  funopg  4959  funimaexglem  5007  fex2  5084  fnreseql  5302  ftpg  5372  mpt2eq3ia  5595  mpt2fvex  5854  poxp  5878  smores3  5936  tfrlemibxssdm  5969  nndi  6093  nnmass  6094  nndir  6097  nnaord  6110  nnaordr  6111  nnawordi  6116  nnmord  6118  ecopovtrn  6231  ecopovtrng  6234  ltsopi  6446  addassnqg  6508  ltsonq  6524  ltmnqg  6527  distrnq0  6585  addlocpr  6662  distrlem1prl  6708  distrlem1pru  6709  distrlem4prl  6710  distrlem4pru  6711  ltpopr  6721  ltsopr  6722  addcanprg  6742  lttrsr  6875  ltsosr  6877  ltasrg  6883  recexgt0sr  6886  mulextsr1lem  6892  mulextsr1  6893  axpre-mulext  6990  adddir  7046  axltwlin  7116  axlttrn  7117  ltleletr  7129  letr  7130  mul32  7174  mul31  7175  add32  7203  subsub23  7249  addsubass  7254  subcan2  7269  subsub2  7272  nppcan2  7275  sub32  7278  nnncan  7279  nnncan2  7281  pnpcan2  7284  subdi  7424  subdir  7425  reapcotr  7633  receuap  7694  divmulap3  7700  divrecap  7711  divrecap2  7712  divsubdirap  7729  divdivap1  7744  redivclap  7752  div2negap  7756  ltmul2  7867  lemul2  7868  lemul2a  7870  lediv1  7880  gt0div  7881  ge0div  7882  ltdivmul  7887  ltdivmul2  7889  ledivmul2  7891  uzind2  8379  nn0ind  8381  fnn0ind  8383  uz3m2nn  8581  xrletr  8795  xrre2  8805  ixxdisj  8843  iooneg  8927  iccneg  8928  icoshft  8929  icoshftf1o  8930  icodisj  8931  fzen  8979  fzrev3  9021  2ffzeq  9070  fzoaddel2  9121  elfzodifsumelfzo  9129  ssfzo12bi  9153  fzoshftral  9166  adddivflid  9207  fldiv4p1lem1div2  9220  modqmulnn  9257  modqeqmodmin  9309  frec2uzf1od  9321  expdivap  9436  shftval2  9619  mulreap  9656  absdivap  9860  absdiflt  9882  absdifle  9883  abs3dif  9895  cau3  9905  dvdsmulc  10098  dvdsmultr1  10108  dvdsmultr2  10110  dvdssub2  10112  oexpneg  10151  nn0seqcvgd  10206  ialgcvga  10216  bj-peano4  10410
  Copyright terms: Public domain W3C validator