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

Theorem 3adant1 922
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 903 . 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 97    /\ w3a 885
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 887
This theorem is referenced by:  3ad2ant2  926  3ad2ant3  927  rsp2e  2372  sbciegft  2793  reuhyp  4204  suc11g  4281  soinxp  4410  breldmg  4541  funopg  4934  funimaexglem  4982  fex2  5059  fnreseql  5277  ftpg  5347  mpt2eq3ia  5570  mpt2fvex  5829  poxp  5853  smores3  5908  tfrlemibxssdm  5941  nndi  6065  nnmass  6066  nndir  6069  nnaord  6082  nnaordr  6083  nnawordi  6088  nnmord  6090  ecopovtrn  6203  ecopovtrng  6206  ltsopi  6418  addassnqg  6480  ltsonq  6496  ltmnqg  6499  distrnq0  6557  addlocpr  6634  distrlem1prl  6680  distrlem1pru  6681  distrlem4prl  6682  distrlem4pru  6683  ltpopr  6693  ltsopr  6694  addcanprg  6714  lttrsr  6847  ltsosr  6849  ltasrg  6855  recexgt0sr  6858  mulextsr1lem  6864  mulextsr1  6865  axpre-mulext  6962  adddir  7018  axltwlin  7087  axlttrn  7088  ltleletr  7100  letr  7101  mul32  7143  mul31  7144  add32  7170  subsub23  7216  addsubass  7221  subcan2  7236  subsub2  7239  nppcan2  7242  sub32  7245  nnncan  7246  nnncan2  7248  pnpcan2  7251  subdi  7382  subdir  7383  reapcotr  7589  receuap  7650  divmulap3  7656  divrecap  7667  divrecap2  7668  divsubdirap  7684  divdivap1  7699  redivclap  7707  div2negap  7711  ltmul2  7822  lemul2  7823  lemul2a  7825  lediv1  7835  gt0div  7836  ge0div  7837  ltdivmul  7842  ltdivmul2  7844  ledivmul2  7846  uzind2  8350  nn0ind  8352  fnn0ind  8354  uz3m2nn  8515  xrletr  8724  xrre2  8734  ixxdisj  8772  iooneg  8856  iccneg  8857  icoshft  8858  icoshftf1o  8859  icodisj  8860  fzen  8907  fzrev3  8949  2ffzeq  8998  fzoaddel2  9049  elfzodifsumelfzo  9057  ssfzo12bi  9081  fzoshftral  9094  adddivflid  9134  fldiv4p1lem1div2  9147  modqmulnn  9184  frec2uzf1od  9192  expdivap  9305  shftval2  9427  mulreap  9464  absdivap  9668  absdiflt  9688  absdifle  9689  abs3dif  9701  cau3  9711  nn0seqcvgd  9880  ialgcvga  9890  bj-peano4  10080
  Copyright terms: Public domain W3C validator