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  2217  19.19  2221  sbbibOLD  2280  sbal2OLD  2567  necon1bbid  3052  rspc2gv  3629  elabgt  3660  reuxfr1d  3738  sbceq1a  3780  sbcralt  3852  sbccsb2  4383  reuprg0  4630  disjxun  5055  dmopab2rex  5779  dfres3  5851  xp11  6025  ressn  6129  fnssresb  6462  dmfco  6750  dffo4  6861  f1ompt  6867  funressn  6913  elunirnALT  7002  fliftf  7057  resoprab2  7260  elrnmpores  7277  ralrnmpo  7278  iunpw  7482  ordunisuc2  7548  tfis  7558  tfinds  7563  dfom2  7571  fiun  7633  f1iun  7634  opiota  7746  1stconst  7784  2ndconst  7785  fnsuppeq0  7847  iinon  7966  dfsmo2  7973  oeeui  8217  omabs  8263  brecop  8379  ixpsnf1o  8490  boxcutc  8493  ac6sfi  8750  wemapwe  9148  sdom2en01  9712  ac6num  9889  zorn2lem7  9912  ttukeylem6  9924  alephval2  9982  fpwwe2  10053  fpwwe  10056  nqereu  10339  suplem2pr  10463  map2psrpr  10520  supsrlem  10521  fimaxre3  11575  infm3  11588  crne0  11619  nn1suc  11647  xmulneg1  12650  supxrbnd1  12702  supxrbnd2  12703  iccneg  12846  wrdmap  13885  wrdind  14072  rtrclreclem3  14407  cnpart  14587  sqrt00  14611  lo1resb  14909  o1resb  14911  absefib  15539  efieq1re  15540  sadadd2lem2  15787  saddisjlem  15801  prmind2  16017  isprm7  16040  mreacs  16917  issubc  17093  isfunc  17122  pospo  17571  mndind  17980  eqgval  18267  resscntz  18400  frgpuplem  18827  qusabl  18914  dmdprd  19049  dprdcntz2  19089  dprd2d2  19095  isnzr2  19964  mpfind  20248  gsummoncoe1  20400  pf1ind  20446  chrdvds  20603  chrcong  20604  znleval  20629  isphld  20726  smadiadetr  21212  mp2pm2mplem4  21345  isclo  21623  ist1-2  21883  isnrm2  21894  bwth  21946  nconnsubb  21959  subislly  22017  ptclsg  22151  qtopcld  22249  kqcldsat  22269  qustgplem  22656  tsmssubm  22678  ustuqtop  22782  utop2nei  22786  blval2  23099  caucfil  23813  ioorinv  24104  mbfss  24174  iblss2  24333  dvivthlem1  24532  lhop1  24538  deg1leb  24616  reeff1o  24962  sincosq3sgn  25013  sincosq4sgn  25014  dcubic  25351  efrlim  25474  fsumharmonic  25516  isppw  25618  issqf  25640  fsumdvdsmul  25699  ppiub  25707  lgsdinn0  25848  tglngne  26263  tgelrnln  26343  axlowdimlem14  26668  nbgrssovtx  27070  clwwlknclwwlkdif  27684  eupth2lem2  27925  fusgr2wsp2nb  28040  h2hlm  28684  isch2  28927  ch0pss  29149  nmcfnlbi  29756  jplem1  29972  hatomistici  30066  mdsymlem5  30111  cdjreui  30136  dfimafnf  30309  funcnvmpt  30340  fpwrelmap  30395  nn0min  30463  wrdt2ind  30554  swrdrn3  30556  isarchi  30738  ordtconnlem1  31066  esumfsup  31228  esumpcvgval  31236  measvuni  31372  aean  31402  eulerpartlemgh  31535  ballotlemsima  31672  sgn3da  31698  bnj1468  32017  subfacp1lem2a  32324  subfacp1lem6  32329  goeleq12bg  32493  dmopab3rexdif  32549  eldm3  32894  onsuct0  33686  currysetlem1  34155  bj-restsn  34267  ptrest  34772  ptrecube  34773  poimirlem2  34775  poimirlem23  34796  sdclem2  34898  fdc  34901  fdc1  34902  istotbnd3  34930  sstotbnd  34934  prdstotbnd  34953  rrncmslem  34991  brinxprnres  35429  brcnvrabga  35480  alrmomodm  35494  br1cossxrnres  35568  lub0N  36205  glb0N  36209  cdlemefrs29bpre0  37412  dvhb1dimN  38002  dvhopellsm  38133  dibord  38175  dochnel2  38408  mapdvalc  38645  mapdval4N  38648  diophin  39247  diophun  39248  diophrex  39250  3rexfrabdioph  39272  6rexfrabdioph  39274  7rexfrabdioph  39275  zindbi  39421  rababg  39811  relexpnul  39901  clsk1independent  40274  scottabf  40453  hashnzfzclim  40531  fveqsb  40662  infxrbnd2  41513  cncfiooicclem1  42052  stoweidlem35  42197  tz6.12-afv  43249  ndmaovg  43260  tz6.12-afv2  43316  ich2exprop  43510  prprspr2  43557  line2x  44669  line2y  44670  itsclc0b  44687  aacllem  44830
  Copyright terms: Public domain W3C validator