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  1793  cbvexdh  1919  repizf2  4148  issref  4993  fnun  5304  ovigg  5973  tfrlem9  6298  tfri3  6346  ordge1n0im  6415  nntri3or  6472  updjud  7059  axprecex  7842  peano5nnnn  7854  peano5nni  8881  zeo  9317  nn0ind-raph  9329  fzm1  10056  fzind2  10195  fzfig  10386  bcpasc  10700  climrecvg1n  11311  oddnn02np1  11839  oddge22np1  11840  evennn02n  11841  evennn2n  11842  gcdaddm  11939  coprmdvds1  12045  qredeq  12050  fiinopn  12796  zabsle1  13694  bj-intabssel  13824  triap  14061
  Copyright terms: Public domain W3C validator