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

Theorem syl5bbr 286
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 225 . 2 (𝜑𝜓)
3 syl5bbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5bb 284 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:  3bitr3g  314  biass  386  sbcom2  2158  19.16  2218  19.19  2222  sbbibOLD  2281  sbal2OLD  2570  necon1bbid  3055  rspc2gv  3631  elabgt  3662  reuxfr1d  3740  sbceq1a  3782  sbcralt  3854  sbccsb2  4385  reuprg0  4632  disjxun  5056  dmopab2rex  5780  dfres3  5852  xp11  6026  ressn  6130  fnssresb  6463  dmfco  6751  dffo4  6862  f1ompt  6868  funressn  6914  elunirnALT  7002  fliftf  7057  resoprab2  7260  elrnmpores  7277  ralrnmpo  7278  iunpw  7481  ordunisuc2  7547  tfis  7557  tfinds  7562  dfom2  7570  fiunw  7632  f1iunw  7633  fiun  7635  f1iun  7636  opiota  7748  1stconst  7786  2ndconst  7787  fnsuppeq0  7849  iinon  7968  dfsmo2  7975  oeeui  8218  omabs  8264  brecop  8380  ixpsnf1o  8491  boxcutc  8494  ac6sfi  8751  wemapwe  9149  sdom2en01  9713  ac6num  9890  zorn2lem7  9913  ttukeylem6  9925  alephval2  9983  fpwwe2  10054  fpwwe  10057  nqereu  10340  suplem2pr  10464  map2psrpr  10521  supsrlem  10522  fimaxre3  11576  infm3  11589  crne0  11620  nn1suc  11648  xmulneg1  12652  supxrbnd1  12704  supxrbnd2  12705  iccneg  12848  wrdmap  13887  wrdind  14074  rtrclreclem3  14409  cnpart  14589  sqrt00  14613  lo1resb  14911  o1resb  14913  absefib  15541  efieq1re  15542  sadadd2lem2  15789  saddisjlem  15803  prmind2  16019  isprm7  16042  mreacs  16919  issubc  17095  isfunc  17124  pospo  17573  mndind  17982  eqgval  18269  resscntz  18402  frgpuplem  18829  qusabl  18916  dmdprd  19051  dprdcntz2  19091  dprd2d2  19097  isnzr2  19966  mpfind  20250  gsummoncoe1  20402  pf1ind  20448  chrdvds  20605  chrcong  20606  znleval  20631  isphld  20728  smadiadetr  21214  mp2pm2mplem4  21347  isclo  21625  ist1-2  21885  isnrm2  21896  bwth  21948  nconnsubb  21961  subislly  22019  ptclsg  22153  qtopcld  22251  kqcldsat  22271  qustgplem  22658  tsmssubm  22680  ustuqtop  22784  utop2nei  22788  blval2  23101  caucfil  23815  ioorinv  24106  mbfss  24176  iblss2  24335  dvivthlem1  24534  lhop1  24540  deg1leb  24618  reeff1o  24964  sincosq3sgn  25015  sincosq4sgn  25016  dcubic  25351  efrlim  25475  fsumharmonic  25517  isppw  25619  issqf  25641  fsumdvdsmul  25700  ppiub  25708  lgsdinn0  25849  tglngne  26264  tgelrnln  26344  axlowdimlem14  26669  nbgrssovtx  27071  clwwlknclwwlkdif  27685  eupth2lem2  27926  fusgr2wsp2nb  28041  h2hlm  28685  isch2  28928  ch0pss  29150  nmcfnlbi  29757  jplem1  29973  hatomistici  30067  mdsymlem5  30112  cdjreui  30137  dfimafnf  30310  funcnvmpt  30341  fpwrelmap  30396  nn0min  30464  wrdt2ind  30555  swrdrn3  30557  isarchi  30739  ordtconnlem1  31067  esumfsup  31229  esumpcvgval  31237  measvuni  31373  aean  31403  eulerpartlemgh  31536  ballotlemsima  31673  sgn3da  31699  bnj1468  32018  subfacp1lem2a  32325  subfacp1lem6  32330  goeleq12bg  32494  dmopab3rexdif  32550  eldm3  32895  onsuct0  33687  currysetlem1  34156  bj-restsn  34268  ptrest  34773  ptrecube  34774  poimirlem2  34776  poimirlem23  34797  sdclem2  34900  fdc  34903  fdc1  34904  istotbnd3  34932  sstotbnd  34936  prdstotbnd  34955  rrncmslem  34993  brinxprnres  35431  brcnvrabga  35482  alrmomodm  35496  br1cossxrnres  35570  lub0N  36207  glb0N  36211  cdlemefrs29bpre0  37414  dvhb1dimN  38004  dvhopellsm  38135  dibord  38177  dochnel2  38410  mapdvalc  38647  mapdval4N  38650  diophin  39249  diophun  39250  diophrex  39252  3rexfrabdioph  39274  6rexfrabdioph  39276  7rexfrabdioph  39277  zindbi  39423  rababg  39813  relexpnul  39903  clsk1independent  40276  scottabf  40456  hashnzfzclim  40534  fveqsb  40665  infxrbnd2  41517  cncfiooicclem1  42056  stoweidlem35  42201  tz6.12-afv  43253  ndmaovg  43264  tz6.12-afv2  43320  ich2exprop  43480  prprspr2  43527  line2x  44639  line2y  44640  itsclc0b  44657  aacllem  44800
  Copyright terms: Public domain W3C validator