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

Theorem sylan 277
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 114 . 2 (𝜒 → (𝜓𝜃))
41, 3mpan9 275 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  sylanb  278  sylanbr  279  syl2an  283  sylanl1  394  sylanl2  395  mpanl1  425  mpanl2  426  adantll  460  adantlr  461  ancom1s  534  3adantl1  1095  3adantl2  1096  3adantl3  1097  syl3anl1  1218  syl3anl3  1220  syl3anl  1221  stoic3  1361  eupick  2021  csbiebt  2943  csbnestgf  2955  reuss2  3251  mpteq12  3869  otexg  3993  opelopabt  4025  sonr  4080  sotr  4081  issod  4082  so2nr  4084  so3nr  4085  ordelss  4142  onelon  4147  elrnmpt1s  4612  iota2  4923  funeu  4956  imadif  5010  fnbr  5032  feu  5103  f1ss  5128  f1ssres  5130  dffo2  5141  foco  5147  foun  5176  fun11iun  5178  ffoss  5189  funbrfv  5244  fvco3  5276  fvopab6  5296  funfvbrb  5312  elpreima  5318  ffvelrn  5332  ffvelrnda  5334  dffo4  5347  foelrn  5349  fmptco  5362  fsn2  5369  fvconst2g  5407  fex  5420  funfvima  5422  f1elima  5444  f1ocnvfv1  5448  f1ocnvfv2  5449  cocan2  5459  foeqcnvco  5461  isocnv  5482  isores2  5484  isoini  5488  isoselem  5490  f1oiso  5496  f1ofveu  5531  eloprabga  5622  grprinvlem  5726  suppssof1  5759  ofco  5760  offveqb  5761  fnexALT  5771  f1dmex  5774  ot1stg  5810  ot2ndg  5811  ot3rdgg  5812  eqopi  5829  2ndrn  5840  fo2ndf  5879  smores3  5942  smores2  5943  smoel  5949  smoiso  5951  tfrlem1  5957  tfrlemisucaccv  5974  tfrlemibxssdm  5976  tfrlemiubacc  5979  tfr1onlemsucaccv  5990  tfr1onlembfn  5993  tfr1onlemubacc  5995  tfr1onlemaccex  5997  tfr1onlemres  5998  tfrcllemsucaccv  6003  tfrcllembfn  6006  tfrcllemubacc  6008  tfrcllemaccex  6010  tfrcllemres  6011  tfrcl  6013  frecrdg  6057  omv2  6109  nnasuc  6120  nnmsuc  6121  nnacom  6128  nnaass  6129  nnmass  6131  nntri1  6140  nnmordi  6155  swoer  6200  erth  6216  riinerm  6245  qliftlem  6250  ecovass  6281  ecoviass  6282  f1domg  6305  endomtr  6337  xpsnen2g  6373  enen1  6381  enen2  6382  domen1  6383  domen2  6384  phplem1  6387  findcard  6422  findcard2  6423  findcard2s  6424  isotilem  6478  supisolem  6480  inflbti  6496  ordiso2  6505  pm54.43  6518  addclpi  6579  addasspig  6582  mulasspig  6584  addnidpig  6588  nnppipi  6595  ltanqi  6654  ltmnqi  6655  ltexnqq  6660  archnqq  6669  prarloclemarch2  6671  enq0sym  6684  enq0tr  6686  nqnq0pi  6690  nqnq0  6693  mulcanenq0ec  6697  addclnq0  6703  nqpnq0nq  6705  distrnq0  6711  addassnq0lemcl  6713  addassnq0  6714  prubl  6738  prarloclemlt  6745  genpdf  6760  genipv  6761  genpelvl  6764  genpelvu  6765  genpml  6769  genpmu  6770  genprndl  6773  genprndu  6774  genpassl  6776  genpassu  6777  genpassg  6778  addnqprl  6781  addnqpru  6782  addlocpr  6788  nqprm  6794  nqprl  6803  nqpru  6804  mulnqprl  6820  mulnqpru  6821  mullocprlem  6822  mullocpr  6823  addcomprg  6830  mulcomprg  6832  distrlem1prl  6834  distrlem1pru  6835  distrlem4prl  6836  distrlem4pru  6837  ltprordil  6841  1idprl  6842  1idpru  6843  ltpopr  6847  ltsopr  6848  ltaddpr  6849  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemlol  6854  ltexprlemopu  6855  ltexprlemupu  6856  ltexprlemdisj  6858  ltexprlemloc  6859  ltexprlemfl  6861  ltexprlemrl  6862  ltexprlemfu  6863  ltexprlemru  6864  addcanprleml  6866  addcanprlemu  6867  prplnqu  6872  recexprlemloc  6883  recexprlem1ssl  6885  recexprlem1ssu  6886  recexprlemss1l  6887  recexprlemss1u  6888  aptiprleml  6891  aptiprlemu  6892  cauappcvgprlemloc  6904  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  caucvgprlemloc  6927  caucvgprlemladdrl  6930  caucvgprprlemml  6946  caucvgprprlemloc  6955  00sr  7008  adddir  7172  eqle  7269  le2tri3i  7286  mul4  7307  muladd11  7308  cnegexlem3  7352  addsub12  7388  2addsub  7389  addsubeq4  7390  subadd4  7419  negcon1  7427  negdi2  7433  negsubdi2  7434  neg2sub  7435  renegcl  7436  muladd  7555  subdir  7557  gt0ne0  7598  ltnegcon1  7634  lenegcon1  7637  recexre  7745  ltmul1  7759  recexap  7810  div12ap  7849  p1le  7994  ltmul2  8001  gt0div  8015  ge0div  8016  zlem1lt  8488  nnaddm1cl  8493  zdceq  8504  gtndiv  8523  prime  8527  msqznn  8528  btwnz  8547  uzss  8720  eluzadd  8728  nn0pzuz  8756  supinfneg  8764  infsupneg  8765  divfnzn  8787  qnegcl  8802  qreccl  8808  elico2  9036  iccss  9040  iccsupr  9065  elfz5  9113  fznn  9182  difelfznle  9223  fzoaddel  9278  qdceq  9333  qbtwnxr  9344  flqbi2  9373  adddivflid  9374  fldivnn0  9377  divfl0  9378  flqmulnn0  9381  fldivnn0le  9385  fldiv4p1lem1div2  9387  ceiqle  9395  flqdiv  9403  modqmulnn  9424  frecuzrdgtcl  9494  frecuzrdgsuc  9496  frecuzrdgdomlem  9499  frecuzrdgfunlem  9501  frecuzrdgsuctlem  9505  iseqsplit  9554  iseqcaopr2  9557  iseqid  9563  iseqz  9566  expap0  9603  mulexp  9612  mulexpzap  9613  expmul  9618  leexp1a  9628  expubnd  9630  zesq  9688  bernneq  9690  bernneq3  9692  facdiv  9762  facndiv  9763  faclbnd3  9767  faclbnd6  9768  bccmpl  9778  bcpasc  9790  bccl  9791  shftlem  9842  ovshftex  9845  shftval4  9854  shftf  9856  shftcan2  9861  crim  9883  mulreap  9889  remul2  9898  immul2  9905  cjexp  9918  caucvgre  10005  r19.2uz  10017  sqrtsq2  10067  absnid  10097  absexp  10103  nn0abscl  10109  abslt  10112  lenegsq  10119  cau3lem  10138  minmax  10250  clim  10258  climshftlemg  10279  climcn1  10285  climcn1lem  10295  clim2iser  10313  clim2iser2  10314  iiserex  10315  iisermulc2  10316  climub  10320  climcaucn  10326  serif0  10327  dvdsval3  10344  iddvdsexp  10364  alzdvds  10399  addmodlteqALT  10404  nnehalf  10448  nno  10450  ndvdsadd  10475  divgcdnnr  10511  neggcd  10518  gcdabs  10523  bezoutlemmain  10531  bezoutlemaz  10536  bezoutlembz  10537  gcdmultiplez  10554  gcdzeq  10555  dvdssq  10564  ialgcvg  10574  ialgcvga  10577  ialgfx  10578  eucalgf  10581  eucialgcvga  10584  neglcm  10601  lcmabs  10602  lcmdvds  10605  lcmgcdeq  10609  qredeq  10622  isprm3  10644  coprm  10667  prmrp  10668  isprm6  10670  prmdvdsexpb  10672  rpexp  10676  cncongrprm  10680  sqrt2irraplemnn  10701  bj-inex  10856  bj-nn0suc  10917  bj-nn0sucALT  10931
  Copyright terms: Public domain W3C validator