ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5 Structured version   GIF 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  3857  csbexga  3875  copsexg  3971  trssord  4082  trsuc  4124  trsucss  4125  ralxfrd  4159  rexxfrd  4160  ralxfrALT  4164  sucprcreg  4226  nlimsucg  4241  tfis  4248  relssres  4590  issref  4649  dmsnopg  4734  dfco2a  4763  imadif  4920  fvelima  5166  mptfvex  5197  fvmptdf  5199  fvmptf  5204  foco2  5259  funfvima2  5332  funfvima3  5333  isores3  5396  oprabid  5477  ovmpt4g  5562  ovmpt2s  5563  ov2gf  5564  ovmpt2df  5571  suppssfv  5647  suppssov1  5648  fo2ndf  5787  rntpos  5810  tposf2  5821  nnmordi  6018  nnmord  6019  nnaordex  6029  ectocld  6101  qsel  6112  f1oeng  6166  ltbtwnnqq  6391  prnmaddl  6465  genpcdl  6495  genpcuu  6496  ltaddpr  6561  recexprlemss1l  6597  recexprlemss1u  6598  lttrsr  6642  recexgt0sr  6653  mulgt0sr  6656  axprecex  6716  recexap  7368  0mnnnnn0  7940  prime  8062  zeo  8068  fnn0ind  8079  zindd  8081  btwnz  8082  lbzbi  8276  bj-sbimedh  8845  bj-vtoclgft  8848  elabgft1  8851  elabgf2  8853
  Copyright terms: Public domain W3C validator