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

Theorem adantlr 461
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 107 . 2  |-  ( (
ph  /\  th )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 277 1  |-  ( ( ( ph  /\  th )  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
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 is referenced by:  ad2antrr  472  ad2ant2r  493  ad2ant2rl  495  3ad2antl1  1101  3ad2antl2  1102  3adant1r  1163  bilukdc  1328  intab  3685  pofun  4095  ralxfrd  4240  rexxfrd  4241  ordtri2or2exmidlem  4297  wessep  4348  poinxp  4455  relop  4534  fun11iun  5198  ssimaex  5286  fndmdif  5324  fconst2g  5428  foeqcnvco  5481  f1eqcocnv  5482  isocnv  5502  isocnv2  5503  riota2df  5539  grprinvd  5747  grpridd  5748  f1o2ndf1  5900  tfr1onlembacc  6011  tfr1onlemaccex  6017  tfr1onlemres  6018  tfrcllembacc  6024  tfrcllemaccex  6030  tfrcllemres  6031  tfrcldm  6032  tfrcl  6033  xpdom2  6396  xpfi  6472  eqsupti  6503  ordiso2  6540  mulcanpig  6639  prarloclemlt  6797  genpdf  6812  genpdisj  6827  addnqprl  6833  addnqpru  6834  addlocpr  6840  prmuloc  6870  mulnqprl  6872  mulnqpru  6873  mullocpr  6875  ltpopr  6899  ltsopr  6900  ltaddpr  6901  ltexprlemdisj  6910  ltexprlemloc  6911  ltexprlemru  6916  addcanprleml  6918  addcanprlemu  6919  ltaprg  6923  recexprlemopu  6931  recexprlemloc  6935  cauappcvgprlemladdfl  6959  cauappcvgprlemladdru  6960  caucvgsrlemcau  7083  caucvgsrlemgt1  7085  caucvgsrlemoffcau  7088  caucvgsrlemoffres  7090  axcaucvglemcau  7178  cnegexlem1  7402  cnegexlem3  7404  cnegex  7405  addsubeq4  7442  rimul  7804  divcanap6  7926  ltmul12a  8057  lemul12b  8058  lbinf  8145  zrevaddcl  8534  nzadd  8536  zextle  8571  fzind  8595  uz11  8774  qreccl  8860  qrevaddcl  8862  irradd  8864  xrlttr  8998  xrltso  8999  iccshftr  9144  iccshftl  9146  iccdil  9148  icccntr  9150  divelunit  9152  uzsubsubfz  9194  fzaddel  9205  fzrev  9229  elfzmlbp  9272  frec2uzrdg  9543  frecuzrdgtcl  9546  frecuzrdgsuc  9548  frecuzrdgdomlem  9551  frecuzrdgfunlem  9553  frecuzrdgsuctlem  9557  iseqovex  9581  iseqval  9582  iseqvalt  9584  iseqfclt  9588  iseqoveq  9592  iseqss  9593  iseqsst  9594  iseqfveq2  9596  iseqfeq2  9597  iseqfeq  9599  iseqshft2  9600  isermono  9605  iseqsplit  9606  iseqcaopr3  9608  iseqcaopr2  9609  iseqid3s  9614  iseqid  9615  iseqid2  9616  iseqhomo  9617  iseqz  9618  expivallem  9626  expival  9627  expp1  9632  expnegap0  9633  expcllem  9636  mulexp  9664  expadd  9667  expaddzap  9669  expmulzap  9671  expdivap  9676  leexp1a  9680  expnlbnd  9746  bcpasc  9842  bccl  9843  resqrexlemfp1  10096  sqrtdiv  10129  climshftlemg  10342  climcn1  10348  climsqz  10374  climsqz2  10375  clim2iser  10376  clim2iser2  10377  iisermulc2  10379  iserile  10381  climub  10383  climserile  10384  serif0  10390  fisumcvg  10401  isumrb  10402  negdvdsb  10419  dvdsnegb  10420  dvdsext  10463  addmodlteqALT  10467  nno  10513  infssuzex  10552  gcdsupex  10556  gcdsupcl  10557  bezoutlembz  10600  dvdssq  10627  eucalgf  10644  dvdslcm  10658  lcmledvds  10659  lcmeq0  10660  lcmcl  10661  lcmdvds  10668  lcmgcdeq  10672  divgcdcoprmex  10691  phibndlem  10799  phiprmpw  10805
  Copyright terms: Public domain W3C validator