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

Theorem syl6rbb 289
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 288 . 2 (𝜑 → (𝜓𝜃))
43bicomd 224 1 (𝜑 → (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  syl6rbbr  291  bibif  373  oranabs  993  necon4bid  3061  2reu4lem  4463  resopab2  5898  xpco  6134  funconstss  6819  xpopth  7721  snmapen  8579  ac6sfi  8751  supgtoreq  8923  rankr1bg  9221  alephsdom  9501  brdom7disj  9942  fpwwe2lem13  10053  nn0sub  11936  elznn0  11985  nn01to3  12330  supxrbnd1  12704  supxrbnd2  12705  rexuz3  14698  smueqlem  15829  qnumdenbi  16074  dfiso3  17033  lssne0  19653  pjfval2  20783  0top  21521  1stccn  22001  dscopn  23112  bcthlem1  23856  ovolgelb  24010  iblpos  24322  itgposval  24325  itgsubstlem  24574  sincosq3sgn  25015  sincosq4sgn  25016  lgsquadlem3  25886  colinearalg  26624  elntg2  26699  wlklnwwlkln2lem  27588  2pthdlem1  27637  wwlks2onsym  27665  rusgrnumwwlkb0  27678  numclwwlk2lem1  28083  nmoo0  28496  leop3  29830  leoptri  29841  f1od2  30384  tltnle  30577  fedgmullem2  30926  dfrdg4  33310  curf  34752  poimirlem28  34802  itgaddnclem2  34833  lfl1dim  36139  glbconxN  36396  2dim  36488  elpadd0  36827  dalawlem13  36901  diclspsn  38212  dihglb2  38360  dochsordN  38392  lzunuz  39245  uneqsn  40253  ntrclskb  40299  ntrneiel2  40316  infxrbnd2  41517  funressnfv  43159  funressndmafv2rn  43303  iccpartiltu  43429
  Copyright terms: Public domain W3C validator