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

Theorem sylan2 274
Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
Hypotheses
Ref Expression
sylan2.1 (𝜑𝜒)
sylan2.2 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
sylan2 ((𝜓𝜑) → 𝜃)

Proof of Theorem sylan2
StepHypRef Expression
1 sylan2.1 . . 3 (𝜑𝜒)
21adantl 266 . 2 ((𝜓𝜑) → 𝜒)
3 sylan2.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3syldan 270 1 ((𝜓𝜑) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  sylan2b  275  sylan2br  276  syl2an  277  sylanr1  390  sylanr2  391  mpanr2  422  adantrl  455  adantrr  456  ancom2s  508  3adantr1  1074  3adantr2  1075  3adantr3  1076  syl3anr1  1198  syl3anr3  1200  dfbi3dc  1304  xordidc  1306  elabgt  2706  sbciegft  2815  csbtt  2889  csbnestgf  2925  copsex2t  4009  pofun  4076  onsucmin  4260  onsucelsucr  4261  onsucsssucr  4262  ordsucunielexmid  4283  ordsuc  4314  nlimsucg  4317  elnn  4355  xpsspw  4477  elxp4  4835  elxp5  4836  funimass2  5004  imain  5008  funimaexg  5010  dff1o2  5158  resdif  5175  funbrfv  5239  fvelimab  5256  eqfnfv2  5293  fvimacnvi  5308  ffvresb  5355  fnressn  5376  fmptapd  5381  fnex  5410  rexima  5421  ralima  5422  f1elima  5439  fnotovb  5575  mpt2eq12  5592  fovrn  5670  fnovrn  5675  ofrfval  5747  fnofval  5748  cofunexg  5765  cofunex2g  5766  mpt2exxg  5860  mpt2exg  5861  f1o2ndf1  5876  spc2ed  5881  smodm2  5940  tfrlem9  5965  tfrlemibxssdm  5971  tfri3  5983  rdgtfr  5991  rdgruledefgg  5992  frecsuclem1  6017  oav2  6073  oasuc  6074  omv2  6075  onasuc  6076  omsuc  6081  onmsuc  6082  nnaass  6094  nndi  6095  nndir  6099  nnaword  6114  ecelqsg  6189  iinerm  6208  ecovass  6245  ecoviass  6246  ecovdi  6247  ecovidi  6248  domentr  6301  xpdom1g  6337  fopwdom  6340  phplem3  6347  phplem4  6348  php5dom  6355  ssfiexmid  6366  diffitest  6374  addclpi  6482  addasspig  6485  mulasspig  6487  distrpig  6488  mulcanpig  6490  nnppipi  6498  enqdc1  6517  addassnqg  6537  ltbtwnnqq  6570  prarloclemarch  6573  prarloclemarch2  6574  enq0sym  6587  enq0ref  6588  addclnq0  6606  nqpnq0nq  6608  nnanq0  6613  distrnq0  6614  addassnq0lemcl  6616  addassnq0  6617  distnq0r  6618  prarloclemlt  6648  genpassl  6679  genpassu  6680  genpassg  6681  nqpru  6707  addcomprg  6733  mulcomprg  6735  distrlem1prl  6737  distrlem1pru  6738  1idprl  6745  1idpru  6746  recexprlemdisj  6785  recexprlem1ssl  6788  peano2nnnn  6986  ax1rid  7008  axcaucvglemcl  7026  le2tri3i  7184  add4  7234  cnegexlem1  7248  cnegexlem3  7250  cnegex  7251  subadd  7276  addsub  7284  addsubeq4  7288  negdi  7330  renegcl  7334  resubcl  7337  subdi  7453  mulneg2  7464  mul2neg  7466  submul2  7467  ltnegcon2  7532  lenegcon2  7535  lesub0  7547  cru  7666  recextlem1  7705  recexap  7707  div12ap  7746  divnegap  7756  letrp1  7888  peano2nn  8001  nndivre  8024  nnsub  8027  nndivtr  8030  arch  8235  bndndx  8237  nn0addge1  8284  nn0addge2  8285  zaddcl  8341  zsubcl  8342  zltnle  8347  zrevaddcl  8351  nzadd  8353  zleltp1  8356  zltlem1  8358  zdiv  8385  peano2uz2  8403  uzind  8407  eluzp1l  8592  ublbneg  8644  qaddcl  8666  qsubcl  8669  qreccl  8673  qdivcl  8674  qrevaddcl  8675  irradd  8677  irrmul  8678  rerpdivcl  8710  nn0ledivnn  8784  xrre  8833  elioc2  8905  icoshft  8958  iccdil  8966  fzss2  9028  fzsuc2  9042  fzrev2  9048  elfzm11  9054  elfzp1b  9060  fzrevral  9068  fzshftral  9071  fzof  9102  fzoval  9106  fzon  9123  fzosubel  9151  zpnn0elfzo  9164  elfzom1b  9186  qltnle  9202  flqlt  9232  flqbi  9239  flqaddz  9246  fzofig  9371  iseqfeq2  9392  iseqfeq  9394  iseqsplit  9401  expp1  9426  expm1t  9447  expeq0  9450  binom2sub  9530  bernneq  9536  expnlbnd  9540  faccl  9602  facdiv  9605  bcpasc  9633  bccl  9634  2shfti  9659  crim  9685  mulreap  9691  resub  9697  imsub  9705  ipcnval  9713  cjsub  9719  resqrexlemfp1  9835  resqrexlemgt0  9846  sqabsadd  9881  sqabssub  9882  abs2dif2  9933  cau3lem  9940  icodiamlt  10006  clim  10032  clim2  10034  clim2c  10035  clim0c  10037  2clim  10052  climabs0  10058  climcn1  10059  climcn2  10060  climsqz  10085  climsqz2  10086  climub  10094  climserile  10095  moddvds  10116  0dvds  10127  iddvdsexp  10130  dvdssub  10151  dvdsle  10155  dvdsleabs  10156  dvdseq  10159  dvdsflip  10162  mulsucdiv2z  10196  bj-inex  10393  peano5set  10430  findset  10436  bj-findis  10470
  Copyright terms: Public domain W3C validator