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  6414  enq0sym  6415  enq0tr  6417  nqnq0pi  6421  genipv  6492  genprndl  6504  genprndu  6505  genpdisj  6506  genpassl  6507  genpassu  6508  addcomprg  6554  mulcomprg  6556  ltexprlemm  6574  ltexprlemdisj  6580  ltsrprg  6675  mulgt0sr  6704  elreal2  6728  ltresr  6736  ltresr2  6737  axprecex  6764  axpre-ltadd  6770  axpre-mulgt0  6771  axpre-mulext  6772  subcan2  7032  negcon1  7059  negcon2  7060  lt0neg1  7258  lt0neg2  7259  le0neg1  7260  le0neg2  7261  reapirr  7361  reapmul1  7379  reapneg  7381  remulext1  7383  apti  7406  negap0  7412  divmulap2  7437  reclt1  7643  recgt1  7644  addltmul  7938  elznn0  8036  zapne  8091  zltlen  8095  nn0lt10b  8097  nn0lt2  8098  eluz1  8253  raluz  8297  rexuz  8299  cnref1o  8357  rpnegap  8390  ltxr  8465  xlt0neg1  8521  xlt0neg2  8522  xle0neg1  8523  xle0neg2  8524  elixx1  8536  elixx3g  8540  elioo2  8560  icc0r  8565  elicc4  8579  elioopnf  8606  elioomnf  8607  iooneg  8626  iccneg  8627  iccshftr  8632  iccshftl  8634  iccdil  8636  icccntr  8638  iccf1o  8642  elfz1  8649  0fz1  8679  fzpr  8709  fzdifsuc  8713  uzsplit  8724  elfzm1b  8730  elfzp12  8731  fznn0  8744  expap0  8939  bernneq  9022
  Copyright terms: Public domain W3C validator