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

Theorem syl5com 26
 Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)
Hypotheses
Ref Expression
syl5com.1 (𝜑𝜓)
syl5com.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5com (𝜑 → (𝜒𝜃))

Proof of Theorem syl5com
StepHypRef Expression
1 syl5com.1 . . 3 (𝜑𝜓)
21a1d 22 . 2 (𝜑 → (𝜒𝜓))
3 syl5com.2 . 2 (𝜒 → (𝜓𝜃))
42, 3sylcom 25 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:  com12  27  syl5  28  pm2.6dc  759  pm5.11dc  815  ax16i  1738  mor  1942  ceqsalg  2582  cgsexg  2589  cgsex2g  2590  cgsex4g  2591  spc2egv  2642  spc2gv  2643  spc3egv  2644  spc3gv  2645  disjne  3273  uneqdifeqim  3308  triun  3867  sucssel  4161  ordsucg  4228  regexmidlem1  4258  relresfld  4847  relcoi1  4849  fornex  5742  f1dmex  5743  rdgon  5973  dom2d  6253  findcard  6345  nneo  8341  zeo2  8344  uznfz  8965  difelfzle  8992  ssfzo12  9080  bj-indsuc  10052  bj-nntrans  10076
 Copyright terms: Public domain W3C validator