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

Theorem sylan 271
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
Hypotheses
Ref Expression
sylan.1  |-  ( ph  ->  ps )
sylan.2  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
sylan  |-  ( (
ph  /\  ch )  ->  th )

Proof of Theorem sylan
StepHypRef Expression
1 sylan.1 . 2  |-  ( ph  ->  ps )
2 sylan.2 . . 3  |-  ( ( ps  /\  ch )  ->  th )
32expcom 113 . 2  |-  ( ch 
->  ( ps  ->  th )
)
41, 3mpan9 269 1  |-  ( (
ph  /\  ch )  ->  th )
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:  sylanb  272  sylanbr  273  syl2an  277  sylanl1  388  sylanl2  389  mpanl1  418  mpanl2  419  adantll  453  adantlr  454  ancom1s  511  3adantl1  1071  3adantl2  1072  3adantl3  1073  syl3anl1  1194  syl3anl3  1196  syl3anl  1197  stoic3  1336  eupick  1995  csbiebt  2914  csbnestgf  2926  reuss2  3245  mpteq12  3868  otexg  3995  opelopabt  4027  sonr  4082  sotr  4083  issod  4084  so2nr  4086  so3nr  4087  ordelss  4144  onelon  4149  elrnmpt1s  4612  iota2  4921  funeu  4954  imadif  5007  fnbr  5029  feu  5100  f1ss  5125  f1ssres  5127  dffo2  5138  foco  5144  foun  5173  fun11iun  5175  ffoss  5186  funbrfv  5240  fvco3  5272  fvopab6  5292  funfvbrb  5308  elpreima  5314  ffvelrn  5328  ffvelrnda  5330  dffo4  5343  foelrn  5345  fmptco  5358  fsn2  5365  fvconst2g  5403  fex  5416  funfvima  5418  f1elima  5440  f1ocnvfv1  5445  f1ocnvfv2  5446  cocan2  5456  foeqcnvco  5458  isocnv  5479  isores2  5481  isoini  5485  isoselem  5487  f1oiso  5493  f1ofveu  5528  eloprabga  5619  grprinvlem  5723  suppssof1  5756  ofco  5757  offveqb  5758  fnexALT  5768  f1dmex  5771  ot1stg  5807  ot2ndg  5808  ot3rdgg  5809  eqopi  5826  2ndrn  5837  fo2ndf  5876  smores3  5939  smores2  5940  smoel  5946  smoiso  5948  tfrlem1  5954  tfrlemisucaccv  5970  tfrlemibxssdm  5972  tfrlemiubacc  5975  rdgon  6004  frecrdg  6023  freccl  6024  omv2  6076  nnasuc  6086  nnmsuc  6087  nnacom  6094  nnaass  6095  nnmass  6097  nntri1  6105  nnmordi  6120  swoer  6165  erth  6181  riinerm  6210  qliftlem  6215  ecovass  6246  ecoviass  6247  f1domg  6269  endomtr  6301  xpsnen2g  6334  enen1  6342  enen2  6343  domen1  6344  domen2  6345  phplem1  6346  findcard  6376  findcard2  6377  findcard2s  6378  isotilem  6410  supisolem  6412  ordiso2  6415  addclpi  6483  addasspig  6486  mulasspig  6488  addnidpig  6492  nnppipi  6499  ltanqi  6558  ltmnqi  6559  ltexnqq  6564  archnqq  6573  prarloclemarch2  6575  enq0sym  6588  enq0tr  6590  nqnq0pi  6594  nqnq0  6597  mulcanenq0ec  6601  addclnq0  6607  nqpnq0nq  6609  distrnq0  6615  addassnq0lemcl  6617  addassnq0  6618  prubl  6642  prarloclemlt  6649  genpdf  6664  genipv  6665  genpelvl  6668  genpelvu  6669  genpml  6673  genpmu  6674  genprndl  6677  genprndu  6678  genpassl  6680  genpassu  6681  genpassg  6682  addnqprl  6685  addnqpru  6686  addlocpr  6692  nqprm  6698  nqprl  6707  nqpru  6708  mulnqprl  6724  mulnqpru  6725  mullocprlem  6726  mullocpr  6727  addcomprg  6734  mulcomprg  6736  distrlem1prl  6738  distrlem1pru  6739  distrlem4prl  6740  distrlem4pru  6741  ltprordil  6745  1idprl  6746  1idpru  6747  ltpopr  6751  ltsopr  6752  ltaddpr  6753  ltexprlemm  6756  ltexprlemopl  6757  ltexprlemlol  6758  ltexprlemopu  6759  ltexprlemupu  6760  ltexprlemdisj  6762  ltexprlemloc  6763  ltexprlemfl  6765  ltexprlemrl  6766  ltexprlemfu  6767  ltexprlemru  6768  addcanprleml  6770  addcanprlemu  6771  prplnqu  6776  recexprlemloc  6787  recexprlem1ssl  6789  recexprlem1ssu  6790  recexprlemss1l  6791  recexprlemss1u  6792  aptiprleml  6795  aptiprlemu  6796  cauappcvgprlemloc  6808  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgprlemloc  6831  caucvgprlemladdrl  6834  caucvgprprlemml  6850  caucvgprprlemloc  6859  00sr  6912  adddir  7076  eqle  7168  le2tri3i  7185  mul4  7206  muladd11  7207  cnegexlem3  7251  addsub12  7287  2addsub  7288  addsubeq4  7289  subadd4  7318  negcon1  7326  negdi2  7332  negsubdi2  7333  neg2sub  7334  renegcl  7335  muladd  7453  subdir  7455  gt0ne0  7496  ltnegcon1  7532  lenegcon1  7535  recexre  7643  ltmul1  7657  recexap  7708  div12ap  7747  p1le  7890  ltmul2  7897  gt0div  7911  ge0div  7912  zlem1lt  8358  nnaddm1cl  8363  zdceq  8374  gtndiv  8393  prime  8396  msqznn  8397  btwnz  8416  uzss  8589  eluzadd  8597  nn0pzuz  8626  divfnzn  8653  qnegcl  8668  qreccl  8674  elico2  8907  iccss  8911  iccsupr  8936  elfz5  8984  fznn  9053  difelfznle  9095  fzoaddel  9150  qdceq  9204  qbtwnxr  9214  flqbi2  9241  adddivflid  9242  fldivnn0  9245  divfl0  9246  flqmulnn0  9249  fldivnn0le  9253  fldiv4p1lem1div2  9255  ceiqle  9263  flqdiv  9271  modqmulnn  9292  frec2uzzd  9350  frecuzrdgfn  9362  frecuzrdgcl  9363  frecuzrdgsuc  9365  iseqsplit  9402  iseqcaopr2  9405  iseqid  9411  iseqz  9413  expap0  9450  mulexp  9459  mulexpzap  9460  expmul  9465  leexp1a  9475  expubnd  9477  zesq  9535  bernneq  9537  bernneq3  9539  facdiv  9606  facndiv  9607  faclbnd3  9611  faclbnd6  9612  bccmpl  9622  bcpasc  9634  bccl  9635  shftlem  9645  ovshftex  9648  shftval4  9657  shftf  9659  shftcan2  9664  crim  9686  mulreap  9692  remul2  9701  immul2  9708  cjexp  9721  caucvgre  9808  r19.2uz  9820  sqrtsq2  9870  absnid  9900  absexp  9906  nn0abscl  9912  abslt  9915  lenegsq  9922  cau3lem  9941  clim  10033  climshftlemg  10054  climcn1  10060  climcn1lem  10070  clim2iser  10088  clim2iser2  10089  iiserex  10090  iisermulc2  10091  climub  10095  climcaucn  10101  serif0  10102  dvdsval3  10112  iddvdsexp  10131  alzdvds  10166  addmodlteqALT  10171  nnehalf  10216  nno  10218  ndvdsadd  10243  ialgcvg  10270  ialgcvga  10273  ialgfx  10274  bj-inex  10414  bj-nn0suc  10476  bj-nn0sucALT  10490
  Copyright terms: Public domain W3C validator