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

Theorem syl6bb 185
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6bb.1
syl6bb.2
Assertion
Ref Expression
syl6bb

Proof of Theorem syl6bb
StepHypRef Expression
1 syl6bb.1 . 2
2 syl6bb.2 . . 3
32a1i 9 . 2
41, 3bitrd 177 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  syl6rbb  186  syl6bbr  187  3bitr3g  211  bibi2i  216  ibibr  235  imandc  785  pm5.75  868  xordidc  1287  19.17  1445  alexdc  1507  nf4dc  1557  abeq2d  2147  cbvralf  2521  cbvrexf  2522  cbvreu  2525  cbvrab  2549  ceqsralt  2575  ralab2  2699  rexab2  2701  euxfr2dc  2720  reu7  2730  reu8  2731  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  ralss  3000  rexss  3001  prssg  3512  2ralunsn  3560  eluniab  3583  elintab  3617  dfiun2g  3680  dfiin2g  3681  cbvopab1  3821  cbvmpt  3842  axsep2  3867  bnd2  3917  opeqsn  3980  reusv3  4158  tfisi  4253  opeliunxp  4338  eliunxp  4418  relop  4429  eldm2g  4474  reldm0  4496  relrn0  4537  xpmlem  4687  elxp5  4752  cnvpom  4803  cbviota  4815  iota1  4824  sniota  4837  fncnv  4908  fnres  4958  brprcneu  5114  fnopfvb  5158  fvelrnb  5164  fvelimab  5172  fvopab3g  5188  eqfnfv3  5210  eqfnfv2f  5212  fvreseq  5214  fnreseql  5220  rexsupp  5234  respreima  5238  rexrn  5247  ralrn  5248  f1ompt  5263  fsn  5278  fconstfvm  5322  fconst3m  5323  fconst4m  5324  rexima  5337  ralima  5338  dff13  5350  foeqcnvco  5373  fliftfun  5379  isocnv  5394  isoini  5400  f1oiso  5408  cbvriota  5421  eusvobj2  5441  oprabid  5480  eloprabga  5533  resoprab  5539  eqfnov  5549  eqfnov2  5550  ov6g  5580  funimassov  5592  ovelimab  5593  caovord2  5615  releldm2  5753  dfoprab4  5760  xporderlem  5793  poxp  5794  mpt2xopovel  5797  brtpos2  5807  brtpos0  5808  rntpos  5813  dftpos3  5818  tpostpos  5820  tpossym  5832  tposoprab  5836  frecsuclem3  5929  erth2  6087  qliftfun  6124  erovlem  6134  ecopovsym  6138  ecopovsymg  6141  th3qlem1  6144  dom2lem  6188  xpdom2  6241  ssfiexmid  6254  ltexpi  6321  ordpipqqs  6358  ltexnqq  6391  enq0enq  6413  enq0sym  6414  enq0tr  6416  nqnq0pi  6420  genipv  6491  genprndl  6504  genprndu  6505  genpdisj  6506  genpassl  6507  genpassu  6508  addcomprg  6552  mulcomprg  6554  ltexprlemm  6572  ltexprlemdisj  6578  ltsrprg  6635  mulgt0sr  6664  elreal2  6688  ltresr  6696  ltresr2  6697  axprecex  6724  axpre-ltadd  6730  axpre-mulgt0  6731  axpre-mulext  6732  subcan2  6992  negcon1  7019  negcon2  7020  lt0neg1  7218  lt0neg2  7219  le0neg1  7220  le0neg2  7221  reapirr  7321  reapmul1  7339  reapneg  7341  remulext1  7343  apti  7366  negap0  7372  divmulap2  7397  reclt1  7603  recgt1  7604  addltmul  7898  elznn0  7996  zapne  8051  zltlen  8055  nn0lt10b  8057  nn0lt2  8058  eluz1  8213  raluz  8257  rexuz  8259  cnref1o  8317  rpnegap  8350  ltxr  8425  xlt0neg1  8481  xlt0neg2  8482  xle0neg1  8483  xle0neg2  8484  elixx1  8496  elixx3g  8500  elioo2  8520  icc0r  8525  elicc4  8539  elioopnf  8566  elioomnf  8567  iooneg  8586  iccneg  8587  iccshftr  8592  iccshftl  8594  iccdil  8596  icccntr  8598  iccf1o  8602  elfz1  8609  0fz1  8639  fzpr  8669  fzdifsuc  8673  uzsplit  8684  elfzm1b  8690  elfzp12  8691  fznn0  8704  expap0  8899  bernneq  8982
  Copyright terms: Public domain W3C validator