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

Theorem syl5bir 151
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bir.1  |-  ( ps  <->  ph )
syl5bir.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
syl5bir  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5bir
StepHypRef Expression
1 syl5bir.1 . . 3  |-  ( ps  <->  ph )
21biimpri 131 . 2  |-  ( ph  ->  ps )
3 syl5bir.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  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:  3imtr3g  202  19.37-1  1605  mo3h  1995  necon1bidc  2298  necon4aidc  2314  ceqex  2723  ssdisj  3307  ralidm  3349  rexxfrd  4221  sucprcreg  4300  imain  5012  funopfv  5245  mpteqb  5293  funfvima  5422  fliftfun  5467  iinerm  6244  eroveu  6263  th3qlem1  6274  elni2  6566  genpdisj  6775  lttri3  7258  cau3lem  10138  maxleast  10237  rexanre  10244  climcau  10322  divgcdcoprmex  10628  prmind2  10646
  Copyright terms: Public domain W3C validator