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

Theorem syl6bir 162
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 156 . 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 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  exdistrfor  1728  cbvexdh  1849  repizf2  3997  issref  4814  fnun  5120  ovigg  5765  tfrlem9  6084  tfri3  6132  ordge1n0im  6200  nntri3or  6254  updjud  6773  axprecex  7415  peano5nnnn  7427  peano5nni  8425  zeo  8851  nn0ind-raph  8863  fzm1  9514  fzind2  9650  fzfig  9837  bcpasc  10174  climrecvg1n  10737  oddnn02np1  11158  oddge22np1  11159  evennn02n  11160  evennn2n  11161  gcdaddm  11253  coprmdvds1  11351  qredeq  11356  fiinopn  11601  bj-intabssel  11689
  Copyright terms: Public domain W3C validator