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

Theorem syl2an 289
Description: A double syllogism inference. (Contributed by NM, 31-Jan-1997.)
Hypotheses
Ref Expression
syl2an.1 (𝜑𝜓)
syl2an.2 (𝜏𝜒)
syl2an.3 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
syl2an ((𝜑𝜏) → 𝜃)

Proof of Theorem syl2an
StepHypRef Expression
1 syl2an.2 . 2 (𝜏𝜒)
2 syl2an.1 . . 3 (𝜑𝜓)
3 syl2an.3 . . 3 ((𝜓𝜒) → 𝜃)
42, 3sylan 283 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2 286 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  syl2anr  290  anim12i  338  syl2an2  594  syl2an2r  595  mp3an3an  1343  eqeqan12d  2193  sylan9eq  2230  csbcomg  3080  sylan9ss  3168  ssconb  3268  ineqan12d  3338  dfopg  3774  breqan12d  4016  opexg  4224  copsex2g  4242  ordin  4381  onin  4382  unexg  4439  eusv1  4448  opelvvg  4671  opthprc  4673  opbrop  4701  relop  4772  dmpropg  5096  unixpm  5159  funssres  5253  funinsn  5260  funtp  5264  fnco  5319  resasplitss  5390  fodmrnu  5441  relrnfvex  5528  fconst2g  5726  oveqan12d  5887  ovi3  6004  ovg  6006  f1opw2  6070  off  6088  offres  6129  iunon  6278  nnsucsssuc  6486  nnaword1  6507  ertr  6543  erex  6552  brecop  6618  ecovdi  6639  ecovidi  6640  mapvalg  6651  pmvalg  6652  pmss12g  6668  mapsn  6683  en2sn  6806  xpf1o  6837  xpen  6838  phplem4  6848  ssfilem  6868  diffitest  6880  en1eqsn  6940  sbthlem7  6955  ordiso  7028  updjud  7074  fodju0  7138  finnum  7175  pr2nelem  7183  djucomen  7208  exmidontriimlem1  7213  ltsopi  7297  pitric  7298  pitri3or  7299  ltdcpi  7300  mulclpi  7305  addcompig  7306  mulcompig  7308  distrpig  7310  ltexpi  7314  ltapig  7315  ltmpig  7316  dfplpq2  7331  dfmpq2  7332  enqbreq2  7334  enqdc  7338  addcmpblnq  7344  addpipqqslem  7346  mulpipq2  7348  mulpipq  7349  mulpipqqs  7350  addclnq  7352  distrnqg  7364  ltdcnq  7374  ltrnqg  7397  enq0breq  7413  addclnq0  7428  nqnq0a  7431  nqnq0m  7432  nq0m0r  7433  distrnq0  7436  mulcomnq0  7437  genipv  7486  genplt2i  7487  genpelvl  7489  genpelvu  7490  addnqprlemrl  7534  addnqprlemru  7535  addnqprlemfl  7536  addnqprlemfu  7537  addnqpr  7538  mulnqprlemrl  7550  mulnqprlemru  7551  mulnqprlemfl  7552  mulnqprlemfu  7553  mulnqpr  7554  distrlem4prl  7561  distrlem4pru  7562  ltnqpr  7570  recexprlemloc  7608  archrecnq  7640  mulclsr  7731  1idsr  7745  00sr  7746  prsradd  7763  axmulass  7850  axdistr  7851  axcnre  7858  peano5nnnn  7869  mulid1  7932  axltadd  8004  lenlt  8010  cnegexlem3  8111  cnegex  8112  resubcl  8198  subeqrev  8310  muladd  8318  mulsub  8335  mulsub2  8336  ltaddsub2  8371  leaddsub2  8373  leltadd  8381  ltaddpos2  8387  posdif  8389  addge02  8407  mullt0  8414  recexre  8512  recextlem1  8584  recexap  8586  divmuldivap  8645  conjmulap  8662  div2subap  8770  prodgt02  8786  prodge02  8788  lemul2  8790  lemul2a  8792  ltmulgt12  8798  lemulge12  8800  ltmuldiv2  8808  ltdivmul2  8811  ledivmul2  8813  lemuldiv2  8815  negiso  8888  cju  8894  peano5nni  8898  nnaddcl  8915  nnmulcl  8916  nnsub  8934  addltmul  9131  avgle1  9135  avgle2  9136  nnrecl  9150  nn0nnaddcl  9183  zsubcl  9270  zleloe  9276  znnsub  9280  nzadd  9281  zmulcl  9282  zltp1le  9283  zleltp1  9284  nnleltp1  9288  nnltp1le  9289  nnaddm1cl  9290  nn0ltp1le  9291  nn0leltp1  9292  nn0ltlem1  9293  znn0sub  9294  nn0sub  9295  elz2  9300  zapne  9303  zdcle  9305  zdclt  9306  zltlen  9307  nn0lem1lt  9312  nnlem1lt  9313  nnltlem1  9314  zdiv  9317  zextle  9320  zextlt  9321  btwnnz  9323  prime  9328  nneo  9332  peano2uz2  9336  peano5uzti  9337  uzind  9340  fzind  9344  fnn0ind  9345  uzneg  9522  uz11  9526  eluzp1m1  9527  eluzp1p1  9529  uzin  9536  indstr  9569  uz2mulcl  9584  qre  9601  qaddcl  9611  qsubcl  9614  qltlen  9616  qlttri2  9617  irradd  9622  elpqb  9625  cnref1o  9626  rpaddcl  9651  rpmulcl  9652  rpdivcl  9653  rexadd  9826  rexsub  9827  xaddcom  9835  xnn0xadd0  9841  xnegdi  9842  elicc2  9912  iccshftr  9968  iccshftl  9970  iccdil  9972  icccntr  9974  fzval2  9985  elfz1eq  10008  peano2fzr  10010  fznlem  10014  fzsplit2  10023  fzaddel  10032  fzsubel  10033  fzrev2  10058  fzrev3  10060  uzsplit  10065  fzrevral  10078  fzrevral3  10080  fzshftral  10081  elfz2nn0  10085  fznn0sub2  10101  fz0fzdiffz0  10103  elfzmlbp  10105  difelfzle  10107  difelfznle  10108  1fv  10112  elfzouz2  10134  fzouzsplit  10152  elfzo0le  10158  fzonmapblen  10160  fzofzim  10161  fzoaddel2  10166  eluzgtdifelfzo  10170  elfzodifsumelfzo  10174  ubmelm1fzo  10199  fzofzp1b  10201  fzosplitprm1  10207  fzostep1  10210  subfzo0  10215  qbtwnxr  10231  flqbi2  10264  divfl0  10269  flqzadd  10271  flqmulnn0  10272  addmodidr  10346  modfzo0difsn  10368  frec2uzltd  10376  frec2uzrand  10378  frecfzen2  10400  seq3split  10452  seq3caopr2  10455  exp3vallem  10494  expcllem  10504  expcl2lemap  10505  1exp  10522  expge1  10530  expadd  10535  expmul  10538  expsubap  10541  leexp1a  10548  lt2sq  10566  le2sq  10567  sumsqeq0  10571  qsqeqor  10603  bernneq  10613  bernneq2  10614  sq11ap  10660  facdiv  10689  faclbnd  10692  faclbnd3  10694  faclbnd6  10695  facavg  10697  bcrpcl  10704  bccmpl  10705  fiubm  10779  seq3coll  10793  shftfvalg  10798  shftf  10810  crre  10837  crim  10838  mulreap  10844  readd  10849  resub  10850  remul2  10853  imadd  10857  imsub  10858  immul2  10860  ipcnval  10866  cjsub  10872  cjreim  10883  caucvgre  10961  rexanuz  10968  rexuz3  10970  resqrexlemover  10990  resqrexlemcvg  10999  resqrexlemglsq  11002  sqrtle  11016  sqrtlt  11017  sqrt11ap  11018  sqrt11  11019  absreimsq  11047  absreim  11048  absmul  11049  sqabs  11062  absdiflt  11072  absdifle  11073  abssuble0  11083  abs2difabs  11088  fzomaxdif  11093  caubnd2  11097  rpmaxcl  11203  zmaxcl  11204  minmax  11209  mincl  11210  min1inf  11211  min2inf  11212  minabs  11215  minclpr  11216  rpmincl  11217  2zinfmin  11222  xrmaxrecl  11234  xrminmax  11244  xrmincl  11245  xrmin1inf  11246  xrmin2inf  11247  xrminrecl  11252  xrminrpcl  11253  iooinsup  11256  climconst2  11270  climuni  11272  2clim  11280  climshft  11283  climshft2  11285  cjcn2  11295  climaddc1  11308  climmulc2  11310  climsubc1  11311  climsubc2  11312  climlec2  11320  summodclem2a  11360  zsumdc  11363  isumclim3  11402  mptfzshft  11421  fsumrev  11422  fisum0diag2  11426  telfsumo2  11446  fsumparts  11449  cvgcmpub  11455  binomlem  11462  binom1p  11464  binom1dif  11466  bcxmas  11468  isumshft  11469  expcnvap0  11481  expcnv  11483  geosergap  11485  geolim  11490  cvgratnnlemrate  11509  mertenslemi1  11514  mertenslem2  11515  mertensabs  11516  prodmodc  11557  zproddc  11558  fprodf1o  11567  fprodeq0  11596  efcj  11652  eftlub  11669  effsumlt  11671  efieq  11714  sinsub  11719  cossub  11720  subsin  11722  sinmul  11723  cosmul  11724  addcos  11725  subcos  11726  dvdssub2  11813  dvdsadd  11814  dvdsaddr  11815  dvdssub  11816  dvdssubr  11817  fzocongeq  11834  odd2np1  11848  opoe  11870  omoe  11871  opeo  11872  omeo  11873  divalgb  11900  ndvdsadd  11906  zsupcllemstep  11916  gcdabs  11959  dvdsgcd  11983  absmulgcd  11988  gcdmultiple  11991  gcdmultiplez  11992  rpmulgcd  11997  sqgcd  12000  dvdssqlem  12001  dvdssq  12002  nn0seqcvgd  12011  ialgrlemconst  12013  algrf  12015  algrp1  12016  algcvg  12018  algcvga  12021  lcmval  12033  lcmabs  12046  lcmgcd  12048  lcmdvds  12049  lcmgcdnn  12052  coprmgcdb  12058  coprmdvds  12062  coprmdvds2  12063  qredeq  12066  isprm3  12088  nprm  12093  divgcdodd  12113  prmdvdsexp  12118  sqrt2irr  12132  zgcdsq  12171  hashdvds  12191  phiprmpw  12192  crth  12194  phimullem  12195  modprm0  12224  coprimeprodsq  12227  coprimeprodsq2  12228  pythagtriplem2  12236  pythagtriplem19  12252  pcdvdsb  12289  pcneg  12294  pc2dvds  12299  pc11  12300  pcmpt  12311  pcfac  12318  infpnlem1  12327  prmunb  12330  1arithlem4  12334  1arith  12335  gzaddcl  12345  gzmulcl  12346  gzreim  12347  gzsubcl  12348  4sqlem1  12356  4sqlem4a  12359  4sqlem4  12360  setsvalg  12462  setsfun0  12468  restval  12629  mndinvmod  12723  mhmco  12751  dfgrp3m  12845  mhmmnd  12856  mulgnn0z  12885  mulgnndir  12887  ablsubsub23  12942  innei  13296  cnovex  13329  txuni2  13389  txbasex  13390  txbas  13391  txtop  13393  txtopon  13395  txss12  13399  txbasval  13400  txcnp  13404  upxp  13405  txcnmpt  13406  uptx  13407  txcn  13408  txrest  13409  txdis  13410  cnmpt21  13424  hmeoco  13449  txhmeo  13452  isxmet2d  13481  blin2  13565  comet  13632  metcn  13647  txmetcn  13652  qtopbasss  13654  qtopbas  13655  remetdval  13672  bl2ioo  13675  blssioo  13678  divcnap  13688  cncfmet  13712  dvaddxxbr  13798  dvcjbr  13805  efle  13830  reapef  13832  sinperlem  13862  sincosq2sgn  13881  sincosq3sgn  13882  sincos6thpi  13896  ioocosf1o  13908  relogoprlem  13922  logleb  13929  cxple3  13974  cxpcom  13990  lgslem3  14036  lgsdir2  14067  lgsdir  14069  lgsdilem2  14070  lgsdi  14071  2sqlem2  14084  mul2sq  14085  2sqlem7  14090  bj-inex  14281  bj-bdfindis  14321  triap  14400  cvgcmp2nlemabs  14403  trilpolemisumle  14409  inffz  14440
  Copyright terms: Public domain W3C validator