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

Theorem syl5bb 190
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 186 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:  syl5rbb  191  syl5bbr  192  3bitr4g  221  imim21b  250  pm5.17dc  846  dn1dc  904  bilukdc  1330  nf4dc  1603  sbal1  1923  abbi  2198  necon3abid  2290  necon3bid  2292  necon1abiidc  2311  r19.21t  2444  ceqsralt  2640  ceqsrexv  2738  ceqsrex2v  2740  elab2g  2753  elrabf  2760  eueq2dc  2779  euxfrdc  2792  eqreu  2798  reu8  2802  ru  2828  sbcralt  2904  sbcrext  2905  sbcne12g  2938  csbnestgf  2969  dfss4st  3221  rexsng  3469  ralprg  3478  rexprg  3479  difsn  3559  opthpr  3601  ralunsn  3626  dfiin2g  3748  iunxsng  3790  elpwuni  3799  pwnss  3971  exmid01  4008  opelopabt  4065  opelopabga  4066  brabga  4067  elsucg  4207  elsuc2g  4208  brab2a  4461  opeliunxp  4463  posng  4480  brab2ga  4483  csbdmg  4600  elrnmpt1  4656  elrnmptg  4657  poleloe  4800  elxp4  4886  elxp5  4887  cnvpom  4941  sbcfung  5006  dffun8  5010  fncnv  5047  fununi  5049  fnssresb  5093  fnimaeq0  5102  funcocnv2  5243  dffn5im  5315  funimass4  5320  fnsnfv  5328  dmfco  5337  fndmdif  5369  fndmin  5371  unpreima  5389  respreima  5392  fsn2  5436  fnressn  5448  fressnfv  5449  elunirn  5508  dff13  5510  fliftel  5535  isoini  5560  f1oiso  5568  acexmid  5614  eloprabga  5694  resoprab2  5701  ralrnmpt2  5718  rexrnmpt2  5719  ovid  5720  ov  5723  ovg  5742  ofrfval2  5830  fmpt2x  5929  1stconst  5945  2ndconst  5946  f1od2  5959  isprmpt2  5964  brtpos2  5972  dfsmo2  6008  frecabcl  6120  brdifun  6273  eqerlem  6277  brecop  6336  erovlem  6338  mapsn  6401  map1  6483  xpsnen  6491  xpdom2  6501  xpf1o  6514  supubti  6641  infglbti  6667  ltpiord  6825  nlt1pig  6847  elinp  6980  ltdfpr  7012  genpassl  7030  genpassu  7031  1idprl  7096  1idpru  7097  gt0srpr  7241  peano2nnnn  7337  recidpirq  7342  axprecex  7362  xrlenlt  7498  addsubeq4  7644  renegcl  7690  lesub0  7904  recexaplem2  8063  conjmulap  8138  rerecclap  8139  creui  8358  peano2nn  8372  nndiv  8400  elznn0  8701  eqreznegel  9034  ltxr  9181  divelunit  9354  iccf1o  9356  elfz2  9366  elfzp1  9419  fzdifsuc  9428  fznn  9436  fzosplitsni  9577  fvinim0ffz  9583  frec2uzisod  9745  sq11i  9946  cjreb  10199  rexfiuz  10321  cau3lem  10446  divides  10704  dvdsabseq  10754  odd2np1  10779  oddm1even  10781  modremain  10835  infssuzex  10851  bezoutlemnewy  10891  bezoutlemstep  10892  bezoutlemmain  10893  bezoutlema  10894  bezoutlemb  10895  isprm2  11005  isprm4  11007  dvdsnprmd  11013  bj-indeq  11293  bj-nn0sucALT  11342
  Copyright terms: Public domain W3C validator