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

Theorem syl5com 29
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 28 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  30  syl5  32  pm2.6dc  770  pm5.11dc  826  ax16i  1754  mor  1958  ceqsalg  2599  cgsexg  2606  cgsex2g  2607  cgsex4g  2608  spc2egv  2659  spc2gv  2660  spc3egv  2661  spc3gv  2662  disjne  3300  uneqdifeqim  3335  triun  3894  sucssel  4188  ordsucg  4255  regexmidlem1  4285  relresfld  4874  relcoi1  4876  fornex  5769  f1dmex  5770  rdgon  6003  dom2d  6283  findcard  6375  nneo  8399  zeo2  8402  uznfz  9066  difelfzle  9093  ssfzo12  9181  facndiv  9600  bj-indsuc  10411  bj-nntrans  10435
  Copyright terms: Public domain W3C validator