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

Theorem syl6rbb 290
 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 289 . 2 (𝜑 → (𝜓𝜃))
43bicomd 225 1 (𝜑 → (𝜃𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208 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 209 This theorem is referenced by:  syl6rbbr  292  bibif  374  oranabs  996  necon4bid  3061  2reu4lem  4465  resopab2  5899  xpco  6135  funconstss  6821  xpopth  7724  snmapen  8584  ac6sfi  8756  supgtoreq  8928  rankr1bg  9226  alephsdom  9506  brdom7disj  9947  fpwwe2lem13  10058  nn0sub  11941  elznn0  11990  nn01to3  12335  supxrbnd1  12708  supxrbnd2  12709  rexuz3  14702  smueqlem  15833  qnumdenbi  16078  dfiso3  17037  lssne0  19716  pjfval2  20847  0top  21585  1stccn  22065  dscopn  23177  bcthlem1  23921  ovolgelb  24075  iblpos  24387  itgposval  24390  itgsubstlem  24639  sincosq3sgn  25080  sincosq4sgn  25081  lgsquadlem3  25952  colinearalg  26690  elntg2  26765  wlklnwwlkln2lem  27654  2pthdlem1  27703  wwlks2onsym  27731  rusgrnumwwlkb0  27744  numclwwlk2lem1  28149  nmoo0  28562  leop3  29896  leoptri  29907  f1od2  30451  tltnle  30644  fedgmullem2  31021  dfrdg4  33407  curf  34864  poimirlem28  34914  itgaddnclem2  34945  lfl1dim  36251  glbconxN  36508  2dim  36600  elpadd0  36939  dalawlem13  37013  diclspsn  38324  dihglb2  38472  dochsordN  38504  lzunuz  39358  uneqsn  40366  ntrclskb  40412  ntrneiel2  40429  infxrbnd2  41629  funressnfv  43271  funressndmafv2rn  43415  iccpartiltu  43575
 Copyright terms: Public domain W3C validator