MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6rbb Structured version   Visualization version   GIF version

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

Proof of Theorem syl6rbb
StepHypRef Expression
1 syl6rbb.1 . . 3 (𝜑 → (𝜓𝜒))
2 syl6rbb.2 . . 3 (𝜒𝜃)
31, 2syl6bb 274 . 2 (𝜑 → (𝜓𝜃))
43bicomd 211 1 (𝜑 → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195
This theorem is referenced by:  syl6rbbr  277  bibif  359  pm5.61  744  oranabs  896  necon4bid  2826  resopab2  5355  xpco  5578  funconstss  6228  xpopth  7075  map1  7898  ac6sfi  8066  supgtoreq  8236  rankr1bg  8526  alephsdom  8769  brdom7disj  9211  fpwwe2lem13  9320  nn0sub  11190  elznn0  11225  nn01to3  11613  supxrbnd1  11979  supxrbnd2  11980  rexuz3  13882  smueqlem  14996  qnumdenbi  15236  dfiso3  16202  lssne0  18718  pjfval2  19814  0top  20540  1stccn  21018  dscopn  22129  bcthlem1  22846  ovolgelb  22972  iblpos  23282  itgposval  23285  itgsubstlem  23532  sincosq3sgn  23973  sincosq4sgn  23974  lgsquadlem3  24824  colinearalg  25508  wlklniswwlkn2  25994  rusgranumwlkb0  26246  usgreg2spot  26360  extwwlkfab  26383  numclwwlk2lem1  26395  nmoo0  26836  leop3  28174  leoptri  28185  f1od2  28693  tltnle  28799  nofulllem5  30911  dfrdg4  31034  curf  32353  poimirlem28  32403  itgaddnclem2  32435  lfl1dim  33222  glbconxN  33478  2dim  33570  elpadd0  33909  dalawlem13  33983  diclspsn  35297  dihglb2  35445  dochsordN  35477  lzunuz  36145  uneqsn  37137  ntrclskb  37183  ntrneiel2  37200  infxrbnd2  38323  2reu4a  39635  funressnfv  39654  iccpartiltu  39758  1wlklnwwlkln2lem  41074  2pthdlem1  41132  rusgrnumwwlkb0  41169  fusgreg2wsp  41495  av-numclwwlk2lem1  41527
  Copyright terms: Public domain W3C validator