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  1609  mo3h  2001  necon1bidc  2307  necon4aidc  2323  ceqex  2744  ssdisj  3339  ralidm  3382  rexxfrd  4285  sucprcreg  4365  imain  5096  f0rn0  5205  funopfv  5344  mpteqb  5393  funfvima  5526  fliftfun  5575  iinerm  6364  eroveu  6383  th3qlem1  6394  updjudhf  6770  elni2  6873  genpdisj  7082  lttri3  7565  zfz1iso  10246  cau3lem  10547  maxleast  10646  rexanre  10653  climcau  10736  isummo  10773  mertenslem2  10930  divgcdcoprmex  11362  prmind2  11380
  Copyright terms: Public domain W3C validator