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

Theorem syl5 27
Description: A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. (The proof was 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 25 . 2 (φ → (χθ))
43com12 26 1 (χ → (φθ))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem is referenced by:  syl56  29  syl2im  33  imim12i  52  pm2.86d  92  syl5bi  140  syl5bir  141  syl5ib  142  adantld  262  adantrd  263  mpan9  264  nsyli  557  pm2.36  692  pm4.72  712  pm4.79  819  ecased  879  ecase3ad  880  syl3an2  1180  alrimd  1359  a9wa9lem2  1405  a9wa9lem8OLD  1414  ax5o  1424  ax5  1426  a4sd  1434  hbnt  1435  a5i  1437  19.21  1464  19.33bOLD  1521  hbae  1578  dvelimfALT  1585  exdistrf  1590  sbied  1629  ax11a2  1652  sb4  1659  hbsb4  1686  hbsb4t  1687  ax11v  1703  ax11indn  1813  ax11inda2  1817  a12study  1825  a12study3  1828  hbeu  1840  hbeud  1841  euimmo  1873  mopick  1886
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator