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

Theorem sylan2 284
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 275 . 2 ((𝜓𝜑) → 𝜒)
3 sylan2.2 . 2 ((𝜓𝜒) → 𝜃)
42, 3syldan 280 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:  sylan2b  285  sylan2br  286  syl2an  287  sylanr1  401  sylanr2  402  mpanr2  434  adantrl  469  adantrr  470  ancom2s  555  3adantr1  1140  3adantr2  1141  3adantr3  1142  syl3anr1  1268  syl3anr3  1270  dfbi3dc  1375  xordidc  1377  elabgt  2825  sbciegft  2939  csbtt  3014  csbnestgf  3052  copsex2t  4167  pofun  4234  onsucmin  4423  onsucelsucr  4424  onsucsssucr  4425  ordsucunielexmid  4446  ordsuc  4478  nlimsucg  4481  elnn  4519  xpsspw  4651  elxp4  5026  elxp5  5027  funimass2  5201  imain  5205  funimaexg  5207  f1ff1  5336  dff1o2  5372  resdif  5389  funbrfv  5460  fvelimab  5477  eqfnfv2  5519  fvimacnvi  5534  ffvresb  5583  fnressn  5606  fmptapd  5611  fnex  5642  rexima  5656  ralima  5657  f1elima  5674  fnotovb  5814  mpoeq12  5831  fovrn  5913  fnovrn  5918  ofrfval  5990  ofvalg  5991  cofunexg  6009  cofunex2g  6010  mpoexxg  6108  mpoexg  6109  f1o2ndf1  6125  spc2ed  6130  smodm2  6192  tfrlem9  6216  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  tfri3  6264  rdgtfr  6271  rdgruledefgg  6272  oav2  6359  oasuc  6360  omv2  6361  onasuc  6362  omsuc  6368  onmsuc  6369  nnaass  6381  nndi  6382  nndir  6386  nnaword  6407  ecelqsg  6482  iinerm  6501  ecovass  6538  ecoviass  6539  ecovdi  6540  ecovidi  6541  fvdiagfn  6587  ixpssmap2g  6621  domentr  6685  xpdom1g  6727  fopwdom  6730  ssenen  6745  phplem3  6748  phplem4  6749  php5dom  6757  ssfilem  6769  diffitest  6781  ctssdccl  6996  pm54.43  7046  addclpi  7142  addasspig  7145  mulasspig  7147  distrpig  7148  mulcanpig  7150  nnppipi  7158  enqdc1  7177  addassnqg  7197  ltbtwnnqq  7230  prarloclemarch  7233  prarloclemarch2  7234  enq0sym  7247  enq0ref  7248  addclnq0  7266  nqpnq0nq  7268  nnanq0  7273  distrnq0  7274  addassnq0lemcl  7276  addassnq0  7277  distnq0r  7278  prarloclemlt  7308  genpassl  7339  genpassu  7340  genpassg  7341  nqpru  7367  addcomprg  7393  mulcomprg  7395  distrlem1prl  7397  distrlem1pru  7398  1idprl  7405  1idpru  7406  recexprlemdisj  7445  recexprlem1ssl  7448  peano2nnnn  7668  ax1rid  7692  axcaucvglemcl  7710  le2tri3i  7879  add4  7930  cnegexlem1  7944  cnegexlem3  7946  cnegex  7947  subadd  7972  addsub  7980  addsubeq4  7984  negdi  8026  renegcl  8030  resubcl  8033  subdi  8154  mulneg2  8165  mul2neg  8167  submul2  8168  ltnegcon2  8233  lenegcon2  8236  lesub0  8248  cru  8371  recextlem1  8419  recexap  8421  div12ap  8461  divnegap  8473  letrp1  8613  dfinfre  8721  peano2nn  8739  nndivre  8763  nnsub  8766  nndivtr  8769  arch  8981  bndndx  8983  nn0addge1  9030  nn0addge2  9031  zaddcl  9101  zsubcl  9102  zltnle  9107  zrevaddcl  9111  nzadd  9113  zleltp1  9116  zltlem1  9118  zdiv  9146  peano2uz2  9165  uzind  9169  eluzp1l  9357  ublbneg  9412  qaddcl  9434  qsubcl  9437  qreccl  9441  qdivcl  9442  qrevaddcl  9443  irradd  9445  irrmul  9446  rerpdivcl  9479  nn0ledivnn  9561  xrre  9610  rexsub  9643  xaddass  9659  xnpcan  9662  xsubge0  9671  xposdif  9672  elioc2  9726  icoshft  9780  iccdil  9788  fzss2  9851  fzsuc2  9866  fzrev2  9872  elfzm11  9878  elfzp1b  9884  fzrevral  9892  fzshftral  9895  fzof  9928  fzoval  9932  fzon  9950  fzosubel  9978  zpnn0elfzo  9991  elfzom1b  10013  qltnle  10030  flqlt  10063  flqbi  10070  flqaddz  10077  fzofig  10212  seq3feq2  10250  ser3le  10298  expp1  10307  expm1t  10328  expeq0  10331  binom2sub  10412  bernneq  10419  expnlbnd  10423  faccl  10488  facdiv  10491  bcpasc  10519  bccl  10520  ffz0hash  10583  fnfzo0hash  10585  2shfti  10610  crim  10637  mulreap  10643  resub  10649  imsub  10657  ipcnval  10665  cjsub  10671  resqrexlemfp1  10788  resqrexlemgt0  10799  sqabsadd  10834  sqabssub  10835  abs2dif2  10886  cau3lem  10893  icodiamlt  10959  xrmaxaddlem  11036  clim  11057  clim2  11059  clim2c  11060  clim0c  11062  2clim  11077  climabs0  11083  climcn1  11084  climcn2  11085  climsqz  11111  climsqz2  11112  climub  11120  climserle  11121  fsum3cvg  11154  fisumss  11168  fsum3ser  11173  sumsplitdc  11208  fsump1i  11209  fsumlessfi  11236  telfsumo  11242  fsumparts  11246  iserabs  11251  binomlem  11259  isumsplit  11267  isum1p  11268  isumlessdc  11272  mertenslem2  11312  mertensabs  11313  prodfap0  11321  prodfrecap  11322  prodfdivap  11323  fproddccvg  11348  prodmodclem2  11353  ege2le3  11384  efsub  11394  efexp  11395  efsep  11404  sinsub  11454  cossub  11455  demoivre  11486  eirraplem  11490  moddvds  11509  0dvds  11520  iddvdsexp  11524  dvdssub  11545  dvdsle  11549  dvdsleabs  11550  dvdseq  11553  dvdsflip  11556  mulsucdiv2z  11589  divalgb  11629  divalg2  11630  ndvdsadd  11635  gcdneg  11677  gcdabs2  11685  modgcd  11686  bezoutlemsup  11704  gcdmultiplez  11716  gcdeq  11718  dvdssq  11726  lcmcllem  11755  lcmneg  11762  lcmdvds  11767  qredeu  11785  cncongrcoprm  11794  isprm3  11806  prmrp  11830  divnumden  11881  phiprmpw  11905  crth  11907  hashgcdlem  11910  hashgcdeq  11911  setsresg  12007  iunopn  12179  unopn  12182  eltg  12231  eltg2  12232  tgcl  12243  tgiun  12252  tgidm  12253  isopn3i  12314  isneip  12325  neipsm  12333  restbasg  12347  restopn2  12362  lmbrf  12394  cnclima  12402  lmss  12425  txbasval  12446  txlm  12458  psmetxrge0  12511  blininf  12603  blssps  12606  blss  12607  elmopn2  12628  bdmet  12681  metrest  12685  bl2ioo  12721  dvcjbr  12851  efper  12901  sinperlem  12902  abssinper  12940  bj-inex  13135  peano5set  13168  findset  13173  bj-findis  13207  nninfsellemsuc  13238  nninfself  13239  cvgcmp2nlemabs  13257  trilpolemeq1  13263
  Copyright terms: Public domain W3C validator