ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl6bb Structured version   GIF 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  6503  genprndu  6504  genpdisj  6505  genpassl  6506  genpassu  6507  addcomprg  6553  mulcomprg  6555  ltexprlemm  6573  ltexprlemdisj  6579  ltsrprg  6655  mulgt0sr  6684  elreal2  6708  ltresr  6716  ltresr2  6717  axprecex  6744  axpre-ltadd  6750  axpre-mulgt0  6751  axpre-mulext  6752  subcan2  7012  negcon1  7039  negcon2  7040  lt0neg1  7238  lt0neg2  7239  le0neg1  7240  le0neg2  7241  reapirr  7341  reapmul1  7359  reapneg  7361  remulext1  7363  apti  7386  negap0  7392  divmulap2  7417  reclt1  7623  recgt1  7624  addltmul  7918  elznn0  8016  zapne  8071  zltlen  8075  nn0lt10b  8077  nn0lt2  8078  eluz1  8233  raluz  8277  rexuz  8279  cnref1o  8337  rpnegap  8370  ltxr  8445  xlt0neg1  8501  xlt0neg2  8502  xle0neg1  8503  xle0neg2  8504  elixx1  8516  elixx3g  8520  elioo2  8540  icc0r  8545  elicc4  8559  elioopnf  8586  elioomnf  8587  iooneg  8606  iccneg  8607  iccshftr  8612  iccshftl  8614  iccdil  8616  icccntr  8618  iccf1o  8622  elfz1  8629  0fz1  8659  fzpr  8689  fzdifsuc  8693  uzsplit  8704  elfzm1b  8710  elfzp12  8711  fznn0  8724  expap0  8919  bernneq  9002
  Copyright terms: Public domain W3C validator