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-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com12  30  syl5  32  pm2.6dc  857  pm5.11dc  904  ax16i  1851  mor  2061  ceqsalg  2758  cgsexg  2765  cgsex2g  2766  cgsex4g  2767  spc2egv  2820  spc2gv  2821  spc3egv  2822  spc3gv  2823  disjne  3467  uneqdifeqim  3499  eqifdc  3559  triun  4098  sucssel  4407  ordsucg  4484  regexmidlem1  4515  relresfld  5138  relcoi1  5140  fornex  6092  f1dmex  6093  dom2d  6748  findcard  6863  nneo  9304  zeo2  9307  uznfz  10048  difelfzle  10079  ssfzo12  10169  facndiv  10662  fisumcom2  11390  fprodssdc  11542  fprodcom2fi  11578  ndvdssub  11878  bezoutlembi  11949  eucalglt  12000  prmind2  12063  coprm  12087  prmdiveq  12179  mhmlin  12679  inopn  12756  basis1  12800  tgss  12818  tgcl  12819  xmeteq0  13114  blssexps  13184  blssex  13185  mopni3  13239  neibl  13246  metss  13249  metcnp3  13266  logbgcd1irr  13640  bj-indsuc  13925  bj-nntrans  13948
  Copyright terms: Public domain W3C validator