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

Theorem syl5bb 191
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bb.1 (𝜑𝜓)
syl5bb.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5bb (𝜒 → (𝜑𝜃))

Proof of Theorem syl5bb
StepHypRef Expression
1 syl5bb.1 . . 3 (𝜑𝜓)
21a1i 9 . 2 (𝜒 → (𝜑𝜓))
3 syl5bb.2 . 2 (𝜒 → (𝜓𝜃))
42, 3bitrd 187 1 (𝜒 → (𝜑𝜃))
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  8381  conjmulap  8457  rerecclap  8458  creui  8686  peano2nn  8700  nndiv  8729  elznn0  9037  eqreznegel  9374  negelrp  9443  ltxr  9530  divelunit  9753  iccf1o  9755  elfz2  9765  elfzp1  9820  fzdifsuc  9829  fznn  9837  fzosplitsni  9980  fvinim0ffz  9986  frec2uzisod  10148  sq11i  10350  cjreb  10606  rexfiuz  10729  cau3lem  10854  pwm1geoserap1  11245  mertensabs  11274  divides  11422  dvdsabseq  11472  odd2np1  11497  oddm1even  11499  modremain  11553  infssuzex  11569  bezoutlemnewy  11611  bezoutlemstep  11612  bezoutlemmain  11613  bezoutlema  11614  bezoutlemb  11615  isprm2  11725  isprm4  11727  dvdsnprmd  11733  istopg  12093  basgen2  12177  isnei  12240  restdis  12280  iscn  12293  iscnp  12295  lmbr2  12310  lmbrf  12311  txcn  12371  cnmpt21  12387  blres  12530  isxms2  12548  metrest  12602  metcnp  12608  txmetcnp  12614  txmetcn  12615  cnblcld  12631  reopnap  12634  bj-indeq  13054  bj-nn0sucALT  13103
  Copyright terms: Public domain W3C validator