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  8308  ltmul1  8322  recexap  8382  div12ap  8422  p1le  8575  ltmul2  8582  gt0div  8596  ge0div  8597  zlem1lt  9078  nnaddm1cl  9083  zdceq  9094  gtndiv  9114  prime  9118  msqznn  9119  btwnz  9138  uzss  9314  eluzadd  9322  nn0pzuz  9350  supinfneg  9358  infsupneg  9359  divfnzn  9381  qnegcl  9396  qreccl  9402  xaddass  9620  xleadd1a  9624  xlesubadd  9634  elico2  9688  iccss  9692  iccsupr  9717  elfz5  9766  fznn  9837  difelfznle  9880  fzoaddel  9937  qdceq  9992  qbtwnxr  10003  flqbi2  10032  adddivflid  10033  fldivnn0  10036  divfl0  10037  flqmulnn0  10040  fldivnn0le  10044  fldiv4p1lem1div2  10046  ceiqle  10054  flqdiv  10062  modqmulnn  10083  frecuzrdgtcl  10153  frecuzrdgsuc  10155  frecuzrdgdomlem  10158  frecuzrdgfunlem  10160  frecuzrdgsuctlem  10164  seq3caopr2  10223  iseqf1olemkle  10225  seq3f1olemp  10243  seq3id  10249  seq3z  10252  expap0  10291  mulexp  10300  mulexpzap  10301  expmul  10306  leexp1a  10316  expubnd  10318  zesq  10378  bernneq  10380  bernneq3  10382  facdiv  10452  facndiv  10453  faclbnd3  10457  faclbnd6  10458  bccmpl  10468  bcpasc  10480  bccl  10481  seq3coll  10553  shftlem  10556  ovshftex  10559  shftval4  10568  shftf  10570  shftcan2  10575  crim  10598  mulreap  10604  remul2  10613  immul2  10620  cjexp  10633  caucvgre  10721  r19.2uz  10733  sqrtsq2  10783  absnid  10813  absexp  10819  nn0abscl  10825  abslt  10828  lenegsq  10835  cau3lem  10854  minmax  10969  xrmaxadd  10998  clim  11018  climshftlemg  11039  climcn1  11045  climcn1lem  11056  clim2ser  11074  clim2ser2  11075  iserex  11076  isermulc2  11077  climub  11081  climcaucn  11088  serf0  11089  summodclem3  11117  summodclem2a  11118  summodclem2  11119  summodc  11120  fsum3  11124  fsumf1o  11127  fisumss  11129  isumss2  11130  fsumcl2lem  11135  fsumadd  11143  fsumsplit  11144  isummulc2  11163  fsum2d  11172  fsummulc2  11185  telfsumo  11203  fsumparts  11207  hash2iun1dif1  11217  bcxmas  11226  isumshft  11227  isumsplit  11228  expcnvap0  11239  geolim  11248  geolim2  11249  cvgratnnlemmn  11262  cvgratnnlemseq  11263  mertenslemi1  11272  mertenslem2  11273  mertensabs  11274  efcllemp  11291  reefcl  11301  efcj  11306  efaddlem  11307  efexp  11315  reeftlcl  11322  eftlub  11323  efsep  11324  effsumlt  11325  eflegeo  11335  retanclap  11356  demoivre  11406  demoivreALT  11407  eirraplem  11410  dvdsval3  11424  iddvdsexp  11444  alzdvds  11479  addmodlteqALT  11484  nnehalf  11528  nno  11530  ndvdsadd  11555  divgcdnnr  11591  neggcd  11598  gcdabs  11603  bezoutlemmain  11613  bezoutlemaz  11618  bezoutlembz  11619  gcdmultiplez  11636  gcdzeq  11637  dvdssq  11646  algrf  11653  algcvg  11656  algcvga  11659  algfx  11660  eucalgf  11663  eucalgcvga  11666  neglcm  11683  lcmabs  11684  lcmdvds  11687  lcmgcdeq  11691  qredeq  11704  isprm3  11726  coprm  11749  prmrp  11750  isprm6  11752  prmdvdsexpb  11754  rpexp  11758  cncongrprm  11762  sqrt2irraplemnn  11784  phibndlem  11819  phiprmpw  11825  ennnfonelemrn  11859  topnidg  12060  tgss3  12174  clsval  12207  clsss3  12226  neiss2  12238  resttop  12266  resttopon2  12274  lmconst  12312  cnima  12316  cnntri  12320  cncnp  12326  cnrest  12331  cndis  12337  lmss  12342  lmff  12345  lmtopcnp  12346  txcnp  12367  upxp  12368  uptx  12370  cnmpt11  12379  hmeoima  12406  hmeoopn  12407  hmeocld  12408  hmeontr  12409  hmeoimaf1o  12410  mettri2  12458  met0  12460  metres2  12477  blpnf  12496  xblss2ps  12500  xblss2  12501  blbas  12529  blres  12530  xmetec  12533  mopnss  12546  xmstri2  12566  mstri2  12567  xmstri  12568  mstri  12569  xmstri3  12570  mstri3  12571  msrtri  12572  mopni3  12580  unimopn  12582  comet  12595  bdxmet  12597  climcncf  12667  dedekindeulemuub  12691  dedekindicclemuub  12700  dvfgg  12753  dvidlemap  12756  dvfre  12770  sinperlem  12816  abssinper  12854  bj-inex  13032  bj-nn0suc  13089  bj-nn0sucALT  13103  trilpolemeq1  13160  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator