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

Theorem syl6bir 164
Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)
Hypotheses
Ref Expression
syl6bir.1 (𝜑 → (𝜒𝜓))
syl6bir.2 (𝜒𝜃)
Assertion
Ref Expression
syl6bir (𝜑 → (𝜓𝜃))

Proof of Theorem syl6bir
StepHypRef Expression
1 syl6bir.1 . . 3 (𝜑 → (𝜒𝜓))
21biimprd 158 . 2 (𝜑 → (𝜓𝜒))
3 syl6bir.2 . 2 (𝜒𝜃)
42, 3syl6 33 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  exdistrfor  1800  cbvexdh  1926  repizf2  4164  issref  5013  fnun  5324  ovigg  5997  tfrlem9  6322  tfri3  6370  ordge1n0im  6439  nntri3or  6496  updjud  7083  axprecex  7881  peano5nnnn  7893  peano5nni  8924  zeo  9360  nn0ind-raph  9372  fzm1  10102  fzind2  10241  fzfig  10432  bcpasc  10748  climrecvg1n  11358  oddnn02np1  11887  oddge22np1  11888  evennn02n  11889  evennn2n  11890  gcdaddm  11987  coprmdvds1  12093  qredeq  12098  fiinopn  13543  zabsle1  14439  bj-intabssel  14580  triap  14816
  Copyright terms: Public domain W3C validator