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

Theorem syl6rbbr 198
 Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
Hypotheses
Ref Expression
syl6rbbr.1 (𝜑 → (𝜓𝜒))
syl6rbbr.2 (𝜃𝜒)
Assertion
Ref Expression
syl6rbbr (𝜑 → (𝜃𝜓))

Proof of Theorem syl6rbbr
StepHypRef Expression
1 syl6rbbr.1 . 2 (𝜑 → (𝜓𝜒))
2 syl6rbbr.2 . . 3 (𝜃𝜒)
32bicomi 131 . 2 (𝜒𝜃)
41, 3syl6rbb 196 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:  imimorbdc  881  baib  904  pm5.6dc  911  xornbidc  1369  mo2dc  2054  reu8  2880  sbc6g  2933  dfss4st  3309  r19.28m  3452  r19.45mv  3456  r19.44mv  3457  r19.27m  3458  ralsnsg  3563  ralsns  3564  iunconstm  3824  iinconstm  3825  exmidsssnc  4129  unisucg  4339  relsng  4645  funssres  5168  fncnv  5192  dff1o5  5379  funimass4  5475  fneqeql2  5532  fnniniseg2  5546  rexsupp  5547  unpreima  5548  dffo3  5570  funfvima  5652  dff13  5672  f1eqcocnv  5695  fliftf  5703  isocnv2  5716  eloprabga  5861  mpo2eqb  5883  opabex3d  6022  opabex3  6023  elxp6  6070  elxp7  6071  sbthlemi5  6852  sbthlemi6  6853  genpdflem  7334  ltnqpr  7420  ltexprlemloc  7434  xrlenlt  7848  negcon2  8034  dfinfre  8733  sup3exmid  8734  elznn  9089  zq  9440  rpnegap  9496  modqmuladdnn0  10165  shftdm  10618  rexfiuz  10785  rexanuz2  10787  sumsplitdc  11225  fsum2dlemstep  11227  odd2np1  11593  divalgb  11645  infssuzex  11665  isprm4  11823  ctiunctlemudc  11973  tx1cn  12464  tx2cn  12465  cnbl0  12729  cnblcld  12730  reopnap  12733  pilem1  12894  sinq34lt0t  12946
 Copyright terms: Public domain W3C validator