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

Theorem syl5 28
Description: A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)
Hypotheses
Ref Expression
syl5.1
syl5.2
Assertion
Ref Expression
syl5

Proof of Theorem syl5
StepHypRef Expression
1 syl5.1 . . 3
2 syl5.2 . . 3
31, 2syl5com 26 . 2
43com12 27 1
Colors of variables: wff set class
Syntax hints:   wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  syl56  30  syl2im  34  imim12i  53  pm2.86d  93  syl5bi  141  syl5bir  142  syl5ib  143  adantld  263  adantrd  264  mpan9  265  nsyli  577  pm2.36  716  pm4.72  735  pm2.18dc  749  con1dc  752  jadc  759  pm2.521dc  763  con1biimdc  766  condandc  774  pm5.18dc  776  pm2.68dc  792  annimdc  844  syl3an2  1168  xor3dc  1275  alrimdh  1365  spsd  1428  a5i  1432  19.21h  1446  hbnt  1540  hbae  1603  sbiedh  1667  exdistrfor  1678  sbcof2  1688  ax11a2  1699  ax11v  1705  sb4  1710  hbsb4t  1886  exmoeudc  1960  euimmo  1964  mopick  1975  r19.37  2456  spcimgft  2623  spcimegft  2625  rr19.28v  2677  mob2  2715  euind  2722  reuind  2738  sbeqalb  2809  sbcimdv  2817  triun  3858  csbexga  3876  copsexg  3972  trssord  4083  trsuc  4125  trsucss  4126  ralxfrd  4160  rexxfrd  4161  ralxfrALT  4165  sucprcreg  4227  nlimsucg  4242  tfis  4249  relssres  4591  issref  4650  dmsnopg  4735  dfco2a  4764  imadif  4922  fvelima  5168  mptfvex  5199  fvmptdf  5201  fvmptf  5206  foco2  5261  funfvima2  5334  funfvima3  5335  isores3  5398  oprabid  5480  ovmpt4g  5565  ovmpt2s  5566  ov2gf  5567  ovmpt2df  5574  suppssfv  5650  suppssov1  5651  fo2ndf  5790  rntpos  5813  tposf2  5824  nnmordi  6025  nnmord  6026  nnaordex  6036  ectocld  6108  qsel  6119  f1oeng  6173  ltbtwnnqq  6398  prnmaddl  6472  genpcdl  6502  genpcuu  6503  ltaddpr  6569  recexprlemss1l  6605  recexprlemss1u  6606  lttrsr  6650  recexgt0sr  6661  mulgt0sr  6664  axprecex  6724  recexap  7376  0mnnnnn0  7950  prime  8073  zeo  8079  fnn0ind  8090  zindd  8092  btwnz  8093  lbzbi  8287  bj-sbimedh  9180  bj-vtoclgft  9183  elabgft1  9186  elabgf2  9188
  Copyright terms: Public domain W3C validator