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  770  pm5.75  853  xordidc  1271  19.17  1424  alexdc  1486  nf4dc  1536  abeq2d  2126  cbvralf  2499  cbvrexf  2500  cbvreu  2503  cbvrab  2527  ceqsralt  2552  ralab2  2676  rexab2  2678  euxfr2dc  2697  reu7  2707  reu8  2708  cbvralcsf  2879  cbvrexcsf  2880  cbvreucsf  2881  cbvrabcsf  2882  ralss  2977  rexss  2978  prssg  3487  2ralunsn  3535  eluniab  3558  elintab  3592  dfiun2g  3655  dfiin2g  3656  cbvopab1  3796  cbvmpt  3817  axsep2  3842  bnd2  3892  opeqsn  3955  reusv3  4133  tfisi  4228  opeliunxp  4313  eliunxp  4393  relop  4404  eldm2g  4449  reldm0  4471  relrn0  4512  xpmlem  4662  elxp5  4727  cnvpom  4778  cbviota  4790  iota1  4799  sniota  4812  fncnv  4882  fnres  4932  brprcneu  5087  fnopfvb  5131  fvelrnb  5137  fvelimab  5145  fvopab3g  5161  eqfnfv3  5183  eqfnfv2f  5185  fvreseq  5187  fnreseql  5193  rexsupp  5207  respreima  5211  rexrn  5220  ralrn  5221  f1ompt  5236  fsn  5251  fconstfvm  5295  fconst3m  5296  fconst4m  5297  rexima  5310  ralima  5311  dff13  5323  foeqcnvco  5346  fliftfun  5352  isocnv  5367  isoini  5373  f1oiso  5381  cbvriota  5393  eusvobj2  5413  oprabid  5452  eloprabga  5505  resoprab  5511  eqfnov  5521  eqfnov2  5522  ov6g  5552  funimassov  5564  ovelimab  5565  caovord2  5587  releldm2  5725  dfoprab4  5732  xporderlem  5765  poxp  5766  mpt2xopovel  5769  brtpos2  5779  brtpos0  5780  rntpos  5785  dftpos3  5790  tpostpos  5792  tpossym  5804  tposoprab  5808  frecsuclem3  5897  erth2  6053  qliftfun  6090  erovlem  6100  ecopovsym  6104  ecopovsymg  6107  th3qlem1  6110  ltexpi  6186  ordpipqqs  6222  ltexnqq  6255  enq0enq  6275  enq0sym  6276  enq0tr  6278  nqnq0pi  6282  genipv  6352  genprndl  6365  genprndu  6366  genpdisj  6367  genpassl  6368  genpassu  6369  addcomprg  6406  mulcomprg  6408  ltexprlemm  6426  ltexprlemdisj  6432  ltsrprg  6488  mulgt0sr  6517  elreal2  6540  ltresr  6548  ltresr2  6549  axprecex  6572  axpre-ltadd  6578  axpre-mulgt0  6579  axpre-mulext  6580  subcan2  6838  negcon1  6865  negcon2  6866  lt0neg1  7064  lt0neg2  7065  le0neg1  7066  le0neg2  7067  reapirr  7167  reapmul1  7185  reapneg  7187  remulext1  7189  apti  7212  negap0  7218  divmulap2  7243  reclt1  7448  recgt1  7449  addltmul  7742  elznn0  7837  zapne  7886  zltlen  7888  nn0lt10b  7889  nn0lt2  7890  rpnegap  8099  ltxr  8174  xlt0neg1  8230  xlt0neg2  8231  xle0neg1  8232  xle0neg2  8233  elixx1  8245  elixx3g  8249  elioo2  8269  icc0r  8274  elicc4  8288  elioopnf  8315  elioomnf  8316  iooneg  8335  iccneg  8336  iccshftr  8341  iccshftl  8343  iccdil  8345  icccntr  8347  iccf1o  8351
  Copyright terms: Public domain W3C validator