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

Theorem syl5 26
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 24 . 2 (φ → (χθ))
43com12 25 1 (χ → (φθ))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem is referenced by:  syl56  28  syl2im  32  imim12i  51  pm2.86d  91  syl5bi  139  syl5bir  140  syl5ib  141  adantld  261  adantrd  262  mpan9  263  nsyli  559  pm2.36  695  pm4.72  715  pm2.18dc  725  con1dc  727  jadc  734  pm2.521dc  738  con1biimdc  741  condandc  749  pm5.18dc  751  pm2.68dc  766  annimdc  806  syl3an2  1122  xor3dc  1218  alrimdh  1303  spsd  1369  a5i  1373  19.21h  1387  hbnt  1470  hbae  1524  sbiedh  1589  exdistrf  1599  ax11a2  1620  ax11v  1626  sb4  1631  sbalyz  1789  hbsb4t  1801  exmoeudc  1871  euimmo  1875  mopick  1887  r19.37  2324  spcimgft  2489  spcimegft  2491  rr19.28v  2542  mob2  2578  euind  2585  reuind  2601
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
  Copyright terms: Public domain W3C validator