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

Theorem syl5bir 152
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 132 . 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 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:  3imtr3g  203  19.37-1  1637  mo3h  2030  necon1bidc  2337  necon4aidc  2353  ceqex  2786  ssdisj  3389  ralidm  3433  exmid1dc  4093  rexxfrd  4354  sucprcreg  4434  imain  5175  f0rn0  5287  funopfv  5429  mpteqb  5479  funfvima  5617  fliftfun  5665  iinerm  6469  eroveu  6488  th3qlem1  6499  updjudhf  6932  elni2  7090  genpdisj  7299  lttri3  7812  zfz1iso  10552  cau3lem  10854  maxleast  10953  rexanre  10960  climcau  11084  summodc  11120  mertenslem2  11273  divgcdcoprmex  11710  prmind2  11728  opnneiid  12260  txuni2  12352  txbas  12354  txbasval  12363  txlm  12375  blin2  12528  tgqioo  12643
  Copyright terms: Public domain W3C validator