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

Theorem sylan 281
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 115 . 2  |-  ( ch 
->  ( ps  ->  th )
)
41, 3mpan9 279 1  |-  ( (
ph  /\  ch )  ->  th )
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:  sylanb  282  sylanbr  283  syl2an  287  sylanl1  400  sylanl2  401  mpanl1  431  mpanl2  432  adantll  468  adantlr  469  ancom1s  559  3adantl1  1138  3adantl2  1139  3adantl3  1140  syl3anl1  1265  syl3anl3  1267  syl3anl  1268  stoic3  1408  eupick  2079  csbiebt  3040  csbnestgf  3053  reuss2  3357  mpteq12  4015  otexg  4156  opelopabt  4188  sonr  4243  sotr  4244  issod  4245  so2nr  4247  so3nr  4248  ordelss  4305  onelon  4310  elrnmpt1s  4793  iota2  5118  funeu  5152  imadif  5207  fnbr  5229  feu  5309  f1ss  5338  f1ssres  5341  f1resf1  5342  dffo2  5353  foco  5359  foun  5390  fun11iun  5392  ffoss  5403  funbrfv  5464  fvco3  5496  fvopab6  5521  funfvbrb  5537  elpreima  5543  ffvelrn  5557  ffvelrnda  5559  dffo4  5572  fmptco  5590  fsn2  5598  fvconst2g  5638  fex  5651  funfvima  5653  f1elima  5678  f1ocnvfv1  5682  f1ocnvfv2  5683  cocan2  5693  foeqcnvco  5695  isocnv  5716  isores2  5718  isoini  5723  isoselem  5725  f1oiso  5731  f1ofveu  5766  eloprabga  5862  grprinvlem  5969  suppssof1  6003  ofco  6004  offveqb  6005  fnexALT  6015  f1dmex  6018  ot1stg  6054  ot2ndg  6055  ot3rdgg  6056  eqopi  6074  2ndrn  6085  fo2ndf  6128  smores3  6194  smores2  6195  smoel  6201  smoiso  6203  tfrlem1  6209  tfrlemisucaccv  6226  tfrlemibxssdm  6228  tfrlemiubacc  6231  tfr1onlemsucaccv  6242  tfr1onlembfn  6245  tfr1onlemubacc  6247  tfr1onlemaccex  6249  tfr1onlemres  6250  tfrcllemsucaccv  6255  tfrcllembfn  6258  tfrcllemubacc  6260  tfrcllemaccex  6262  tfrcllemres  6263  tfrcl  6265  frecrdg  6309  omv2  6365  nnasuc  6376  nnmsuc  6377  nnacom  6384  nnaass  6385  nnmass  6387  nntri1  6396  nndifsnid  6407  nnmordi  6416  swoer  6461  erth  6477  riinerm  6506  qliftlem  6511  ecovass  6542  ecoviass  6543  elmapssres  6571  fvixp  6601  f1domg  6656  endomtr  6688  xpsnen2g  6727  enen1  6738  enen2  6739  domen1  6740  domen2  6741  mapen  6744  mapxpen  6746  ssenen  6749  phplem1  6750  fidifsnid  6769  findcard  6786  findcard2  6787  findcard2s  6788  fieq0  6868  isotilem  6897  supisolem  6899  inflbti  6915  ordiso2  6924  djuex  6932  updjudhcoinlf  6969  updjudhcoinrg  6970  updjud  6971  ctssdccl  7000  enumctlemm  7003  finomni  7016  nnnninf  7027  pm54.43  7059  acfun  7076  ccfunen  7092  cc2lem  7094  cc3  7096  addclpi  7155  addasspig  7158  mulasspig  7160  addnidpig  7164  nnppipi  7171  ltanqi  7230  ltmnqi  7231  ltexnqq  7236  archnqq  7245  prarloclemarch2  7247  enq0sym  7260  enq0tr  7262  nqnq0pi  7266  nqnq0  7269  mulcanenq0ec  7273  addclnq0  7279  nqpnq0nq  7281  distrnq0  7287  addassnq0lemcl  7289  addassnq0  7290  prubl  7314  prarloclemlt  7321  genpdf  7336  genipv  7337  genpelvl  7340  genpelvu  7341  genpml  7345  genpmu  7346  genprndl  7349  genprndu  7350  genpassl  7352  genpassu  7353  genpassg  7354  addnqprl  7357  addnqpru  7358  addlocpr  7364  nqprm  7370  nqprl  7379  nqpru  7380  mulnqprl  7396  mulnqpru  7397  mullocprlem  7398  mullocpr  7399  addcomprg  7406  mulcomprg  7408  distrlem1prl  7410  distrlem1pru  7411  distrlem4prl  7412  distrlem4pru  7413  ltprordil  7417  1idprl  7418  1idpru  7419  ltpopr  7423  ltsopr  7424  ltaddpr  7425  ltexprlemm  7428  ltexprlemopl  7429  ltexprlemlol  7430  ltexprlemopu  7431  ltexprlemupu  7432  ltexprlemdisj  7434  ltexprlemloc  7435  ltexprlemfl  7437  ltexprlemrl  7438  ltexprlemfu  7439  ltexprlemru  7440  addcanprleml  7442  addcanprlemu  7443  prplnqu  7448  recexprlemloc  7459  recexprlem1ssl  7461  recexprlem1ssu  7462  recexprlemss1l  7463  recexprlemss1u  7464  aptiprleml  7467  aptiprlemu  7468  cauappcvgprlemloc  7480  cauappcvgprlemladdru  7484  cauappcvgprlemladdrl  7485  caucvgprlemloc  7503  caucvgprlemladdrl  7506  caucvgprprlemml  7522  caucvgprprlemloc  7531  00sr  7597  map2psrprg  7633  suplocsrlempr  7635  suplocsrlem  7636  adddir  7777  axsuploc  7857  eqle  7875  le2tri3i  7892  mul4  7914  muladd11  7915  cnegexlem3  7959  addsub12  7995  2addsub  7996  addsubeq4  7997  subadd4  8026  negcon1  8034  negdi2  8040  negsubdi2  8041  neg2sub  8042  renegcl  8043  muladd  8166  subdir  8168  gt0ne0  8209  ltnegcon1  8245  lenegcon1  8248  eqord1  8265  eqord2  8266  recexre  8360  ltmul1  8374  recexap  8434  div12ap  8474  p1le  8627  ltmul2  8634  gt0div  8648  ge0div  8649  zlem1lt  9130  nnaddm1cl  9135  zdceq  9146  gtndiv  9166  prime  9170  msqznn  9171  btwnz  9190  uzss  9366  eluzadd  9374  nn0pzuz  9405  supinfneg  9413  infsupneg  9414  divfnzn  9436  qnegcl  9451  qreccl  9457  elpqb  9464  xaddass  9678  xleadd1a  9682  xlesubadd  9692  elico2  9746  iccss  9750  iccsupr  9775  elfz5  9825  fznn  9896  difelfznle  9939  fzoaddel  9996  qdceq  10051  qbtwnxr  10062  flqbi2  10091  adddivflid  10092  fldivnn0  10095  divfl0  10096  flqmulnn0  10099  fldivnn0le  10103  fldiv4p1lem1div2  10105  ceiqle  10113  flqdiv  10121  modqmulnn  10142  frecuzrdgtcl  10212  frecuzrdgsuc  10214  frecuzrdgdomlem  10217  frecuzrdgfunlem  10219  frecuzrdgsuctlem  10223  seq3caopr2  10282  iseqf1olemkle  10284  seq3f1olemp  10302  seq3id  10308  seq3z  10311  expap0  10350  mulexp  10359  mulexpzap  10360  expmul  10365  leexp1a  10375  expubnd  10377  zesq  10437  bernneq  10439  bernneq3  10441  facdiv  10512  facndiv  10513  faclbnd3  10517  faclbnd6  10518  bccmpl  10528  bcpasc  10540  bccl  10541  seq3coll  10613  shftlem  10616  ovshftex  10619  shftval4  10628  shftf  10630  shftcan2  10635  crim  10658  mulreap  10664  remul2  10673  immul2  10680  cjexp  10693  caucvgre  10781  r19.2uz  10793  sqrtsq2  10843  absnid  10873  absexp  10879  nn0abscl  10885  abslt  10888  lenegsq  10895  cau3lem  10914  minmax  11029  xrmaxadd  11058  clim  11078  climshftlemg  11099  climcn1  11105  climcn1lem  11116  clim2ser  11134  clim2ser2  11135  iserex  11136  isermulc2  11137  climub  11141  climcaucn  11148  serf0  11149  summodclem3  11177  summodclem2a  11178  summodclem2  11179  summodc  11180  fsum3  11184  fsumf1o  11187  fisumss  11189  isumss2  11190  fsumcl2lem  11195  fsumadd  11203  fsumsplit  11204  isummulc2  11223  fsum2d  11232  fsummulc2  11245  telfsumo  11263  fsumparts  11267  hash2iun1dif1  11277  bcxmas  11286  isumshft  11287  isumsplit  11288  expcnvap0  11299  geolim  11308  geolim2  11309  cvgratnnlemmn  11322  cvgratnnlemseq  11323  mertenslemi1  11332  mertenslem2  11333  mertensabs  11334  clim2divap  11337  prodmodclem3  11372  prodmodclem2a  11373  efcllemp  11392  reefcl  11402  efcj  11407  efaddlem  11408  efexp  11416  reeftlcl  11423  eftlub  11424  efsep  11425  effsumlt  11426  eflegeo  11435  retanclap  11456  demoivre  11506  demoivreALT  11507  eirraplem  11510  dvdsval3  11524  iddvdsexp  11544  alzdvds  11579  addmodlteqALT  11584  nnehalf  11628  nno  11630  ndvdsadd  11655  divgcdnnr  11691  neggcd  11698  gcdabs  11703  bezoutlemmain  11713  bezoutlemaz  11718  bezoutlembz  11719  gcdmultiplez  11736  gcdzeq  11737  dvdssq  11746  algrf  11753  algcvg  11756  algcvga  11759  algfx  11760  eucalgf  11763  eucalgcvga  11766  neglcm  11783  lcmabs  11784  lcmdvds  11787  lcmgcdeq  11791  qredeq  11804  isprm3  11826  coprm  11849  prmrp  11850  isprm6  11852  prmdvdsexpb  11854  rpexp  11858  cncongrprm  11862  sqrt2irraplemnn  11884  phibndlem  11919  phiprmpw  11925  ennnfonelemrn  11959  topnidg  12163  tgss3  12277  clsval  12310  clsss3  12329  neiss2  12341  resttop  12369  resttopon2  12377  lmconst  12415  cnima  12419  cnntri  12423  cncnp  12429  cnrest  12434  cndis  12440  lmss  12445  lmff  12448  lmtopcnp  12449  txcnp  12470  upxp  12471  uptx  12473  cnmpt11  12482  hmeoima  12509  hmeoopn  12510  hmeocld  12511  hmeontr  12512  hmeoimaf1o  12513  mettri2  12561  met0  12563  metres2  12580  blpnf  12599  xblss2ps  12603  xblss2  12604  blbas  12632  blres  12633  xmetec  12636  mopnss  12649  xmstri2  12669  mstri2  12670  xmstri  12671  mstri  12672  xmstri3  12673  mstri3  12674  msrtri  12675  mopni3  12683  unimopn  12685  comet  12698  bdxmet  12700  climcncf  12770  dedekindeulemuub  12794  dedekindicclemuub  12803  dvfgg  12856  dvidlemap  12859  dvfre  12873  reeff1olem  12891  reeff1o  12893  sinperlem  12928  abssinper  12966  reexplog  12991  relogexp  12992  cxpexpnn  13016  cxprec  13030  abscxp  13034  bj-inex  13259  bj-nn0suc  13316  bj-nn0sucALT  13330  trilpolemeq1  13391  trilpolemlt1  13392  trirec0  13395
  Copyright terms: Public domain W3C validator