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

Theorem adantlr 468
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 108 . 2  |-  ( (
ph  /\  th )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 281 1  |-  ( ( ( ph  /\  th )  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  ad2antrr  479  ad2ant2r  500  ad2ant2rl  502  adantl3r  503  ad4ant14  505  ad4ant24  507  ad5ant13  510  ad5ant14  511  ad5ant15  512  3ad2antl1  1143  3ad2antl2  1144  ad4ant124  1194  3adant1r  1209  bilukdc  1374  intab  3800  pofun  4234  ralxfrd  4383  rexxfrd  4384  ordtri2or2exmidlem  4441  wessep  4492  poinxp  4608  relop  4689  fun11iun  5388  ssimaex  5482  fndmdif  5525  fconst2g  5635  foeqcnvco  5691  f1eqcocnv  5692  isocnv  5712  isocnv2  5713  riota2df  5750  grprinvd  5966  grpridd  5967  f1o2ndf1  6125  tfr1onlembacc  6239  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllembacc  6252  tfrcllemaccex  6258  tfrcllemres  6259  tfrcldm  6260  tfrcl  6261  xpdom2  6725  fimax2gtrilemstep  6794  xpfi  6818  eqsupti  6883  ordiso2  6920  enumctlemm  6999  cc2lem  7086  mulcanpig  7155  prarloclemlt  7313  genpdf  7328  genpdisj  7343  addnqprl  7349  addnqpru  7350  addlocpr  7356  prmuloc  7386  mulnqprl  7388  mulnqpru  7389  mullocpr  7391  ltpopr  7415  ltsopr  7416  ltaddpr  7417  ltexprlemdisj  7426  ltexprlemloc  7427  ltexprlemru  7432  addcanprleml  7434  addcanprlemu  7435  ltaprg  7439  recexprlemopu  7447  recexprlemloc  7451  cauappcvgprlemladdfl  7475  cauappcvgprlemladdru  7476  caucvgsrlemcau  7613  caucvgsrlemgt1  7615  caucvgsrlemoffcau  7618  caucvgsrlemoffres  7620  suplocsrlem  7628  axcaucvglemcau  7718  axpre-suploclemres  7721  axsuploc  7849  cnegexlem1  7949  cnegexlem3  7951  cnegex  7952  addsubeq4  7989  rimul  8359  divcanap6  8491  ltmul12a  8630  lemul12b  8631  lbinf  8718  zrevaddcl  9116  nzadd  9118  zextle  9154  fzind  9178  uz11  9360  qreccl  9446  qrevaddcl  9448  irradd  9450  xrlttr  9593  xrltso  9594  xaddass  9664  xleadd1a  9668  xlt2add  9675  iccshftr  9789  iccshftl  9791  iccdil  9793  icccntr  9795  divelunit  9797  uzsubsubfz  9839  fzaddel  9851  fzrev  9876  elfzmlbp  9921  frec2uzrdg  10194  frecuzrdgtcl  10197  frecuzrdgsuc  10199  frecuzrdgdomlem  10202  frecuzrdgfunlem  10204  frecuzrdgsuctlem  10208  iseqovex  10241  seq3val  10243  seqf  10246  seq3clss  10252  seq3fveq2  10254  seq3feq2  10255  seq3feq  10257  seq3shft2  10258  ser3mono  10263  seq3split  10264  seq3caopr3  10266  seq3caopr2  10267  iseqf1olemab  10274  seq3f1olemqsumkj  10283  seq3f1olemqsumk  10284  seq3f1olemqsum  10285  seq3f1olemstep  10286  seq3f1oleml  10288  seq3id3  10292  seq3id  10293  seq3id2  10294  seq3homo  10295  seq3z  10296  seqfeq3  10297  ser3ge0  10302  expp1  10312  expnegap0  10313  expcllem  10316  mulexp  10344  expadd  10347  expaddzap  10349  expmulzap  10351  expdivap  10356  leexp1a  10360  expnlbnd  10428  bcpasc  10524  bccl  10525  hashfacen  10591  seq3coll  10597  seq3shft  10622  resqrexlemfp1  10793  sqrtdiv  10826  climshftlemg  11083  climcn1  11089  climsqz  11116  climsqz2  11117  clim2ser  11118  clim2ser2  11119  isermulc2  11121  climub  11125  serf0  11133  fsum3cvg  11159  sumrbdc  11160  summodclem3  11161  summodclem2a  11162  zsumdc  11165  fsumf1o  11171  isumss  11172  fisumss  11173  isumss2  11174  fsum3cvg2  11175  fsum3cvg3  11177  fsumcl2lem  11179  fsumcllem  11180  fsumadd  11187  fsumsplit  11188  fsumsplitsn  11191  sumsplitdc  11213  fisumrev2  11227  fsum2mul  11234  fsum00  11243  telfsumo  11247  fsumparts  11251  iserabs  11256  cvgratnnlemabsle  11308  cvgratnn  11312  cvgratz  11313  mertenslemub  11315  mertenslemi1  11316  mertenslem2  11317  mertensabs  11318  clim2prod  11320  clim2divap  11321  prodfap0  11326  prodfrecap  11327  prodeq2  11338  fproddccvg  11353  prodrbdclem2  11354  prodmodc  11359  eftlcvg  11405  negdvdsb  11520  dvdsnegb  11521  dvdsext  11564  addmodlteqALT  11568  nno  11614  infssuzex  11653  gcdsupex  11657  gcdsupcl  11658  bezoutlembz  11703  dvdssq  11730  eucalgf  11747  dvdslcm  11761  lcmledvds  11762  lcmeq0  11763  lcmcl  11764  lcmdvds  11771  lcmgcdeq  11775  divgcdcoprmex  11794  phibndlem  11903  phiprmpw  11909  ctiunctlemf  11962  ctiunct  11964  opnssneib  12339  neissex  12348  tgrest  12352  iscnp3  12386  cnpnei  12402  cnrest  12418  tx1cn  12452  txcnp  12454  elbl3ps  12577  elbl3  12578  blininf  12607  blssexps  12612  blssex  12613  blpnfctr  12622  mopni2  12666  blsscls2  12676  metss  12677  bdmet  12685  metrest  12689  metcn  12697  txmetcn  12702  bl2ioo  12725  ivthinclemlr  12798  ivthinclemur  12800  dvcj  12856  dvfre  12857  coseq0q4123  12937  abssinper  12949  subctctexmid  13255  cvgcmp2n  13289
  Copyright terms: Public domain W3C validator