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

Theorem syl6bir 163
Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)
Hypotheses
Ref Expression
syl6bir.1  |-  ( ph  ->  ( ch  <->  ps )
)
syl6bir.2  |-  ( ch 
->  th )
Assertion
Ref Expression
syl6bir  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syl6bir
StepHypRef Expression
1 syl6bir.1 . . 3  |-  ( ph  ->  ( ch  <->  ps )
)
21biimprd 157 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 syl6bir.2 . 2  |-  ( ch 
->  th )
42, 3syl6 33 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  exdistrfor  1780  cbvexdh  1906  repizf2  4123  issref  4968  fnun  5276  ovigg  5941  tfrlem9  6266  tfri3  6314  ordge1n0im  6383  nntri3or  6440  updjud  7026  axprecex  7800  peano5nnnn  7812  peano5nni  8836  zeo  9269  nn0ind-raph  9281  fzm1  10002  fzind2  10138  fzfig  10329  bcpasc  10640  climrecvg1n  11245  oddnn02np1  11771  oddge22np1  11772  evennn02n  11773  evennn2n  11774  gcdaddm  11868  coprmdvds1  11968  qredeq  11973  fiinopn  12413  bj-intabssel  13374  triap  13611
  Copyright terms: Public domain W3C validator