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

Theorem syl6bbr 196
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 130 . 2 (𝜒𝜃)
41, 3syl6bb 194 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3bitr4g  221  bibi2i  225  equsalh  1656  eueq3dc  2777  sbcel12g  2932  sbceqg  2933  sbcnel12g  2934  reldisj  3316  r19.3rm  3351  rabxp  4436  elrng  4585  iss  4715  eliniseg  4757  fcnvres  5142  dffv3g  5249  funimass4  5300  fndmdif  5349  fneqeql  5352  funimass3  5360  elrnrexdmb  5384  dff4im  5390  fconst4m  5457  elunirn  5485  riota1  5565  riota2df  5567  f1ocnvfv3  5580  eqfnov  5686  caoftrn  5815  mpt2xopovel  5938  rntpos  5954  ordgt0ge1  6131  iinerm  6294  erinxp  6296  qliftfun  6304  mapdm0  6350  isomnimap  6698  pr2nelem  6722  indpi  6804  genpdflem  6969  genpdisj  6985  genpassl  6986  genpassu  6987  ltnqpri  7056  ltpopr  7057  ltexprlemm  7062  ltexprlemdisj  7068  ltexprlemloc  7069  ltrennb  7294  letri3  7469  letr  7471  ltneg  7843  leneg  7846  reapltxor  7966  apsym  7983  suprnubex  8308  suprleubex  8309  elnnnn0  8608  zrevaddcl  8696  znnsub  8697  znn0sub  8711  prime  8741  eluz2  8920  eluz2b1  8983  nn01to3  8997  qrevaddcl  9024  xrletri3  9165  xrletr  9168  iccid  9238  elicopnf  9282  fzsplit2  9359  fzsn  9374  fzpr  9384  uzsplit  9399  fvinim0ffz  9541  lt2sqi  9879  le2sqi  9880  abs00ap  10322  gcddiv  10788  algcvgblem  10811  isprm3  10880  bj-sseq  11035  nnti  11234
  Copyright terms: Public domain W3C validator