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

Theorem sylan 279
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 277 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  sylanb  280  sylanbr  281  syl2an  285  sylanl1  397  sylanl2  398  mpanl1  428  mpanl2  429  adantll  463  adantlr  464  ancom1s  539  3adantl1  1105  3adantl2  1106  3adantl3  1107  syl3anl1  1232  syl3anl3  1234  syl3anl  1235  stoic3  1375  eupick  2039  csbiebt  2989  csbnestgf  3002  reuss2  3303  mpteq12  3951  otexg  4090  opelopabt  4122  sonr  4177  sotr  4178  issod  4179  so2nr  4181  so3nr  4182  ordelss  4239  onelon  4244  elrnmpt1s  4727  iota2  5050  funeu  5084  imadif  5139  fnbr  5161  feu  5241  f1ss  5270  f1ssres  5273  f1resf1  5274  dffo2  5285  foco  5291  foun  5320  fun11iun  5322  ffoss  5333  funbrfv  5392  fvco3  5424  fvopab6  5449  funfvbrb  5465  elpreima  5471  ffvelrn  5485  ffvelrnda  5487  dffo4  5500  fmptco  5518  fsn2  5526  fvconst2g  5566  fex  5579  funfvima  5581  f1elima  5606  f1ocnvfv1  5610  f1ocnvfv2  5611  cocan2  5621  foeqcnvco  5623  isocnv  5644  isores2  5646  isoini  5651  isoselem  5653  f1oiso  5659  f1ofveu  5694  eloprabga  5790  grprinvlem  5897  suppssof1  5930  ofco  5931  offveqb  5932  fnexALT  5942  f1dmex  5945  ot1stg  5981  ot2ndg  5982  ot3rdgg  5983  eqopi  6000  2ndrn  6011  fo2ndf  6054  smores3  6120  smores2  6121  smoel  6127  smoiso  6129  tfrlem1  6135  tfrlemisucaccv  6152  tfrlemibxssdm  6154  tfrlemiubacc  6157  tfr1onlemsucaccv  6168  tfr1onlembfn  6171  tfr1onlemubacc  6173  tfr1onlemaccex  6175  tfr1onlemres  6176  tfrcllemsucaccv  6181  tfrcllembfn  6184  tfrcllemubacc  6186  tfrcllemaccex  6188  tfrcllemres  6189  tfrcl  6191  frecrdg  6235  omv2  6291  nnasuc  6302  nnmsuc  6303  nnacom  6310  nnaass  6311  nnmass  6313  nntri1  6322  nndifsnid  6333  nnmordi  6342  swoer  6387  erth  6403  riinerm  6432  qliftlem  6437  ecovass  6468  ecoviass  6469  elmapssres  6497  fvixp  6527  f1domg  6582  endomtr  6614  xpsnen2g  6652  enen1  6663  enen2  6664  domen1  6665  domen2  6666  mapen  6669  mapxpen  6671  ssenen  6674  phplem1  6675  fidifsnid  6694  findcard  6711  findcard2  6712  findcard2s  6713  isotilem  6808  supisolem  6810  inflbti  6826  ordiso2  6835  djuex  6843  updjudhcoinlf  6880  updjudhcoinrg  6881  updjud  6882  enumctlemm  6913  finomni  6924  nnnninf  6935  pm54.43  6957  addclpi  7036  addasspig  7039  mulasspig  7041  addnidpig  7045  nnppipi  7052  ltanqi  7111  ltmnqi  7112  ltexnqq  7117  archnqq  7126  prarloclemarch2  7128  enq0sym  7141  enq0tr  7143  nqnq0pi  7147  nqnq0  7150  mulcanenq0ec  7154  addclnq0  7160  nqpnq0nq  7162  distrnq0  7168  addassnq0lemcl  7170  addassnq0  7171  prubl  7195  prarloclemlt  7202  genpdf  7217  genipv  7218  genpelvl  7221  genpelvu  7222  genpml  7226  genpmu  7227  genprndl  7230  genprndu  7231  genpassl  7233  genpassu  7234  genpassg  7235  addnqprl  7238  addnqpru  7239  addlocpr  7245  nqprm  7251  nqprl  7260  nqpru  7261  mulnqprl  7277  mulnqpru  7278  mullocprlem  7279  mullocpr  7280  addcomprg  7287  mulcomprg  7289  distrlem1prl  7291  distrlem1pru  7292  distrlem4prl  7293  distrlem4pru  7294  ltprordil  7298  1idprl  7299  1idpru  7300  ltpopr  7304  ltsopr  7305  ltaddpr  7306  ltexprlemm  7309  ltexprlemopl  7310  ltexprlemlol  7311  ltexprlemopu  7312  ltexprlemupu  7313  ltexprlemdisj  7315  ltexprlemloc  7316  ltexprlemfl  7318  ltexprlemrl  7319  ltexprlemfu  7320  ltexprlemru  7321  addcanprleml  7323  addcanprlemu  7324  prplnqu  7329  recexprlemloc  7340  recexprlem1ssl  7342  recexprlem1ssu  7343  recexprlemss1l  7344  recexprlemss1u  7345  aptiprleml  7348  aptiprlemu  7349  cauappcvgprlemloc  7361  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  caucvgprlemloc  7384  caucvgprlemladdrl  7387  caucvgprprlemml  7403  caucvgprprlemloc  7412  00sr  7465  adddir  7629  eqle  7726  le2tri3i  7743  mul4  7765  muladd11  7766  cnegexlem3  7810  addsub12  7846  2addsub  7847  addsubeq4  7848  subadd4  7877  negcon1  7885  negdi2  7891  negsubdi2  7892  neg2sub  7893  renegcl  7894  muladd  8013  subdir  8015  gt0ne0  8056  ltnegcon1  8092  lenegcon1  8095  eqord1  8112  eqord2  8113  recexre  8206  ltmul1  8220  recexap  8275  div12ap  8315  p1le  8465  ltmul2  8472  gt0div  8486  ge0div  8487  zlem1lt  8962  nnaddm1cl  8967  zdceq  8978  gtndiv  8998  prime  9002  msqznn  9003  btwnz  9022  uzss  9196  eluzadd  9204  nn0pzuz  9232  supinfneg  9240  infsupneg  9241  divfnzn  9263  qnegcl  9278  qreccl  9284  xaddass  9493  xleadd1a  9497  xlesubadd  9507  elico2  9561  iccss  9565  iccsupr  9590  elfz5  9639  fznn  9710  difelfznle  9753  fzoaddel  9810  qdceq  9865  qbtwnxr  9876  flqbi2  9905  adddivflid  9906  fldivnn0  9909  divfl0  9910  flqmulnn0  9913  fldivnn0le  9917  fldiv4p1lem1div2  9919  ceiqle  9927  flqdiv  9935  modqmulnn  9956  frecuzrdgtcl  10026  frecuzrdgsuc  10028  frecuzrdgdomlem  10031  frecuzrdgfunlem  10033  frecuzrdgsuctlem  10037  seq3caopr2  10096  iseqf1olemkle  10098  seq3f1olemp  10116  seq3id  10122  seq3z  10125  expap0  10164  mulexp  10173  mulexpzap  10174  expmul  10179  leexp1a  10189  expubnd  10191  zesq  10251  bernneq  10253  bernneq3  10255  facdiv  10325  facndiv  10326  faclbnd3  10330  faclbnd6  10331  bccmpl  10341  bcpasc  10353  bccl  10354  seq3coll  10426  shftlem  10429  ovshftex  10432  shftval4  10441  shftf  10443  shftcan2  10448  crim  10471  mulreap  10477  remul2  10486  immul2  10493  cjexp  10506  caucvgre  10593  r19.2uz  10605  sqrtsq2  10655  absnid  10685  absexp  10691  nn0abscl  10697  abslt  10700  lenegsq  10707  cau3lem  10726  minmax  10840  xrmaxadd  10869  clim  10889  climshftlemg  10910  climcn1  10916  climcn1lem  10927  clim2ser  10945  clim2ser2  10946  iserex  10947  isermulc2  10948  climub  10952  climcaucn  10959  serf0  10960  summodclem3  10988  summodclem2a  10989  summodclem2  10990  summodc  10991  fsum3  10995  fsumf1o  10998  fisumss  11000  isumss2  11001  fsumcl2lem  11006  fsumadd  11014  fsumsplit  11015  isummulc2  11034  fsum2d  11043  fsummulc2  11056  telfsumo  11074  fsumparts  11078  hash2iun1dif1  11088  bcxmas  11097  isumshft  11098  isumsplit  11099  expcnvap0  11110  geolim  11119  geolim2  11120  cvgratnnlemmn  11133  cvgratnnlemseq  11134  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  efcllemp  11162  reefcl  11172  efcj  11177  efaddlem  11178  efexp  11186  reeftlcl  11193  eftlub  11194  efsep  11195  effsumlt  11196  eflegeo  11206  retanclap  11227  demoivre  11276  demoivreALT  11277  eirraplem  11278  dvdsval3  11292  iddvdsexp  11312  alzdvds  11347  addmodlteqALT  11352  nnehalf  11396  nno  11398  ndvdsadd  11423  divgcdnnr  11459  neggcd  11466  gcdabs  11471  bezoutlemmain  11479  bezoutlemaz  11484  bezoutlembz  11485  gcdmultiplez  11502  gcdzeq  11503  dvdssq  11512  algrf  11519  algcvg  11522  algcvga  11525  algfx  11526  eucalgf  11529  eucalgcvga  11532  neglcm  11549  lcmabs  11550  lcmdvds  11553  lcmgcdeq  11557  qredeq  11570  isprm3  11592  coprm  11615  prmrp  11616  isprm6  11618  prmdvdsexpb  11620  rpexp  11624  cncongrprm  11628  sqrt2irraplemnn  11649  phibndlem  11684  phiprmpw  11690  ennnfonelemrn  11724  topnidg  11915  tgss3  12029  clsval  12062  clsss3  12081  neiss2  12093  resttop  12121  resttopon2  12129  lmconst  12166  cnima  12170  cnntri  12174  cncnp  12180  cnrest  12185  cndis  12191  lmss  12196  lmff  12199  lmtopcnp  12200  txcnp  12221  upxp  12222  uptx  12224  cnmpt11  12233  mettri2  12290  met0  12292  metres2  12309  blpnf  12328  xblss2ps  12332  xblss2  12333  blbas  12361  blres  12362  xmetec  12365  mopnss  12378  xmstri2  12398  mstri2  12399  xmstri  12400  mstri  12401  xmstri3  12402  mstri3  12403  msrtri  12404  mopni3  12412  unimopn  12414  comet  12427  bdxmet  12429  climcncf  12484  dvfgg  12530  dvidlemap  12533  bj-inex  12686  bj-nn0suc  12747  bj-nn0sucALT  12761  trilpolemeq1  12817  trilpolemlt1  12818
  Copyright terms: Public domain W3C validator