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

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

Proof of Theorem syl5bbr
StepHypRef Expression
1 syl5bbr.1 . . 3 (𝜓𝜑)
21bicomi 214 . 2 (𝜑𝜓)
3 syl5bbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5bb 272 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  3bitr3g  302  biass  374  19.16  2096  19.19  2100  sbcom2  2449  sbal2  2465  necon1bbid  2835  elabgt  3335  sbceq1a  3433  sbcralt  3497  sbccsb2  3982  disjxun  4616  xp11  5532  ressn  5633  fnssresb  5963  dmfco  6230  dffo4  6332  f1ompt  6339  funressn  6381  elunirnALT  6465  fliftf  6520  resoprab2  6711  elrnmpt2res  6728  ralrnmpt2  6729  iunpw  6926  ordunisuc2  6992  tfis  7002  tfinds  7007  dfom2  7015  fun11iun  7076  opiota  7175  1stconst  7211  2ndconst  7212  fnsuppeq0  7269  iinon  7383  dfsmo2  7390  oeeui  7628  omabs  7673  brecop  7786  ixpsnf1o  7893  boxcutc  7896  ac6sfi  8149  wemapwe  8539  sdom2en01  9069  ac6num  9246  zorn2lem7  9269  ttukeylem6  9281  alephval2  9339  fpwwe2  9410  fpwwe  9413  nqereu  9696  suplem2pr  9820  map2psrpr  9876  supsrlem  9877  fimaxre3  10915  infm3  10927  crne0  10958  nn1suc  10986  xmulneg1  12039  supxrbnd1  12091  supxrbnd2  12092  iccneg  12232  wrdmap  13270  wrdind  13409  rtrclreclem3  13729  cnpart  13909  sqrt00  13933  lo1resb  14224  o1resb  14226  absefib  14848  efieq1re  14849  sadadd2lem2  15091  saddisjlem  15105  prmind2  15317  isprm7  15339  mreacs  16235  issubc  16411  isfunc  16440  pospo  16889  mrcmndind  17282  eqgval  17559  resscntz  17680  frgpuplem  18101  qusabl  18184  dmdprd  18313  dprdcntz2  18353  dprd2d2  18359  isnzr2  19177  mpfind  19450  gsummoncoe1  19588  pf1ind  19633  chrdvds  19790  chrcong  19791  znleval  19817  isphld  19913  smadiadetr  20395  mp2pm2mplem4  20528  isclo  20796  ist1-2  21056  isnrm2  21067  bwth  21118  nconnsubb  21131  subislly  21189  ptclsg  21323  qtopcld  21421  kqcldsat  21441  qustgplem  21829  tsmssubm  21851  ustuqtop  21955  utop2nei  21959  blval2  22272  caucfil  22984  ioorinv  23245  mbfss  23314  iblss2  23473  dvivthlem1  23670  lhop1  23676  deg1leb  23754  reeff1o  24100  sincosq3sgn  24151  sincosq4sgn  24152  dcubic  24468  efrlim  24591  fsumharmonic  24633  isppw  24735  issqf  24757  fsumdvdsmul  24816  ppiub  24824  lgsdinn0  24965  tglngne  25340  tgelrnln  25420  axlowdimlem14  25730  nbgrssovtx  26141  eupth2lem2  26939  fusgr2wsp2nb  27050  h2hlm  27677  isch2  27920  ch0pss  28144  nmcfnlbi  28751  jplem1  28967  hatomistici  29061  mdsymlem5  29106  cdjreui  29131  reuxfr4d  29170  dfimafnf  29270  funcnvmpt  29302  fpwrelmap  29342  nn0min  29400  isarchi  29513  ordtconnlem1  29744  esumfsup  29905  esumpcvgval  29913  measvuni  30050  aean  30080  eulerpartlemgh  30213  ballotlemsima  30350  sgn3da  30376  bnj1468  30616  subfacp1lem2a  30862  subfacp1lem6  30867  dfres3  31348  eldm3  31351  onsuct0  32055  bj-restsn  32645  ptrest  33007  ptrecube  33008  poimirlem2  33010  poimirlem23  33031  sdclem2  33137  fdc  33140  fdc1  33141  istotbnd3  33169  sstotbnd  33173  prdstotbnd  33192  rrncmslem  33230  lub0N  33923  glb0N  33927  cdlemefrs29bpre0  35131  dvhb1dimN  35721  dvhopellsm  35853  dibord  35895  dochnel2  36128  mapdvalc  36365  mapdval4N  36368  diophin  36783  diophun  36784  diophrex  36786  3rexfrabdioph  36808  6rexfrabdioph  36810  7rexfrabdioph  36811  zindbi  36958  rababg  37327  relexpnul  37418  clsk1independent  37793  hashnzfzclim  37970  fveqsb  38106  infxrbnd2  39017  cncfiooicclem1  39378  stoweidlem35  39527  tz6.12-afv  40525  ndmaovg  40536  aacllem  41805
  Copyright terms: Public domain W3C validator