ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylan GIF 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 (𝜑𝜓)
sylan.2 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
sylan ((𝜑𝜒) → 𝜃)

Proof of Theorem sylan
StepHypRef Expression
1 sylan.1 . 2 (𝜑𝜓)
2 sylan.2 . . 3 ((𝜓𝜒) → 𝜃)
32expcom 115 . 2 (𝜒 → (𝜓𝜃))
41, 3mpan9 279 1 ((𝜑𝜒) → 𝜃)
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  399  sylanl2  400  mpanl1  430  mpanl2  431  adantll  467  adantlr  468  ancom1s  543  3adantl1  1122  3adantl2  1123  3adantl3  1124  syl3anl1  1249  syl3anl3  1251  syl3anl  1252  stoic3  1392  eupick  2056  csbiebt  3009  csbnestgf  3022  reuss2  3326  mpteq12  3981  otexg  4122  opelopabt  4154  sonr  4209  sotr  4210  issod  4211  so2nr  4213  so3nr  4214  ordelss  4271  onelon  4276  elrnmpt1s  4759  iota2  5084  funeu  5118  imadif  5173  fnbr  5195  feu  5275  f1ss  5304  f1ssres  5307  f1resf1  5308  dffo2  5319  foco  5325  foun  5354  fun11iun  5356  ffoss  5367  funbrfv  5428  fvco3  5460  fvopab6  5485  funfvbrb  5501  elpreima  5507  ffvelrn  5521  ffvelrnda  5523  dffo4  5536  fmptco  5554  fsn2  5562  fvconst2g  5602  fex  5615  funfvima  5617  f1elima  5642  f1ocnvfv1  5646  f1ocnvfv2  5647  cocan2  5657  foeqcnvco  5659  isocnv  5680  isores2  5682  isoini  5687  isoselem  5689  f1oiso  5695  f1ofveu  5730  eloprabga  5826  grprinvlem  5933  suppssof1  5967  ofco  5968  offveqb  5969  fnexALT  5979  f1dmex  5982  ot1stg  6018  ot2ndg  6019  ot3rdgg  6020  eqopi  6038  2ndrn  6049  fo2ndf  6092  smores3  6158  smores2  6159  smoel  6165  smoiso  6167  tfrlem1  6173  tfrlemisucaccv  6190  tfrlemibxssdm  6192  tfrlemiubacc  6195  tfr1onlemsucaccv  6206  tfr1onlembfn  6209  tfr1onlemubacc  6211  tfr1onlemaccex  6213  tfr1onlemres  6214  tfrcllemsucaccv  6219  tfrcllembfn  6222  tfrcllemubacc  6224  tfrcllemaccex  6226  tfrcllemres  6227  tfrcl  6229  frecrdg  6273  omv2  6329  nnasuc  6340  nnmsuc  6341  nnacom  6348  nnaass  6349  nnmass  6351  nntri1  6360  nndifsnid  6371  nnmordi  6380  swoer  6425  erth  6441  riinerm  6470  qliftlem  6475  ecovass  6506  ecoviass  6507  elmapssres  6535  fvixp  6565  f1domg  6620  endomtr  6652  xpsnen2g  6691  enen1  6702  enen2  6703  domen1  6704  domen2  6705  mapen  6708  mapxpen  6710  ssenen  6713  phplem1  6714  fidifsnid  6733  findcard  6750  findcard2  6751  findcard2s  6752  fieq0  6832  isotilem  6861  supisolem  6863  inflbti  6879  ordiso2  6888  djuex  6896  updjudhcoinlf  6933  updjudhcoinrg  6934  updjud  6935  ctssdccl  6964  enumctlemm  6967  finomni  6980  nnnninf  6991  pm54.43  7014  acfun  7031  ccfunen  7047  addclpi  7103  addasspig  7106  mulasspig  7108  addnidpig  7112  nnppipi  7119  ltanqi  7178  ltmnqi  7179  ltexnqq  7184  archnqq  7193  prarloclemarch2  7195  enq0sym  7208  enq0tr  7210  nqnq0pi  7214  nqnq0  7217  mulcanenq0ec  7221  addclnq0  7227  nqpnq0nq  7229  distrnq0  7235  addassnq0lemcl  7237  addassnq0  7238  prubl  7262  prarloclemlt  7269  genpdf  7284  genipv  7285  genpelvl  7288  genpelvu  7289  genpml  7293  genpmu  7294  genprndl  7297  genprndu  7298  genpassl  7300  genpassu  7301  genpassg  7302  addnqprl  7305  addnqpru  7306  addlocpr  7312  nqprm  7318  nqprl  7327  nqpru  7328  mulnqprl  7344  mulnqpru  7345  mullocprlem  7346  mullocpr  7347  addcomprg  7354  mulcomprg  7356  distrlem1prl  7358  distrlem1pru  7359  distrlem4prl  7360  distrlem4pru  7361  ltprordil  7365  1idprl  7366  1idpru  7367  ltpopr  7371  ltsopr  7372  ltaddpr  7373  ltexprlemm  7376  ltexprlemopl  7377  ltexprlemlol  7378  ltexprlemopu  7379  ltexprlemupu  7380  ltexprlemdisj  7382  ltexprlemloc  7383  ltexprlemfl  7385  ltexprlemrl  7386  ltexprlemfu  7387  ltexprlemru  7388  addcanprleml  7390  addcanprlemu  7391  prplnqu  7396  recexprlemloc  7407  recexprlem1ssl  7409  recexprlem1ssu  7410  recexprlemss1l  7411  recexprlemss1u  7412  aptiprleml  7415  aptiprlemu  7416  cauappcvgprlemloc  7428  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  caucvgprlemloc  7451  caucvgprlemladdrl  7454  caucvgprprlemml  7470  caucvgprprlemloc  7479  00sr  7545  map2psrprg  7581  suplocsrlempr  7583  suplocsrlem  7584  adddir  7725  axsuploc  7805  eqle  7823  le2tri3i  7840  mul4  7862  muladd11  7863  cnegexlem3  7907  addsub12  7943  2addsub  7944  addsubeq4  7945  subadd4  7974  negcon1  7982  negdi2  7988  negsubdi2  7989  neg2sub  7990  renegcl  7991  muladd  8114  subdir  8116  gt0ne0  8157  ltnegcon1  8193  lenegcon1  8196  eqord1  8213  eqord2  8214  recexre  8307  ltmul1  8321  recexap  8381  div12ap  8421  p1le  8571  ltmul2  8578  gt0div  8592  ge0div  8593  zlem1lt  9068  nnaddm1cl  9073  zdceq  9084  gtndiv  9104  prime  9108  msqznn  9109  btwnz  9128  uzss  9302  eluzadd  9310  nn0pzuz  9338  supinfneg  9346  infsupneg  9347  divfnzn  9369  qnegcl  9384  qreccl  9390  xaddass  9607  xleadd1a  9611  xlesubadd  9621  elico2  9675  iccss  9679  iccsupr  9704  elfz5  9753  fznn  9824  difelfznle  9867  fzoaddel  9924  qdceq  9979  qbtwnxr  9990  flqbi2  10019  adddivflid  10020  fldivnn0  10023  divfl0  10024  flqmulnn0  10027  fldivnn0le  10031  fldiv4p1lem1div2  10033  ceiqle  10041  flqdiv  10049  modqmulnn  10070  frecuzrdgtcl  10140  frecuzrdgsuc  10142  frecuzrdgdomlem  10145  frecuzrdgfunlem  10147  frecuzrdgsuctlem  10151  seq3caopr2  10210  iseqf1olemkle  10212  seq3f1olemp  10230  seq3id  10236  seq3z  10239  expap0  10278  mulexp  10287  mulexpzap  10288  expmul  10293  leexp1a  10303  expubnd  10305  zesq  10365  bernneq  10367  bernneq3  10369  facdiv  10439  facndiv  10440  faclbnd3  10444  faclbnd6  10445  bccmpl  10455  bcpasc  10467  bccl  10468  seq3coll  10540  shftlem  10543  ovshftex  10546  shftval4  10555  shftf  10557  shftcan2  10562  crim  10585  mulreap  10591  remul2  10600  immul2  10607  cjexp  10620  caucvgre  10708  r19.2uz  10720  sqrtsq2  10770  absnid  10800  absexp  10806  nn0abscl  10812  abslt  10815  lenegsq  10822  cau3lem  10841  minmax  10956  xrmaxadd  10985  clim  11005  climshftlemg  11026  climcn1  11032  climcn1lem  11043  clim2ser  11061  clim2ser2  11062  iserex  11063  isermulc2  11064  climub  11068  climcaucn  11075  serf0  11076  summodclem3  11104  summodclem2a  11105  summodclem2  11106  summodc  11107  fsum3  11111  fsumf1o  11114  fisumss  11116  isumss2  11117  fsumcl2lem  11122  fsumadd  11130  fsumsplit  11131  isummulc2  11150  fsum2d  11159  fsummulc2  11172  telfsumo  11190  fsumparts  11194  hash2iun1dif1  11204  bcxmas  11213  isumshft  11214  isumsplit  11215  expcnvap0  11226  geolim  11235  geolim2  11236  cvgratnnlemmn  11249  cvgratnnlemseq  11250  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  efcllemp  11278  reefcl  11288  efcj  11293  efaddlem  11294  efexp  11302  reeftlcl  11309  eftlub  11310  efsep  11311  effsumlt  11312  eflegeo  11322  retanclap  11343  demoivre  11393  demoivreALT  11394  eirraplem  11395  dvdsval3  11409  iddvdsexp  11429  alzdvds  11464  addmodlteqALT  11469  nnehalf  11513  nno  11515  ndvdsadd  11540  divgcdnnr  11576  neggcd  11583  gcdabs  11588  bezoutlemmain  11598  bezoutlemaz  11603  bezoutlembz  11604  gcdmultiplez  11621  gcdzeq  11622  dvdssq  11631  algrf  11638  algcvg  11641  algcvga  11644  algfx  11645  eucalgf  11648  eucalgcvga  11651  neglcm  11668  lcmabs  11669  lcmdvds  11672  lcmgcdeq  11676  qredeq  11689  isprm3  11711  coprm  11734  prmrp  11735  isprm6  11737  prmdvdsexpb  11739  rpexp  11743  cncongrprm  11747  sqrt2irraplemnn  11768  phibndlem  11803  phiprmpw  11809  ennnfonelemrn  11843  topnidg  12044  tgss3  12158  clsval  12191  clsss3  12210  neiss2  12222  resttop  12250  resttopon2  12258  lmconst  12296  cnima  12300  cnntri  12304  cncnp  12310  cnrest  12315  cndis  12321  lmss  12326  lmff  12329  lmtopcnp  12330  txcnp  12351  upxp  12352  uptx  12354  cnmpt11  12363  hmeoima  12390  hmeoopn  12391  hmeocld  12392  hmeontr  12393  hmeoimaf1o  12394  mettri2  12442  met0  12444  metres2  12461  blpnf  12480  xblss2ps  12484  xblss2  12485  blbas  12513  blres  12514  xmetec  12517  mopnss  12530  xmstri2  12550  mstri2  12551  xmstri  12552  mstri  12553  xmstri3  12554  mstri3  12555  msrtri  12556  mopni3  12564  unimopn  12566  comet  12579  bdxmet  12581  climcncf  12651  dedekindeulemuub  12675  dedekindicclemuub  12684  dvfgg  12737  dvidlemap  12740  dvfre  12754  sinperlem  12800  bj-inex  13001  bj-nn0suc  13058  bj-nn0sucALT  13072  trilpolemeq1  13129  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator