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

Theorem syl5bb 190
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 186 1 (𝜒 → (𝜑𝜃))
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  2639  ceqsrexv  2737  ceqsrex2v  2739  elab2g  2752  elrabf  2759  eueq2dc  2778  euxfrdc  2791  eqreu  2797  reu8  2801  ru  2827  sbcralt  2903  sbcrext  2904  sbcne12g  2937  csbnestgf  2967  dfss4st  3218  rexsng  3461  ralprg  3470  rexprg  3471  difsn  3551  opthpr  3593  ralunsn  3618  dfiin2g  3740  iunxsng  3782  elpwuni  3791  pwnss  3962  exmid01  3999  opelopabt  4056  opelopabga  4057  brabga  4058  elsucg  4198  elsuc2g  4199  brab2a  4452  opeliunxp  4454  posng  4471  brab2ga  4474  csbdmg  4591  elrnmpt1  4647  elrnmptg  4648  poleloe  4789  elxp4  4875  elxp5  4876  cnvpom  4930  sbcfung  4995  dffun8  4999  fncnv  5036  fununi  5038  fnssresb  5082  fnimaeq0  5091  funcocnv2  5229  dffn5im  5298  funimass4  5303  fnsnfv  5311  dmfco  5320  fndmdif  5352  fndmin  5354  unpreima  5372  respreima  5375  fsn2  5416  fnressn  5428  fressnfv  5429  elunirn  5488  dff13  5490  fliftel  5515  isoini  5539  f1oiso  5547  acexmid  5593  eloprabga  5673  resoprab2  5680  ralrnmpt2  5697  rexrnmpt2  5698  ovid  5699  ov  5702  ovg  5721  ofrfval2  5809  fmpt2x  5908  1stconst  5924  2ndconst  5925  f1od2  5938  isprmpt2  5943  brtpos2  5951  dfsmo2  5987  frecabcl  6099  brdifun  6252  eqerlem  6256  brecop  6315  erovlem  6317  mapsn  6380  map1  6462  xpsnen  6470  xpdom2  6480  xpf1o  6493  supubti  6615  infglbti  6641  ltpiord  6799  nlt1pig  6821  elinp  6954  ltdfpr  6986  genpassl  7004  genpassu  7005  1idprl  7070  1idpru  7071  gt0srpr  7215  peano2nnnn  7311  recidpirq  7316  axprecex  7336  xrlenlt  7472  addsubeq4  7618  renegcl  7664  lesub0  7878  recexaplem2  8037  conjmulap  8112  rerecclap  8113  creui  8332  peano2nn  8346  nndiv  8374  elznn0  8675  eqreznegel  9008  ltxr  9155  divelunit  9328  iccf1o  9330  elfz2  9340  elfzp1  9393  fzdifsuc  9402  fznn  9410  fzosplitsni  9549  fvinim0ffz  9555  frec2uzisod  9717  sq11i  9895  cjreb  10141  rexfiuz  10263  cau3lem  10388  divides  10592  dvdsabseq  10642  odd2np1  10667  oddm1even  10669  modremain  10723  infssuzex  10739  bezoutlemnewy  10779  bezoutlemstep  10780  bezoutlemmain  10781  bezoutlema  10782  bezoutlemb  10783  isprm2  10893  isprm4  10895  dvdsnprmd  10901  bj-indeq  11181  bj-nn0sucALT  11230
  Copyright terms: Public domain W3C validator