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  1652  mo3h  2050  necon1bidc  2358  necon4aidc  2374  ceqex  2807  ssdisj  3414  ralidm  3458  exmid1dc  4118  rexxfrd  4379  sucprcreg  4459  imain  5200  f0rn0  5312  funopfv  5454  mpteqb  5504  funfvima  5642  fliftfun  5690  iinerm  6494  eroveu  6513  th3qlem1  6524  updjudhf  6957  elni2  7115  genpdisj  7324  lttri3  7837  zfz1iso  10577  cau3lem  10879  maxleast  10978  rexanre  10985  climcau  11109  summodc  11145  mertenslem2  11298  divgcdcoprmex  11772  prmind2  11790  opnneiid  12322  txuni2  12414  txbas  12416  txbasval  12425  txlm  12437  blin2  12590  tgqioo  12705
  Copyright terms: Public domain W3C validator