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  779  pm5.75  857  xordidc  1273  19.17  1430  alexdc  1492  nf4dc  1542  abeq2d  2132  cbvralf  2505  cbvrexf  2506  cbvreu  2509  cbvrab  2533  ceqsralt  2558  ralab2  2682  rexab2  2684  euxfr2dc  2703  reu7  2713  reu8  2714  cbvralcsf  2885  cbvrexcsf  2886  cbvreucsf  2887  cbvrabcsf  2888  ralss  2983  rexss  2984  prssg  3495  2ralunsn  3543  eluniab  3566  elintab  3600  dfiun2g  3663  dfiin2g  3664  cbvopab1  3804  cbvmpt  3825  axsep2  3850  bnd2  3900  opeqsn  3963  reusv3  4142  tfisi  4237  opeliunxp  4322  eliunxp  4402  relop  4413  eldm2g  4458  reldm0  4480  relrn0  4521  xpmlem  4671  elxp5  4736  cnvpom  4787  cbviota  4799  iota1  4808  sniota  4821  fncnv  4891  fnres  4941  brprcneu  5096  fnopfvb  5140  fvelrnb  5146  fvelimab  5154  fvopab3g  5170  eqfnfv3  5192  eqfnfv2f  5194  fvreseq  5196  fnreseql  5202  rexsupp  5216  respreima  5220  rexrn  5229  ralrn  5230  f1ompt  5245  fsn  5260  fconstfvm  5304  fconst3m  5305  fconst4m  5306  rexima  5319  ralima  5320  dff13  5332  foeqcnvco  5355  fliftfun  5361  isocnv  5376  isoini  5382  f1oiso  5390  cbvriota  5402  eusvobj2  5422  oprabid  5461  eloprabga  5514  resoprab  5520  eqfnov  5530  eqfnov2  5531  ov6g  5561  funimassov  5573  ovelimab  5574  caovord2  5596  releldm2  5734  dfoprab4  5741  xporderlem  5774  poxp  5775  mpt2xopovel  5778  brtpos2  5788  brtpos0  5789  rntpos  5794  dftpos3  5799  tpostpos  5801  tpossym  5813  tposoprab  5817  frecsuclem3  5906  erth2  6062  qliftfun  6099  erovlem  6109  ecopovsym  6113  ecopovsymg  6116  th3qlem1  6119  ltexpi  6197  ordpipqqs  6233  ltexnqq  6266  enq0enq  6286  enq0sym  6287  enq0tr  6289  nqnq0pi  6293  genipv  6363  genprndl  6376  genprndu  6377  genpdisj  6378  genpassl  6379  genpassu  6380  addcomprg  6417  mulcomprg  6419  ltexprlemm  6437  ltexprlemdisj  6443  ltsrprg  6494  mulgt0sr  6522  elreal2  6542  ltresr  6550  ltresr2  6551  axprecex  6574  axpre-ltadd  6579  axpre-mulgt0  6580  subcan2  6822  negcon1  6849  negcon2  6850
  Copyright terms: Public domain W3C validator