Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl6bbr GIF version

Theorem syl6bbr 197
 Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6bbr.1 (𝜑 → (𝜓𝜒))
syl6bbr.2 (𝜃𝜒)
Assertion
Ref Expression
syl6bbr (𝜑 → (𝜓𝜃))

Proof of Theorem syl6bbr
StepHypRef Expression
1 syl6bbr.1 . 2 (𝜑 → (𝜓𝜒))
2 syl6bbr.2 . . 3 (𝜃𝜒)
32bicomi 131 . 2 (𝜒𝜃)
41, 3syl6bb 195 1 (𝜑 → (𝜓𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  3bitr4g  222  bibi2i  226  equsalh  1704  eueq3dc  2858  sbcel12g  3017  sbceqg  3018  sbcnel12g  3019  reldisj  3414  r19.3rm  3451  rabxp  4576  elrng  4730  iss  4865  eliniseg  4909  fcnvres  5306  dffv3g  5417  funimass4  5472  fndmdif  5525  fneqeql  5528  funimass3  5536  elrnrexdmb  5560  dff4im  5566  fconst4m  5640  elunirn  5667  riota1  5748  riota2df  5750  f1ocnvfv3  5763  eqfnov  5877  caoftrn  6007  mpoxopovel  6138  rntpos  6154  ordgt0ge1  6332  iinerm  6501  erinxp  6503  qliftfun  6511  mapdm0  6557  elfi2  6860  fifo  6868  inl11  6950  ctssdccl  6996  isomnimap  7009  ismkvmap  7028  iswomnimap  7038  omniwomnimkv  7039  pr2nelem  7054  indpi  7164  genpdflem  7329  genpdisj  7345  genpassl  7346  genpassu  7347  ltnqpri  7416  ltpopr  7417  ltexprlemm  7422  ltexprlemdisj  7428  ltexprlemloc  7429  ltrennb  7676  letri3  7859  letr  7861  ltneg  8238  leneg  8241  reapltxor  8365  apsym  8382  suprnubex  8725  suprleubex  8726  elnnnn0  9034  zrevaddcl  9118  znnsub  9119  znn0sub  9133  prime  9164  eluz2  9346  eluz2b1  9409  nn01to3  9423  qrevaddcl  9450  xrletri3  9602  xrletr  9605  iccid  9722  elicopnf  9766  fzsplit2  9844  fzsn  9860  fzpr  9871  uzsplit  9886  fvinim0ffz  10032  lt2sqi  10394  le2sqi  10395  abs00ap  10848  iooinsup  11060  mertenslem2  11319  gcddiv  11720  algcvgblem  11743  isprm3  11812  eltg2b  12239  discld  12321  opnssneib  12341  restbasg  12353  ssidcn  12395  cnptoprest2  12425  lmss  12431  txrest  12461  txlm  12464  imasnopn  12484  bldisj  12586  xmeter  12621  bl2ioo  12727  limcdifap  12816  bj-sseq  13106  nnti  13298  pw1nct  13305
 Copyright terms: Public domain W3C validator