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

Theorem 3adant1 1015
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 996 . 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 104    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  3ad2ant2  1019  3ad2ant3  1020  rsp2e  2528  sbciegft  2993  reuhyp  4469  suc11g  4553  soinxp  4693  breldmg  4829  funopg  5246  funimaexglem  5295  fex2  5380  fnreseql  5622  ftpg  5696  mpoeq3ia  5934  funexw  6107  mpofvex  6198  poxp  6227  smores3  6288  tfrlemibxssdm  6322  nndi  6481  nnmass  6482  nndir  6485  fnsnsplitdc  6500  nnaord  6504  nnaordr  6505  nnawordi  6510  nnmord  6512  ecopovtrn  6626  ecopovtrng  6629  ixpf  6714  mapxpen  6842  netap  7244  2omotaplemap  7247  ltsopi  7310  addassnqg  7372  ltsonq  7388  ltmnqg  7391  distrnq0  7449  addlocpr  7526  distrlem1prl  7572  distrlem1pru  7573  distrlem4prl  7574  distrlem4pru  7575  ltpopr  7585  ltsopr  7586  addcanprg  7606  lttrsr  7752  ltsosr  7754  ltasrg  7760  recexgt0sr  7763  mulextsr1lem  7770  mulextsr1  7771  axpre-mulext  7878  adddir  7939  axltwlin  8015  axlttrn  8016  ltleletr  8029  letr  8030  mul32  8077  mul31  8078  add32  8106  subsub23  8152  addsubass  8157  subcan2  8172  subsub2  8175  nppcan2  8178  sub32  8181  nnncan  8182  nnncan2  8184  pnpcan2  8187  subdi  8332  subdir  8333  reapcotr  8545  receuap  8615  divmulap3  8623  divrecap  8634  divrecap2  8635  divsubdirap  8654  divdivap1  8669  redivclap  8677  div2negap  8681  ltmul2  8802  lemul2  8803  lemul2a  8805  lediv1  8815  gt0div  8816  ge0div  8817  ltdivmul  8822  ltdivmul2  8824  ledivmul2  8826  uzind2  9354  nn0ind  9356  fnn0ind  9358  uz3m2nn  9562  xrletr  9795  xrre2  9808  xleadd2a  9861  xleadd1  9862  xltadd2  9864  ixxdisj  9890  iooneg  9975  iccneg  9976  icoshft  9977  icoshftf1o  9978  icodisj  9979  fzen  10029  fzrev3  10073  2ffzeq  10127  fzoaddel2  10179  elfzodifsumelfzo  10187  ssfzo12bi  10211  fzoshftral  10224  adddivflid  10278  fldiv4p1lem1div2  10291  modqmulnn  10328  modqeqmodmin  10380  frec2uzf1od  10392  expdivap  10557  shftval2  10819  mulreap  10857  absdivap  11063  absdiflt  11085  absdifle  11086  abs3dif  11098  cau3  11108  ltmininf  11227  xrmaxlesup  11251  xrltmininf  11262  xrlemininf  11263  xrminltinf  11264  geoisum1c  11512  dvdsmulc  11810  dvdsmultr1  11822  dvdsmultr2  11824  dvdssub2  11826  oexpneg  11865  divalgb  11913  ndvdsadd  11919  gcdaddm  11968  modgcd  11975  dvdsgcd  11996  dvdsgcdb  11997  gcdass  11999  mulgcd  12000  absmulgcd  12001  rpmulgcd  12010  nn0seqcvgd  12024  algcvga  12034  lcmdvds  12062  lcmdvdsb  12067  lcmass  12068  coprmdvds  12075  coprmdvds2  12076  rpmul  12081  cncongr1  12086  cncongr2  12087  prmgt1  12115  qnumdenbi  12175  coprimeprodsq  12240  pythagtriplem4  12251  pythagtriplem8  12255  pythagtriplem9  12256  pythagtriplem12  12258  pythagtriplem14  12260  pythagtriplem16  12262  pcpremul  12276  pcgcd  12311  setsvala  12476  setsex  12477  ressval2  12508  isgrpi  12790  grpsubrcan  12840  grpinvsub  12841  grpsubeq0  12845  grpsubadd0sub  12846  grpnpcan  12851  opprmulg  13068  unopn  13170  clsss  13285  opnssneib  13323  restabs  13342  upxp  13439  blpnfctr  13606  mscl  13632  xmscl  13633  xmsge0  13634  xmseq0  13635  rpdivcxp  13999  cxpcom  14024  rplogbreexp  14038  rplogbzexp  14039  rprelogbmulexp  14041  logbleb  14046  logblt  14047  lgsneg  14092  lgsne0  14106  lgsmodeq  14113  lgsmulsqcoprm  14114  bj-peano4  14363
  Copyright terms: Public domain W3C validator