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  558  3adantl1  1137  3adantl2  1138  3adantl3  1139  syl3anl1  1264  syl3anl3  1266  syl3anl  1267  stoic3  1407  eupick  2078  csbiebt  3039  csbnestgf  3052  reuss2  3356  mpteq12  4011  otexg  4152  opelopabt  4184  sonr  4239  sotr  4240  issod  4241  so2nr  4243  so3nr  4244  ordelss  4301  onelon  4306  elrnmpt1s  4789  iota2  5114  funeu  5148  imadif  5203  fnbr  5225  feu  5305  f1ss  5334  f1ssres  5337  f1resf1  5338  dffo2  5349  foco  5355  foun  5386  fun11iun  5388  ffoss  5399  funbrfv  5460  fvco3  5492  fvopab6  5517  funfvbrb  5533  elpreima  5539  ffvelrn  5553  ffvelrnda  5555  dffo4  5568  fmptco  5586  fsn2  5594  fvconst2g  5634  fex  5647  funfvima  5649  f1elima  5674  f1ocnvfv1  5678  f1ocnvfv2  5679  cocan2  5689  foeqcnvco  5691  isocnv  5712  isores2  5714  isoini  5719  isoselem  5721  f1oiso  5727  f1ofveu  5762  eloprabga  5858  grprinvlem  5965  suppssof1  5999  ofco  6000  offveqb  6001  fnexALT  6011  f1dmex  6014  ot1stg  6050  ot2ndg  6051  ot3rdgg  6052  eqopi  6070  2ndrn  6081  fo2ndf  6124  smores3  6190  smores2  6191  smoel  6197  smoiso  6199  tfrlem1  6205  tfrlemisucaccv  6222  tfrlemibxssdm  6224  tfrlemiubacc  6227  tfr1onlemsucaccv  6238  tfr1onlembfn  6241  tfr1onlemubacc  6243  tfr1onlemaccex  6245  tfr1onlemres  6246  tfrcllemsucaccv  6251  tfrcllembfn  6254  tfrcllemubacc  6256  tfrcllemaccex  6258  tfrcllemres  6259  tfrcl  6261  frecrdg  6305  omv2  6361  nnasuc  6372  nnmsuc  6373  nnacom  6380  nnaass  6381  nnmass  6383  nntri1  6392  nndifsnid  6403  nnmordi  6412  swoer  6457  erth  6473  riinerm  6502  qliftlem  6507  ecovass  6538  ecoviass  6539  elmapssres  6567  fvixp  6597  f1domg  6652  endomtr  6684  xpsnen2g  6723  enen1  6734  enen2  6735  domen1  6736  domen2  6737  mapen  6740  mapxpen  6742  ssenen  6745  phplem1  6746  fidifsnid  6765  findcard  6782  findcard2  6783  findcard2s  6784  fieq0  6864  isotilem  6893  supisolem  6895  inflbti  6911  ordiso2  6920  djuex  6928  updjudhcoinlf  6965  updjudhcoinrg  6966  updjud  6967  ctssdccl  6996  enumctlemm  6999  finomni  7012  nnnninf  7023  pm54.43  7051  acfun  7068  ccfunen  7084  cc2lem  7086  cc3  7088  addclpi  7147  addasspig  7150  mulasspig  7152  addnidpig  7156  nnppipi  7163  ltanqi  7222  ltmnqi  7223  ltexnqq  7228  archnqq  7237  prarloclemarch2  7239  enq0sym  7252  enq0tr  7254  nqnq0pi  7258  nqnq0  7261  mulcanenq0ec  7265  addclnq0  7271  nqpnq0nq  7273  distrnq0  7279  addassnq0lemcl  7281  addassnq0  7282  prubl  7306  prarloclemlt  7313  genpdf  7328  genipv  7329  genpelvl  7332  genpelvu  7333  genpml  7337  genpmu  7338  genprndl  7341  genprndu  7342  genpassl  7344  genpassu  7345  genpassg  7346  addnqprl  7349  addnqpru  7350  addlocpr  7356  nqprm  7362  nqprl  7371  nqpru  7372  mulnqprl  7388  mulnqpru  7389  mullocprlem  7390  mullocpr  7391  addcomprg  7398  mulcomprg  7400  distrlem1prl  7402  distrlem1pru  7403  distrlem4prl  7404  distrlem4pru  7405  ltprordil  7409  1idprl  7410  1idpru  7411  ltpopr  7415  ltsopr  7416  ltaddpr  7417  ltexprlemm  7420  ltexprlemopl  7421  ltexprlemlol  7422  ltexprlemopu  7423  ltexprlemupu  7424  ltexprlemdisj  7426  ltexprlemloc  7427  ltexprlemfl  7429  ltexprlemrl  7430  ltexprlemfu  7431  ltexprlemru  7432  addcanprleml  7434  addcanprlemu  7435  prplnqu  7440  recexprlemloc  7451  recexprlem1ssl  7453  recexprlem1ssu  7454  recexprlemss1l  7455  recexprlemss1u  7456  aptiprleml  7459  aptiprlemu  7460  cauappcvgprlemloc  7472  cauappcvgprlemladdru  7476  cauappcvgprlemladdrl  7477  caucvgprlemloc  7495  caucvgprlemladdrl  7498  caucvgprprlemml  7514  caucvgprprlemloc  7523  00sr  7589  map2psrprg  7625  suplocsrlempr  7627  suplocsrlem  7628  adddir  7769  axsuploc  7849  eqle  7867  le2tri3i  7884  mul4  7906  muladd11  7907  cnegexlem3  7951  addsub12  7987  2addsub  7988  addsubeq4  7989  subadd4  8018  negcon1  8026  negdi2  8032  negsubdi2  8033  neg2sub  8034  renegcl  8035  muladd  8158  subdir  8160  gt0ne0  8201  ltnegcon1  8237  lenegcon1  8240  eqord1  8257  eqord2  8258  recexre  8352  ltmul1  8366  recexap  8426  div12ap  8466  p1le  8619  ltmul2  8626  gt0div  8640  ge0div  8641  zlem1lt  9122  nnaddm1cl  9127  zdceq  9138  gtndiv  9158  prime  9162  msqznn  9163  btwnz  9182  uzss  9358  eluzadd  9366  nn0pzuz  9394  supinfneg  9402  infsupneg  9403  divfnzn  9425  qnegcl  9440  qreccl  9446  xaddass  9664  xleadd1a  9668  xlesubadd  9678  elico2  9732  iccss  9736  iccsupr  9761  elfz5  9810  fznn  9881  difelfznle  9924  fzoaddel  9981  qdceq  10036  qbtwnxr  10047  flqbi2  10076  adddivflid  10077  fldivnn0  10080  divfl0  10081  flqmulnn0  10084  fldivnn0le  10088  fldiv4p1lem1div2  10090  ceiqle  10098  flqdiv  10106  modqmulnn  10127  frecuzrdgtcl  10197  frecuzrdgsuc  10199  frecuzrdgdomlem  10202  frecuzrdgfunlem  10204  frecuzrdgsuctlem  10208  seq3caopr2  10267  iseqf1olemkle  10269  seq3f1olemp  10287  seq3id  10293  seq3z  10296  expap0  10335  mulexp  10344  mulexpzap  10345  expmul  10350  leexp1a  10360  expubnd  10362  zesq  10422  bernneq  10424  bernneq3  10426  facdiv  10496  facndiv  10497  faclbnd3  10501  faclbnd6  10502  bccmpl  10512  bcpasc  10524  bccl  10525  seq3coll  10597  shftlem  10600  ovshftex  10603  shftval4  10612  shftf  10614  shftcan2  10619  crim  10642  mulreap  10648  remul2  10657  immul2  10664  cjexp  10677  caucvgre  10765  r19.2uz  10777  sqrtsq2  10827  absnid  10857  absexp  10863  nn0abscl  10869  abslt  10872  lenegsq  10879  cau3lem  10898  minmax  11013  xrmaxadd  11042  clim  11062  climshftlemg  11083  climcn1  11089  climcn1lem  11100  clim2ser  11118  clim2ser2  11119  iserex  11120  isermulc2  11121  climub  11125  climcaucn  11132  serf0  11133  summodclem3  11161  summodclem2a  11162  summodclem2  11163  summodc  11164  fsum3  11168  fsumf1o  11171  fisumss  11173  isumss2  11174  fsumcl2lem  11179  fsumadd  11187  fsumsplit  11188  isummulc2  11207  fsum2d  11216  fsummulc2  11229  telfsumo  11247  fsumparts  11251  hash2iun1dif1  11261  bcxmas  11270  isumshft  11271  isumsplit  11272  expcnvap0  11283  geolim  11292  geolim2  11293  cvgratnnlemmn  11306  cvgratnnlemseq  11307  mertenslemi1  11316  mertenslem2  11317  mertensabs  11318  clim2divap  11321  prodmodclem3  11356  prodmodclem2a  11357  efcllemp  11376  reefcl  11386  efcj  11391  efaddlem  11392  efexp  11400  reeftlcl  11407  eftlub  11408  efsep  11409  effsumlt  11410  eflegeo  11419  retanclap  11440  demoivre  11490  demoivreALT  11491  eirraplem  11494  dvdsval3  11508  iddvdsexp  11528  alzdvds  11563  addmodlteqALT  11568  nnehalf  11612  nno  11614  ndvdsadd  11639  divgcdnnr  11675  neggcd  11682  gcdabs  11687  bezoutlemmain  11697  bezoutlemaz  11702  bezoutlembz  11703  gcdmultiplez  11720  gcdzeq  11721  dvdssq  11730  algrf  11737  algcvg  11740  algcvga  11743  algfx  11744  eucalgf  11747  eucalgcvga  11750  neglcm  11767  lcmabs  11768  lcmdvds  11771  lcmgcdeq  11775  qredeq  11788  isprm3  11810  coprm  11833  prmrp  11834  isprm6  11836  prmdvdsexpb  11838  rpexp  11842  cncongrprm  11846  sqrt2irraplemnn  11868  phibndlem  11903  phiprmpw  11909  ennnfonelemrn  11943  topnidg  12147  tgss3  12261  clsval  12294  clsss3  12313  neiss2  12325  resttop  12353  resttopon2  12361  lmconst  12399  cnima  12403  cnntri  12407  cncnp  12413  cnrest  12418  cndis  12424  lmss  12429  lmff  12432  lmtopcnp  12433  txcnp  12454  upxp  12455  uptx  12457  cnmpt11  12466  hmeoima  12493  hmeoopn  12494  hmeocld  12495  hmeontr  12496  hmeoimaf1o  12497  mettri2  12545  met0  12547  metres2  12564  blpnf  12583  xblss2ps  12587  xblss2  12588  blbas  12616  blres  12617  xmetec  12620  mopnss  12633  xmstri2  12653  mstri2  12654  xmstri  12655  mstri  12656  xmstri3  12657  mstri3  12658  msrtri  12659  mopni3  12667  unimopn  12669  comet  12682  bdxmet  12684  climcncf  12754  dedekindeulemuub  12778  dedekindicclemuub  12787  dvfgg  12840  dvidlemap  12843  dvfre  12857  reeff1olem  12875  reeff1o  12877  sinperlem  12911  abssinper  12949  reexplog  12972  relogexp  12973  bj-inex  13164  bj-nn0suc  13221  bj-nn0sucALT  13235  trilpolemeq1  13294  trilpolemlt1  13295  trirec0  13298
  Copyright terms: Public domain W3C validator