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  bitr3id  193  3bitr4g  222  imim21b  251  pm5.17dc  890  dn1dc  945  bilukdc  1375  nf4dc  1649  sbal1  1978  abbi  2254  necon3abid  2348  necon3bid  2350  necon1abiidc  2369  r19.21t  2508  ceqsralt  2714  ceqsrexv  2816  ceqsrex2v  2818  elab2g  2832  elrabf  2839  eueq2dc  2858  euxfrdc  2871  eqreu  2877  reu8  2881  ru  2909  sbcralt  2986  sbcrext  2987  sbcne12g  3021  csbnestgf  3053  dfss4st  3310  rexsng  3568  ralprg  3578  rexprg  3579  difsn  3661  opthpr  3703  ralunsn  3728  dfiin2g  3850  iunxsng  3892  iunxsngf  3894  elpwuni  3906  pwnss  4087  exmid01  4125  opelopabt  4188  opelopabga  4189  brabga  4190  elsucg  4330  elsuc2g  4331  brab2a  4596  opeliunxp  4598  posng  4615  brab2ga  4618  csbdmg  4737  elrnmpt1  4794  elrnmptg  4795  poleloe  4942  elxp4  5030  elxp5  5031  cnvpom  5085  sbcfung  5151  dffun8  5155  fncnv  5193  fununi  5195  fnssresb  5239  fnimaeq0  5248  funcocnv2  5396  dffn5im  5471  funimass4  5476  fnsnfv  5484  dmfco  5493  fndmdif  5529  fndmin  5531  unpreima  5549  respreima  5552  fsn2  5598  fnressn  5610  fressnfv  5611  elunirn  5671  dff13  5673  fliftel  5698  isoini  5723  f1oiso  5731  acexmid  5777  eloprabga  5862  resoprab2  5872  ralrnmpo  5889  rexrnmpo  5890  ovid  5891  ov  5894  ovg  5913  ofrfval2  6002  fmpox  6102  1stconst  6122  2ndconst  6123  f1od2  6136  rbropapd  6143  brtpos2  6152  dfsmo2  6188  frecabcl  6300  brdifun  6460  eqerlem  6464  brecop  6523  erovlem  6525  mapsn  6588  mptelixpg  6632  map1  6710  xpsnen  6719  xpdom2  6729  xpf1o  6742  supubti  6890  infglbti  6916  ctssdccl  7000  ltpiord  7147  nlt1pig  7169  elinp  7302  ltdfpr  7334  genpassl  7352  genpassu  7353  1idprl  7418  1idpru  7419  gt0srpr  7576  mappsrprg  7632  map2psrprg  7633  peano2nnnn  7681  recidpirq  7686  axprecex  7708  xrlenlt  7849  addsubeq4  7997  renegcl  8043  lesub0  8261  recexaplem2  8433  conjmulap  8509  rerecclap  8510  creui  8738  peano2nn  8752  nndiv  8781  elznn0  9089  eqreznegel  9429  negelrp  9500  ltxr  9588  divelunit  9811  iccf1o  9813  elfz2  9824  elfzp1  9879  fzdifsuc  9888  fznn  9896  fzosplitsni  10039  fvinim0ffz  10045  frec2uzisod  10207  sq11i  10409  cjreb  10666  rexfiuz  10789  cau3lem  10914  pwm1geoserap1  11305  mertensabs  11334  divides  11522  dvdsabseq  11572  odd2np1  11597  oddm1even  11599  modremain  11653  infssuzex  11669  bezoutlemnewy  11711  bezoutlemstep  11712  bezoutlemmain  11713  bezoutlema  11714  bezoutlemb  11715  isprm2  11825  isprm4  11827  dvdsnprmd  11833  istopg  12196  basgen2  12280  isnei  12343  restdis  12383  iscn  12396  iscnp  12398  lmbr2  12413  lmbrf  12414  txcn  12474  cnmpt21  12490  blres  12633  isxms2  12651  metrest  12705  metcnp  12711  txmetcnp  12717  txmetcn  12718  cnblcld  12734  reopnap  12737  ioocosf1o  12974  bj-indeq  13281  bj-nn0sucALT  13330  apdiff  13399
  Copyright terms: Public domain W3C validator