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

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

Proof of Theorem 3adant3
StepHypRef Expression
1 3simpa 912 . 2  |-  ( (
ph  /\  ps  /\  th )  ->  ( ph  /\  ps ) )
2 3adant.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2syl 14 1  |-  ( (
ph  /\  ps  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  stoic4a  1337  stoic4b  1338  vtoclgft  2621  eqeu  2734  tpssi  3558  issod  4084  sotricim  4088  soinxp  4438  funopg  4962  fnco  5035  resasplitss  5097  resdif  5176  fnimapr  5261  ftpg  5375  fsnunfv  5391  fvpr1g  5395  fvpr2g  5396  f1ocnvfvb  5448  f1oiso2  5494  moriotass  5524  f1ofveu  5528  acexmid  5539  ovig  5650  ov6g  5666  ovg  5667  ot1stg  5807  ot2ndg  5808  poxp  5881  brtposg  5900  smores3  5939  smoiso  5948  rdgivallem  5999  frecsuclemdm  6019  frecsuclem3  6021  nnaord  6113  nnaword  6115  nnawordex  6132  ecopovtrn  6234  ecopovtrng  6237  xpdom3m  6339  ltsopi  6476  addcanpig  6490  distrnqg  6543  ltsonq  6554  ltanqg  6556  ltmnqg  6557  nnanq0  6614  distrnq0  6615  distnq0r  6619  prarloclem  6657  genpassl  6680  genpassu  6681  distrlem1prl  6738  distrlem1pru  6739  distrlem5prl  6742  distrlem5pru  6743  1idprl  6746  1idpru  6747  ltpopr  6751  ltsopr  6752  ltexprlemm  6756  ltexprlemfl  6765  ltexprlemfu  6767  addcanprlemu  6771  recexprlem1ssl  6789  recexprlem1ssu  6790  aptipr  6797  lttrsr  6905  ltsosr  6907  ltasrg  6913  recexgt0sr  6916  mulextsr1  6923  axmulass  7005  ltxrlt  7144  axltwlin  7146  axlttrn  7147  axltadd  7148  letr  7160  mul12  7203  add12  7232  subadd  7277  addsub  7285  npncan  7295  nppcan  7296  nnpcan  7297  nppcan3  7298  pnpcan  7313  pnncan  7315  ppncan  7316  subdi  7454  ltaddsub2  7506  leaddsub2  7508  ltaddsublt  7636  apreap  7652  lemul1  7658  reapmul1lem  7659  reapadd1  7661  reapcotr  7663  receuap  7724  divassap  7743  div23ap  7744  divcanap4  7750  divsubdirap  7759  divcanap5  7765  divdiv32ap  7771  divdivap2  7775  letrp1  7889  ltmulgt12  7906  lediv1  7910  ltdiv2  7928  lediv2  7932  xrletr  8825  xrre2  8835  ixxdisj  8873  ubioc1  8899  lbico1  8900  elioo5  8903  iccsupr  8936  lbicc2  8953  ubicc2  8954  iccneg  8958  icoshft  8959  icodisj  8961  iccf1o  8973  zltaddlt1le  8975  fztri3or  9005  fzdcel  9006  fzen  9009  uzsubsubfz  9013  fzrevral2  9070  fzshftral  9072  fz0fzdiffz0  9089  elfzmlbmOLD  9091  difelfznle  9095  fzo1fzo0n0  9141  fzonmapblen  9145  fzosubel2  9153  ubmelfzo  9158  elfzodifsumelfzo  9159  ssfzo12bi  9183  ubmelm1fzo  9184  subfzo0  9199  ceiqle  9263  modqid2  9301  zmodidfzoimp  9304  addmodidr  9323  modfzo0difsn  9345  addmodlteq  9348  frec2uzf1od  9356  exprecap  9461  expdivap  9471  expubnd  9477  sqdivap  9484  mulbinom2  9533  bernneq2  9538  bcval3  9619  bccmpl  9622  shftval2  9655  mulreap  9692  elicc4abs  9921  abssubge0  9929  abssuble0  9930  dvdscmul  10134  summodnegmod  10138  modmulconst  10139  dvdsleabs  10157  dvdsleabs2  10158  addmodlteqALT  10171  dvdsexp  10173  mulmoddvds  10175  divalgb  10237
  Copyright terms: Public domain W3C validator