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

Theorem syl2an 287
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 281 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2 284 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:  syl2anr  288  anim12i  336  syl2an2  568  syl2an2r  569  mp3an3an  1306  eqeqan12d  2133  sylan9eq  2170  csbcomg  2996  sylan9ss  3080  ssconb  3179  ineqan12d  3249  dfopg  3673  breqan12d  3915  opexg  4120  copsex2g  4138  ordin  4277  onin  4278  unexg  4334  eusv1  4343  opelvvg  4558  opthprc  4560  opbrop  4588  relop  4659  dmpropg  4981  unixpm  5044  funssres  5135  funinsn  5142  funtp  5146  fnco  5201  resasplitss  5272  fodmrnu  5323  relrnfvex  5407  fconst2g  5603  oveqan12d  5761  ovi3  5875  ovg  5877  f1opw2  5944  off  5962  offres  6001  iunon  6149  nnsucsssuc  6356  nnaword1  6377  ertr  6412  erex  6421  brecop  6487  ecovdi  6508  ecovidi  6509  mapvalg  6520  pmvalg  6521  pmss12g  6537  mapsn  6552  en2sn  6675  xpf1o  6706  xpen  6707  phplem4  6717  ssfilem  6737  diffitest  6749  en1eqsn  6804  sbthlem7  6819  ordiso  6889  updjud  6935  fodju0  6987  finnum  7007  pr2nelem  7015  djucomen  7040  ltsopi  7096  pitric  7097  pitri3or  7098  ltdcpi  7099  mulclpi  7104  addcompig  7105  mulcompig  7107  distrpig  7109  ltexpi  7113  ltapig  7114  ltmpig  7115  dfplpq2  7130  dfmpq2  7131  enqbreq2  7133  enqdc  7137  addcmpblnq  7143  addpipqqslem  7145  mulpipq2  7147  mulpipq  7148  mulpipqqs  7149  addclnq  7151  distrnqg  7163  ltdcnq  7173  ltrnqg  7196  enq0breq  7212  addclnq0  7227  nqnq0a  7230  nqnq0m  7231  nq0m0r  7232  distrnq0  7235  mulcomnq0  7236  genipv  7285  genplt2i  7286  genpelvl  7288  genpelvu  7289  addnqprlemrl  7333  addnqprlemru  7334  addnqprlemfl  7335  addnqprlemfu  7336  addnqpr  7337  mulnqprlemrl  7349  mulnqprlemru  7350  mulnqprlemfl  7351  mulnqprlemfu  7352  mulnqpr  7353  distrlem4prl  7360  distrlem4pru  7361  ltnqpr  7369  recexprlemloc  7407  archrecnq  7439  mulclsr  7530  1idsr  7544  00sr  7545  prsradd  7562  axmulass  7649  axdistr  7650  axcnre  7657  peano5nnnn  7668  mulid1  7731  axltadd  7802  lenlt  7808  cnegexlem3  7907  cnegex  7908  resubcl  7994  subeqrev  8106  muladd  8114  mulsub  8131  mulsub2  8132  ltaddsub2  8167  leaddsub2  8169  leltadd  8177  ltaddpos2  8183  posdif  8185  addge02  8203  mullt0  8210  recexre  8308  recextlem1  8380  recexap  8382  divmuldivap  8440  conjmulap  8457  div2subap  8564  prodgt02  8579  prodge02  8581  lemul2  8583  lemul2a  8585  ltmulgt12  8591  lemulge12  8593  ltmuldiv2  8601  ltdivmul2  8604  ledivmul2  8606  lemuldiv2  8608  negiso  8681  cju  8687  peano5nni  8691  nnaddcl  8708  nnmulcl  8709  nnsub  8727  addltmul  8924  avgle1  8928  avgle2  8929  nnrecl  8943  nn0nnaddcl  8976  zsubcl  9063  zleloe  9069  znnsub  9073  nzadd  9074  zmulcl  9075  zltp1le  9076  zleltp1  9077  nnleltp1  9081  nnltp1le  9082  nnaddm1cl  9083  nn0ltp1le  9084  nn0leltp1  9085  nn0ltlem1  9086  znn0sub  9087  nn0sub  9088  elz2  9090  zapne  9093  zdcle  9095  zdclt  9096  zltlen  9097  nn0lem1lt  9102  nnlem1lt  9103  nnltlem1  9104  zdiv  9107  zextle  9110  zextlt  9111  btwnnz  9113  prime  9118  nneo  9122  peano2uz2  9126  peano5uzti  9127  uzind  9130  fzind  9134  fnn0ind  9135  uzneg  9312  uz11  9316  eluzp1m1  9317  eluzp1p1  9319  uzin  9326  indstr  9356  uz2mulcl  9370  qre  9385  qaddcl  9395  qsubcl  9398  qltlen  9400  qlttri2  9401  irradd  9406  cnref1o  9408  rpaddcl  9433  rpmulcl  9434  rpdivcl  9435  rexadd  9603  rexsub  9604  xaddcom  9612  xnn0xadd0  9618  xnegdi  9619  elicc2  9689  iccshftr  9745  iccshftl  9747  iccdil  9749  icccntr  9751  fzval2  9761  elfz1eq  9783  peano2fzr  9785  fznlem  9789  fzsplit2  9798  fzaddel  9807  fzsubel  9808  fzrev2  9833  fzrev3  9835  uzsplit  9840  fzrevral  9853  fzrevral3  9855  fzshftral  9856  elfz2nn0  9860  fznn0sub2  9873  fz0fzdiffz0  9875  elfzmlbp  9877  difelfzle  9879  difelfznle  9880  1fv  9884  elfzouz2  9906  fzouzsplit  9924  elfzo0le  9930  fzonmapblen  9932  fzofzim  9933  fzoaddel2  9938  eluzgtdifelfzo  9942  elfzodifsumelfzo  9946  ubmelm1fzo  9971  fzofzp1b  9973  fzosplitprm1  9979  fzostep1  9982  subfzo0  9987  qbtwnxr  10003  flqbi2  10032  divfl0  10037  flqzadd  10039  flqmulnn0  10040  addmodidr  10114  modfzo0difsn  10136  frec2uzltd  10144  frec2uzrand  10146  frecfzen2  10168  seq3split  10220  seq3caopr2  10223  exp3vallem  10262  expcllem  10272  expcl2lemap  10273  1exp  10290  expge1  10298  expadd  10303  expmul  10306  expsubap  10309  leexp1a  10316  lt2sq  10334  le2sq  10335  sumsqeq0  10339  bernneq  10380  bernneq2  10381  sq11ap  10426  facdiv  10452  faclbnd  10455  faclbnd3  10457  faclbnd6  10458  facavg  10460  bcrpcl  10467  bccmpl  10468  seq3coll  10553  shftfvalg  10558  shftf  10570  crre  10597  crim  10598  mulreap  10604  readd  10609  resub  10610  remul2  10613  imadd  10617  imsub  10618  immul2  10620  ipcnval  10626  cjsub  10632  cjreim  10643  caucvgre  10721  rexanuz  10728  rexuz3  10730  resqrexlemover  10750  resqrexlemcvg  10759  resqrexlemglsq  10762  sqrtle  10776  sqrtlt  10777  sqrt11ap  10778  sqrt11  10779  absreimsq  10807  absreim  10808  absmul  10809  sqabs  10822  absdiflt  10832  absdifle  10833  abssuble0  10843  abs2difabs  10848  fzomaxdif  10853  caubnd2  10857  rpmaxcl  10963  zmaxcl  10964  minmax  10969  mincl  10970  min1inf  10971  min2inf  10972  minabs  10975  minclpr  10976  rpmincl  10977  xrmaxrecl  10992  xrminmax  11002  xrmincl  11003  xrmin1inf  11004  xrmin2inf  11005  xrminrecl  11010  xrminrpcl  11011  iooinsup  11014  climconst2  11028  climuni  11030  2clim  11038  climshft  11041  climshft2  11043  cjcn2  11053  climaddc1  11066  climmulc2  11068  climsubc1  11069  climsubc2  11070  climlec2  11078  summodclem2a  11118  zsumdc  11121  isumclim3  11160  mptfzshft  11179  fsumrev  11180  fisum0diag2  11184  telfsumo2  11204  fsumparts  11207  cvgcmpub  11213  binomlem  11220  binom1p  11222  binom1dif  11224  bcxmas  11226  isumshft  11227  expcnvap0  11239  expcnv  11241  geosergap  11243  geolim  11248  cvgratnnlemrate  11267  mertenslemi1  11272  mertenslem2  11273  mertensabs  11274  efcj  11306  eftlub  11323  effsumlt  11325  efieq  11369  sinsub  11374  cossub  11375  subsin  11377  sinmul  11378  cosmul  11379  addcos  11380  subcos  11381  dvdssub2  11462  dvdsadd  11463  dvdsaddr  11464  dvdssub  11465  dvdssubr  11466  fzocongeq  11483  odd2np1  11497  opoe  11519  omoe  11520  opeo  11521  omeo  11522  divalgb  11549  ndvdsadd  11555  zsupcllemstep  11565  gcdabs  11603  dvdsgcd  11627  absmulgcd  11632  gcdmultiple  11635  gcdmultiplez  11636  rpmulgcd  11641  sqgcd  11644  dvdssqlem  11645  dvdssq  11646  nn0seqcvgd  11649  ialgrlemconst  11651  algrf  11653  algrp1  11654  algcvg  11656  algcvga  11659  lcmval  11671  lcmabs  11684  lcmgcd  11686  lcmdvds  11687  lcmgcdnn  11690  coprmgcdb  11696  coprmdvds  11700  coprmdvds2  11701  qredeq  11704  isprm3  11726  nprm  11731  divgcdodd  11748  prmdvdsexp  11753  sqrt2irr  11767  zgcdsq  11806  hashdvds  11824  phiprmpw  11825  crth  11827  phimullem  11828  setsvalg  11916  setsfun0  11922  restval  12053  innei  12259  cnovex  12292  txuni2  12352  txbasex  12353  txbas  12354  txtop  12356  txtopon  12358  txss12  12362  txbasval  12363  txcnp  12367  upxp  12368  txcnmpt  12369  uptx  12370  txcn  12371  txrest  12372  txdis  12373  cnmpt21  12387  hmeoco  12412  txhmeo  12415  isxmet2d  12444  blin2  12528  comet  12595  metcn  12610  txmetcn  12615  qtopbasss  12617  qtopbas  12618  remetdval  12635  bl2ioo  12638  blssioo  12641  divcnap  12651  cncfmet  12675  dvaddxxbr  12761  dvcjbr  12768  sinperlem  12816  sincosq2sgn  12835  sincosq3sgn  12836  sincos6thpi  12850  bj-inex  13032  bj-bdfindis  13072  triap  13151  cvgcmp2nlemabs  13154  trilpolemisumle  13158  inffz  13165
  Copyright terms: Public domain W3C validator