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

Theorem 3adant3 923
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1
Assertion
Ref Expression
3adant3

Proof of Theorem 3adant3
StepHypRef Expression
1 3simpa 900 . 2
2 3adant.1 . 2
31, 2syl 14 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  stoic4a  1318  stoic4b  1319  vtoclgft  2598  eqeu  2705  tpssi  3521  issod  4047  sotricim  4051  soinxp  4353  funopg  4877  fnco  4950  resasplitss  5012  resdif  5091  fnimapr  5176  ftpg  5290  fsnunfv  5306  fvpr1g  5310  fvpr2g  5311  f1ocnvfvb  5363  f1oiso2  5409  moriotass  5439  f1ofveu  5443  acexmid  5454  ovig  5564  ov6g  5580  ovg  5581  ot1stg  5721  ot2ndg  5722  poxp  5794  brtposg  5810  smores3  5849  smoiso  5858  rdgivallem  5908  frecsuclemdm  5927  frecsuclem3  5929  nnaord  6018  nnaword  6020  nnawordex  6037  ecopovtrn  6139  ecopovtrng  6142  xpdom3m  6244  ltsopi  6304  addcanpig  6318  distrnqg  6371  ltsonq  6382  ltanqg  6384  ltmnqg  6385  nnanq0  6441  distrnq0  6442  distnq0r  6446  prarloclem  6484  genpassl  6507  genpassu  6508  distrlem1prl  6558  distrlem1pru  6559  distrlem5prl  6562  distrlem5pru  6563  1idprl  6566  1idpru  6567  ltpopr  6569  ltsopr  6570  ltexprlemm  6574  ltexprlemfl  6583  ltexprlemfu  6585  addcanprlemu  6589  recexprlem1ssl  6605  recexprlem1ssu  6606  aptipr  6613  lttrsr  6690  ltsosr  6692  ltasrg  6698  recexgt0sr  6701  mulextsr1  6707  axmulass  6757  ltxrlt  6882  axltwlin  6884  axlttrn  6885  axltadd  6886  letr  6898  mul12  6939  add12  6966  subadd  7011  addsub  7019  npncan  7028  nppcan  7029  nnpcan  7030  nppcan3  7031  pnpcan  7046  pnncan  7048  ppncan  7049  subdi  7178  ltaddsub2  7227  leaddsub2  7229  ltaddsublt  7355  apreap  7371  lemul1  7377  reapmul1lem  7378  reapadd1  7380  reapcotr  7382  receuap  7432  divassap  7451  div23ap  7452  divcanap4  7458  divsubdirap  7466  divcanap5  7472  divdiv32ap  7478  divdivap2  7482  letrp1  7595  ltmulgt12  7612  lediv1  7616  ltdiv2  7634  lediv2  7638  xrletr  8494  xrre2  8504  ixxdisj  8542  ubioc1  8568  lbico1  8569  elioo5  8572  iccsupr  8605  lbicc2  8622  ubicc2  8623  iccneg  8627  icoshft  8628  icodisj  8630  iccf1o  8642  fztri3or  8673  fzdcel  8674  fzen  8677  uzsubsubfz  8681  fzrevral2  8738  fzshftral  8740  fz0fzdiffz0  8757  elfzmlbmOLD  8759  difelfznle  8763  fzo1fzo0n0  8809  fzonmapblen  8813  fzosubel2  8821  ubmelfzo  8826  elfzodifsumelfzo  8827  ssfzo12bi  8851  ubmelm1fzo  8852  frec2uzf1od  8873  exprecap  8950  expdivap  8959  expubnd  8965  sqdivap  8972  bernneq2  9023  mulreap  9092
  Copyright terms: Public domain W3C validator