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  4159  issref  5007  fnun  5318  ovigg  5989  tfrlem9  6314  tfri3  6362  ordge1n0im  6431  nntri3or  6488  updjud  7075  axprecex  7870  peano5nnnn  7882  peano5nni  8911  zeo  9347  nn0ind-raph  9359  fzm1  10086  fzind2  10225  fzfig  10416  bcpasc  10730  climrecvg1n  11340  oddnn02np1  11868  oddge22np1  11869  evennn02n  11870  evennn2n  11871  gcdaddm  11968  coprmdvds1  12074  qredeq  12079  fiinopn  13169  zabsle1  14067  bj-intabssel  14197  triap  14433
  Copyright terms: Public domain W3C validator