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  847  pm5.11dc  894  ax16i  1830  mor  2039  ceqsalg  2709  cgsexg  2716  cgsex2g  2717  cgsex4g  2718  spc2egv  2770  spc2gv  2771  spc3egv  2772  spc3gv  2773  disjne  3411  uneqdifeqim  3443  eqifdc  3501  triun  4034  sucssel  4341  ordsucg  4413  regexmidlem1  4443  relresfld  5063  relcoi1  5065  fornex  6006  f1dmex  6007  dom2d  6660  findcard  6775  nneo  9147  zeo2  9150  uznfz  9876  difelfzle  9904  ssfzo12  9994  facndiv  10478  fisumcom2  11200  ndvdssub  11616  bezoutlembi  11682  eucalglt  11727  prmind2  11790  coprm  11811  inopn  12159  basis1  12203  tgss  12221  tgcl  12222  xmeteq0  12517  blssexps  12587  blssex  12588  mopni3  12642  neibl  12649  metss  12652  metcnp3  12669  bj-indsuc  13115  bj-nntrans  13138
 Copyright terms: Public domain W3C validator