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

Theorem 3adant1 957
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 938 . 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 102    /\ w3a 920
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 922
This theorem is referenced by:  3ad2ant2  961  3ad2ant3  962  rsp2e  2415  sbciegft  2845  reuhyp  4230  suc11g  4308  soinxp  4436  breldmg  4569  funopg  4964  funimaexglem  5013  fex2  5090  fnreseql  5309  ftpg  5379  mpt2eq3ia  5601  mpt2fvex  5860  poxp  5884  smores3  5942  tfrlemibxssdm  5976  nndi  6130  nnmass  6131  nndir  6134  nnaord  6148  nnaordr  6149  nnawordi  6154  nnmord  6156  ecopovtrn  6269  ecopovtrng  6272  ltsopi  6572  addassnqg  6634  ltsonq  6650  ltmnqg  6653  distrnq0  6711  addlocpr  6788  distrlem1prl  6834  distrlem1pru  6835  distrlem4prl  6836  distrlem4pru  6837  ltpopr  6847  ltsopr  6848  addcanprg  6868  lttrsr  7001  ltsosr  7003  ltasrg  7009  recexgt0sr  7012  mulextsr1lem  7018  mulextsr1  7019  axpre-mulext  7116  adddir  7172  axltwlin  7247  axlttrn  7248  ltleletr  7260  letr  7261  mul32  7305  mul31  7306  add32  7334  subsub23  7380  addsubass  7385  subcan2  7400  subsub2  7403  nppcan2  7406  sub32  7409  nnncan  7410  nnncan2  7412  pnpcan2  7415  subdi  7556  subdir  7557  reapcotr  7765  receuap  7826  divmulap3  7832  divrecap  7843  divrecap2  7844  divsubdirap  7863  divdivap1  7878  redivclap  7886  div2negap  7890  ltmul2  8001  lemul2  8002  lemul2a  8004  lediv1  8014  gt0div  8015  ge0div  8016  ltdivmul  8021  ltdivmul2  8023  ledivmul2  8025  uzind2  8540  nn0ind  8542  fnn0ind  8544  uz3m2nn  8742  xrletr  8954  xrre2  8964  ixxdisj  9002  iooneg  9086  iccneg  9087  icoshft  9088  icoshftf1o  9089  icodisj  9090  fzen  9138  fzrev3  9180  2ffzeq  9228  fzoaddel2  9279  elfzodifsumelfzo  9287  ssfzo12bi  9311  fzoshftral  9324  adddivflid  9374  fldiv4p1lem1div2  9387  modqmulnn  9424  modqeqmodmin  9476  frec2uzf1od  9488  expdivap  9624  shftval2  9852  mulreap  9889  absdivap  10094  absdiflt  10116  absdifle  10117  abs3dif  10129  cau3  10139  ltmininf  10254  dvdsmulc  10368  dvdsmultr1  10378  dvdsmultr2  10380  dvdssub2  10382  oexpneg  10421  divalgb  10469  ndvdsadd  10475  gcdaddm  10519  modgcd  10526  dvdsgcd  10545  dvdsgcdb  10546  gcdass  10548  mulgcd  10549  absmulgcd  10550  rpmulgcd  10559  nn0seqcvgd  10567  ialgcvga  10577  lcmdvds  10605  lcmdvdsb  10610  lcmass  10611  coprmdvds  10618  coprmdvds2  10619  rpmul  10624  cncongr1  10629  cncongr2  10630  prmgt1  10657  qnumdenbi  10714  bj-peano4  10935
  Copyright terms: Public domain W3C validator