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

Theorem syl5 32
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 29 . 2 (𝜑 → (𝜒𝜃))
43com12 30 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  34  syl2im  38  imim12i  58  pm2.86d  98  syl5bi  150  syl5bir  151  syl5ib  152  adantld  272  adantrd  273  impel  274  mpan9  275  nsyli  611  pm2.36  751  pm4.72  770  pm2.18dc  786  con1dc  789  jadc  796  pm2.521dc  800  con1biimdc  803  condandc  811  pm5.18dc  813  pm2.68dc  829  annimdc  881  syl3an2  1206  syl2an23an  1233  xor3dc  1321  alrimdh  1411  spsd  1474  a5i  1478  19.21h  1492  hbnt  1586  hbae  1650  sbiedh  1714  exdistrfor  1725  sbcof2  1735  ax11a2  1746  ax11v  1752  sb4  1757  hbsb4t  1934  exmoeudc  2008  euimmo  2012  mopick  2023  r19.37  2515  spcimgft  2688  spcimegft  2690  rr19.28v  2747  mob2  2786  euind  2793  reuind  2809  sbeqalb  2884  triun  3922  csbexga  3940  copsexg  4043  trssord  4179  trsuc  4221  trsucss  4222  ralxfrd  4256  rexxfrd  4257  ralxfrALT  4261  sucprcreg  4336  nlimsucg  4353  tfis  4369  relssres  4715  issref  4777  dmsnopg  4864  dfco2a  4893  imadif  5055  fvelima  5312  mptfvex  5344  fvmptdf  5346  fvmptf  5351  funfvima2  5481  funfvima3  5482  foco2  5487  isores3  5548  oprabid  5631  ovmpt4g  5717  ovmpt2s  5718  ov2gf  5719  ovmpt2df  5726  suppssfv  5802  suppssov1  5803  fo2ndf  5942  rntpos  5969  tposf2  5980  nnmordi  6220  nnmord  6221  nnaordex  6231  ectocld  6303  qsel  6314  mapsn  6392  f1oeng  6419  mapen  6507  nneneq  6518  findcard2  6550  findcard2s  6551  ac6sfi  6559  sbthlem1  6602  pr2ne  6756  ltbtwnnqq  6910  prnmaddl  6985  genpcdl  7014  genpcuu  7015  ltaddpr  7092  lteupri  7112  recexprlemss1l  7130  recexprlemss1u  7131  cauappcvgprlemdisj  7146  lttrsr  7244  recexgt0sr  7255  mulgt0sr  7259  axprecex  7351  rereceu  7360  addlsub  7784  recexap  8053  0mnnnnn0  8630  prime  8770  zeo  8776  fnn0ind  8787  zindd  8789  btwnz  8790  lbzbi  9025  addmodlteq  9725  facwordi  10036  iseqcoll  10135  qdenre  10522  climcau  10618  serif0  10623  zisum  10655  odd2np1  10739  ndvdssub  10796  dfgcd2  10869  nprm  10971  rpexp  10998  bj-sbimedh  11101  bj-vtoclgft  11104  elabgft1  11107  elabgf2  11109
  Copyright terms: Public domain W3C validator