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

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

Proof of Theorem biimtrrdi
StepHypRef Expression
1 biimtrrdi.1 . . 3 (𝜑 → (𝜒𝜓))
21biimprd 158 . 2 (𝜑 → (𝜓𝜒))
3 biimtrrdi.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  1811  cbvexdh  1938  repizf2  4183  issref  5032  fnun  5344  ovigg  6021  tfrlem9  6348  tfri3  6396  ordge1n0im  6465  nntri3or  6522  updjud  7115  axprecex  7914  peano5nnnn  7926  peano5nni  8957  zeo  9393  nn0ind-raph  9405  fzm1  10136  fzind2  10275  fzfig  10467  bcpasc  10787  climrecvg1n  11397  oddnn02np1  11926  oddge22np1  11927  evennn02n  11928  evennn2n  11929  gcdaddm  12026  coprmdvds1  12134  qredeq  12139  fiinopn  13989  zabsle1  14886  bj-intabssel  15027  triap  15265
  Copyright terms: Public domain W3C validator