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

Theorem adantlr 454
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
adantlr  |-  ( ( ( ph  /\  th )  /\  ps )  ->  ch )

Proof of Theorem adantlr
StepHypRef Expression
1 simpl 106 . 2  |-  ( (
ph  /\  th )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 271 1  |-  ( ( ( ph  /\  th )  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  ad2antrr  465  ad2ant2r  486  ad2ant2rl  488  3ad2antl1  1077  3ad2antl2  1078  3adant1r  1139  bilukdc  1303  intab  3671  pofun  4076  ralxfrd  4221  rexxfrd  4222  ordtri2or2exmidlem  4278  wessep  4329  poinxp  4436  relop  4513  fun11iun  5174  ssimaex  5261  fndmdif  5299  fconst2g  5403  foeqcnvco  5457  f1eqcocnv  5458  isocnv  5478  isocnv2  5479  riota2df  5515  grprinvd  5723  grpridd  5724  f1o2ndf1  5876  xpdom2  6335  eqsupti  6401  ordiso2  6414  mulcanpig  6490  prarloclemlt  6648  genpdf  6663  genpdisj  6678  addnqprl  6684  addnqpru  6685  addlocpr  6691  prmuloc  6721  mulnqprl  6723  mulnqpru  6724  mullocpr  6726  ltpopr  6750  ltsopr  6751  ltaddpr  6752  ltexprlemdisj  6761  ltexprlemloc  6762  ltexprlemru  6767  addcanprleml  6769  addcanprlemu  6770  ltaprg  6774  recexprlemopu  6782  recexprlemloc  6786  cauappcvgprlemladdfl  6810  cauappcvgprlemladdru  6811  caucvgsrlemcau  6934  caucvgsrlemgt1  6936  caucvgsrlemoffcau  6939  caucvgsrlemoffres  6941  axcaucvglemcau  7029  cnegexlem1  7248  cnegexlem3  7250  cnegex  7251  addsubeq4  7288  rimul  7649  divcanap6  7769  ltmul12a  7900  lemul12b  7901  zrevaddcl  8351  nzadd  8353  zextle  8388  fzind  8411  uz11  8590  qreccl  8673  qrevaddcl  8675  irradd  8677  xrlttr  8816  xrltso  8817  iccshftr  8962  iccshftl  8964  iccdil  8966  icccntr  8968  divelunit  8970  uzsubsubfz  9012  fzaddel  9023  fzrev  9047  elfzmlbp  9091  frec2uzrdg  9353  frecuzrdgfn  9356  frecuzrdgcl  9357  frecuzrdgsuc  9359  iseqovex  9377  iseqval  9378  iseqf  9382  iseqss  9384  iseqfveq2  9386  iseqfeq2  9387  iseqfeq  9389  iseqshft2  9390  isermono  9395  iseqsplit  9396  iseqcaopr3  9398  iseqcaopr2  9399  iseqid3s  9404  iseqid  9405  iseqhomo  9406  iseqz  9407  expivallem  9415  expival  9416  expp1  9421  expnegap0  9422  expcllem  9425  mulexp  9453  expadd  9456  expaddzap  9458  expmulzap  9460  expdivap  9465  leexp1a  9469  expnlbnd  9534  bcpasc  9627  bccl  9628  resqrexlemfp1  9828  sqrtdiv  9861  climshftlemg  10046  climcn1  10052  climsqz  10078  climsqz2  10079  clim2iser  10080  clim2iser2  10081  iisermulc2  10083  iserile  10085  climub  10087  climserile  10088  serif0  10094  negdvdsb  10116  dvdsnegb  10117  dvdsext  10159  addmodlteqALT  10163  nno  10210
  Copyright terms: Public domain W3C validator