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

Theorem syl6rbb 279
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 278 . 2 (𝜑 → (𝜓𝜃))
43bicomd 214 1 (𝜑 → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  syl6rbbr  281  bibif  362  oranabs  1022  pm5.61  1023  necon4bid  2982  resopab2  5625  xpco  5861  funconstss  6525  xpopth  7407  snmapen  8241  ac6sfi  8411  supgtoreq  8583  rankr1bg  8881  alephsdom  9160  brdom7disj  9606  fpwwe2lem13  9717  nn0sub  11590  elznn0  11639  nn01to3  11982  supxrbnd1  12353  supxrbnd2  12354  rexuz3  14373  smueqlem  15493  qnumdenbi  15731  dfiso3  16698  lssne0  19220  pjfval2  20329  0top  21067  1stccn  21546  dscopn  22657  bcthlem1  23401  ovolgelb  23538  iblpos  23850  itgposval  23853  itgsubstlem  24102  sincosq3sgn  24544  sincosq4sgn  24545  lgsquadlem3  25398  colinearalg  26081  wlklnwwlkln2lem  27074  2pthdlem1  27153  wwlks2onsym  27182  rusgrnumwwlkb0  27196  numclwwlk2lem1  27680  numclwwlk2lem1OLD  27691  nmoo0  28102  leop3  29440  leoptri  29451  f1od2  29948  tltnle  30109  dfrdg4  32502  curf  33811  poimirlem28  33861  itgaddnclem2  33892  lfl1dim  35077  glbconxN  35334  2dim  35426  elpadd0  35765  dalawlem13  35839  diclspsn  37150  dihglb2  37298  dochsordN  37330  lzunuz  38009  uneqsn  38995  ntrclskb  39041  ntrneiel2  39058  infxrbnd2  40223  funressnfv  41820  2reu4a  41860  funressndmafv2rn  41971  iccpartiltu  42092
  Copyright terms: Public domain W3C validator