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

Theorem syl5bb 191
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bb.1  |-  ( ph  <->  ps )
syl5bb.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5bb  |-  ( ch 
->  ( ph  <->  th )
)

Proof of Theorem syl5bb
StepHypRef Expression
1 syl5bb.1 . . 3  |-  ( ph  <->  ps )
21a1i 9 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
3 syl5bb.2 . 2  |-  ( ch 
->  ( ps  <->  th )
)
42, 3bitrd 187 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:  syl5rbb  192  syl5bbr  193  3bitr4g  222  imim21b  251  pm5.17dc  874  dn1dc  929  bilukdc  1359  nf4dc  1633  sbal1  1955  abbi  2231  necon3abid  2324  necon3bid  2326  necon1abiidc  2345  r19.21t  2484  ceqsralt  2687  ceqsrexv  2789  ceqsrex2v  2791  elab2g  2804  elrabf  2811  eueq2dc  2830  euxfrdc  2843  eqreu  2849  reu8  2853  ru  2881  sbcralt  2957  sbcrext  2958  sbcne12g  2991  csbnestgf  3022  dfss4st  3279  rexsng  3535  ralprg  3544  rexprg  3545  difsn  3627  opthpr  3669  ralunsn  3694  dfiin2g  3816  iunxsng  3858  iunxsngf  3860  elpwuni  3872  pwnss  4053  exmid01  4091  opelopabt  4154  opelopabga  4155  brabga  4156  elsucg  4296  elsuc2g  4297  brab2a  4562  opeliunxp  4564  posng  4581  brab2ga  4584  csbdmg  4703  elrnmpt1  4760  elrnmptg  4761  poleloe  4908  elxp4  4996  elxp5  4997  cnvpom  5051  sbcfung  5117  dffun8  5121  fncnv  5159  fununi  5161  fnssresb  5205  fnimaeq0  5214  funcocnv2  5360  dffn5im  5435  funimass4  5440  fnsnfv  5448  dmfco  5457  fndmdif  5493  fndmin  5495  unpreima  5513  respreima  5516  fsn2  5562  fnressn  5574  fressnfv  5575  elunirn  5635  dff13  5637  fliftel  5662  isoini  5687  f1oiso  5695  acexmid  5741  eloprabga  5826  resoprab2  5836  ralrnmpo  5853  rexrnmpo  5854  ovid  5855  ov  5858  ovg  5877  ofrfval2  5966  fmpox  6066  1stconst  6086  2ndconst  6087  f1od2  6100  rbropapd  6107  brtpos2  6116  dfsmo2  6152  frecabcl  6264  brdifun  6424  eqerlem  6428  brecop  6487  erovlem  6489  mapsn  6552  mptelixpg  6596  map1  6674  xpsnen  6683  xpdom2  6693  xpf1o  6706  supubti  6854  infglbti  6880  ctssdccl  6964  ltpiord  7095  nlt1pig  7117  elinp  7250  ltdfpr  7282  genpassl  7300  genpassu  7301  1idprl  7366  1idpru  7367  gt0srpr  7524  mappsrprg  7580  map2psrprg  7581  peano2nnnn  7629  recidpirq  7634  axprecex  7656  xrlenlt  7797  addsubeq4  7945  renegcl  7991  lesub0  8209  recexaplem2  8380  conjmulap  8456  rerecclap  8457  creui  8682  peano2nn  8696  nndiv  8725  elznn0  9027  eqreznegel  9362  negelrp  9430  ltxr  9517  divelunit  9740  iccf1o  9742  elfz2  9752  elfzp1  9807  fzdifsuc  9816  fznn  9824  fzosplitsni  9967  fvinim0ffz  9973  frec2uzisod  10135  sq11i  10337  cjreb  10593  rexfiuz  10716  cau3lem  10841  pwm1geoserap1  11232  mertensabs  11261  divides  11407  dvdsabseq  11457  odd2np1  11482  oddm1even  11484  modremain  11538  infssuzex  11554  bezoutlemnewy  11596  bezoutlemstep  11597  bezoutlemmain  11598  bezoutlema  11599  bezoutlemb  11600  isprm2  11710  isprm4  11712  dvdsnprmd  11718  istopg  12077  basgen2  12161  isnei  12224  restdis  12264  iscn  12277  iscnp  12279  lmbr2  12294  lmbrf  12295  txcn  12355  cnmpt21  12371  blres  12514  isxms2  12532  metrest  12586  metcnp  12592  txmetcnp  12598  txmetcn  12599  cnblcld  12615  reopnap  12618  bj-indeq  13023  bj-nn0sucALT  13072
  Copyright terms: Public domain W3C validator