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

Theorem syl2an 273
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 267 . 2 ((φ χ) → θ)
51, 4sylan2 270 1 ((φ τ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  syl2anr  274  anim12i  321  eqeqan12d  2029  sylan9eq  2066  csbcomg  2842  sylan9ss  2927  ssconb  3045  ineqan12d  3109  dfopg  3511  breqan12d  3743  prelpwi  3914  opexg  3928  copsex2g  3947  ordin  4061  onin  4062  unexg  4117  eusv1  4123  op1stbg  4149  opelvvg  4305  opthprc  4307  opbrop  4335  relop  4402  dmpropg  4709  unixpm  4769  funssres  4857  funtp  4867  fnco  4922  resasplitss  4983  fodmrnu  5028  relrnfvex  5107  fconst2g  5290  fliftel  5347  oveqan12d  5444  ovi3  5549  ovg  5551  f1opw2  5618  off  5636  offres  5674  iunon  5810  nnsucsssuc  5975  nnaword1  5986  ertr  6021  erex  6030  brecop  6096  ecovdi  6117  ecovidi  6118  ltsopi  6167  pitric  6168  pitri3or  6169  ltdcpi  6170  mulclpi  6175  addcompig  6176  mulcompig  6178  distrpig  6180  ltexpi  6184  ltapig  6185  ltmpig  6186  dfplpq2  6200  dfmpq2  6201  enqbreq2  6203  enqdc  6207  addcmpblnq  6213  addpipqqslem  6215  mulpipq2  6217  mulpipq  6218  mulpipqqs  6219  addclnq  6221  distrnqg  6233  ltdcnq  6243  ltrnqg  6264  enq0breq  6278  addclnq0  6293  nqnq0a  6296  nqnq0m  6297  nq0m0r  6298  distrnq0  6301  mulcomnq0  6302  genipv  6350  genplt2i  6351  genpelvl  6353  genpelvu  6354  distrlem4prl  6410  distrlem4pru  6411  recexprlemloc  6453  mulclsr  6493  1idsr  6507  00sr  6508  axmulass  6563  axdistr  6564  axcnre  6571  mulid1  6626  axltadd  6690  lenlt  6695  cnegexlem3  6789  cnegex  6790  resubcl  6875  subeqrev  6974  muladd  6981  mulsub  6998  mulsub2  6999  ltaddsub2  7031  leaddsub2  7033  leltadd  7041  ltaddpos2  7047  posdif  7049  addge02  7067  mullt0  7074  recexre  7166  recextlem1  7218  recexap  7220  divmuldivap  7274  conjmulap  7291  prodgt02  7403  prodge02  7405  lemul2  7407  lemul2a  7409  ltmulgt12  7415  lemulge12  7417  ltmuldiv2  7425  ltdivmul2  7428  ledivmul2  7430  lemuldiv2  7432  cju  7497  peano5nni  7501  nnaddcl  7518  nnmulcl  7519  nnsub  7536  addltmul  7740  avgle1  7744  avgle2  7745  nn0nnaddcl  7788  zsubcl  7860  znnsub  7868  zmulcl  7869  zltp1le  7870  zleltp1  7871  nnleltp1  7875  nnltp1le  7876  nnaddm1cl  7877  nn0ltp1le  7878  nn0leltp1  7879  nn0ltlem1  7880  znn0sub  7881  nn0sub  7882  zapne  7884  zltlen  7886  nn0lem1lt  7889  nnlem1lt  7890  nnltlem1  7891  zdiv  7894  zextle  7897  zextlt  7898  btwnnz  7900  prime  7903  nneo  7907  peano2uz2  7911  peano5uzti  7912  uzind  7915  fzind  7919  fnn0ind  7920  qre  8044  qaddcl  8054  qsubcl  8057  irradd  8063  rpaddcl  8088  rpmulcl  8089  rpdivcl  8090  bj-inex  8360  bj-bdfindis  8403
  Copyright terms: Public domain W3C validator