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  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  3467  ralprg  3476  rexprg  3477  difsn  3557  opthpr  3599  ralunsn  3624  dfiin2g  3746  iunxsng  3788  elpwuni  3797  pwnss  3968  exmid01  4005  opelopabt  4062  opelopabga  4063  brabga  4064  elsucg  4204  elsuc2g  4205  brab2a  4458  opeliunxp  4460  posng  4477  brab2ga  4480  csbdmg  4597  elrnmpt1  4653  elrnmptg  4654  poleloe  4795  elxp4  4881  elxp5  4882  cnvpom  4936  sbcfung  5001  dffun8  5005  fncnv  5042  fununi  5044  fnssresb  5088  fnimaeq0  5097  funcocnv2  5235  dffn5im  5307  funimass4  5312  fnsnfv  5320  dmfco  5329  fndmdif  5361  fndmin  5363  unpreima  5381  respreima  5384  fsn2  5428  fnressn  5440  fressnfv  5441  elunirn  5500  dff13  5502  fliftel  5527  isoini  5552  f1oiso  5560  acexmid  5606  eloprabga  5686  resoprab2  5693  ralrnmpt2  5710  rexrnmpt2  5711  ovid  5712  ov  5715  ovg  5734  ofrfval2  5822  fmpt2x  5921  1stconst  5937  2ndconst  5938  f1od2  5951  isprmpt2  5956  brtpos2  5964  dfsmo2  6000  frecabcl  6112  brdifun  6265  eqerlem  6269  brecop  6328  erovlem  6330  mapsn  6393  map1  6475  xpsnen  6483  xpdom2  6493  xpf1o  6506  supubti  6631  infglbti  6657  ltpiord  6815  nlt1pig  6837  elinp  6970  ltdfpr  7002  genpassl  7020  genpassu  7021  1idprl  7086  1idpru  7087  gt0srpr  7231  peano2nnnn  7327  recidpirq  7332  axprecex  7352  xrlenlt  7488  addsubeq4  7634  renegcl  7680  lesub0  7894  recexaplem2  8053  conjmulap  8128  rerecclap  8129  creui  8348  peano2nn  8362  nndiv  8390  elznn0  8691  eqreznegel  9024  ltxr  9171  divelunit  9344  iccf1o  9346  elfz2  9356  elfzp1  9409  fzdifsuc  9418  fznn  9426  fzosplitsni  9567  fvinim0ffz  9573  frec2uzisod  9735  sq11i  9935  cjreb  10188  rexfiuz  10310  cau3lem  10435  divides  10665  dvdsabseq  10715  odd2np1  10740  oddm1even  10742  modremain  10796  infssuzex  10812  bezoutlemnewy  10852  bezoutlemstep  10853  bezoutlemmain  10854  bezoutlema  10855  bezoutlemb  10856  isprm2  10966  isprm4  10968  dvdsnprmd  10974  bj-indeq  11254  bj-nn0sucALT  11303
  Copyright terms: Public domain W3C validator