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  373  19.16  2249  19.19  2253  sbcom2  2593  sbal2  2609  necon1bbid  2982  rspc2gv  3471  elabgt  3498  sbceq1a  3598  sbcralt  3660  sbccsb2  4149  disjxun  4784  dfres3  5539  xp11  5710  ressn  5815  fnssresb  6143  dmfco  6414  dffo4  6518  f1ompt  6524  funressn  6569  elunirnALT  6653  fliftf  6708  resoprab2  6904  elrnmpt2res  6921  ralrnmpt2  6922  iunpw  7125  ordunisuc2  7191  tfis  7201  tfinds  7206  dfom2  7214  fun11iun  7273  opiota  7378  1stconst  7416  2ndconst  7417  fnsuppeq0  7475  iinon  7590  dfsmo2  7597  oeeui  7836  omabs  7881  brecop  7992  ixpsnf1o  8102  boxcutc  8105  ac6sfi  8360  wemapwe  8758  sdom2en01  9326  ac6num  9503  zorn2lem7  9526  ttukeylem6  9538  alephval2  9596  fpwwe2  9667  fpwwe  9670  nqereu  9953  suplem2pr  10077  map2psrpr  10133  supsrlem  10134  fimaxre3  11172  infm3  11184  crne0  11215  nn1suc  11243  xmulneg1  12304  supxrbnd1  12356  supxrbnd2  12357  iccneg  12500  wrdmap  13532  wrdind  13685  rtrclreclem3  14008  cnpart  14188  sqrt00  14212  lo1resb  14503  o1resb  14505  absefib  15134  efieq1re  15135  sadadd2lem2  15380  saddisjlem  15394  prmind2  15605  isprm7  15627  mreacs  16526  issubc  16702  isfunc  16731  pospo  17181  mrcmndind  17574  eqgval  17851  resscntz  17971  frgpuplem  18392  qusabl  18475  dmdprd  18605  dprdcntz2  18645  dprd2d2  18651  isnzr2  19478  mpfind  19751  gsummoncoe1  19889  pf1ind  19934  chrdvds  20091  chrcong  20092  znleval  20118  isphld  20216  smadiadetr  20700  mp2pm2mplem4  20834  isclo  21112  ist1-2  21372  isnrm2  21383  bwth  21434  nconnsubb  21447  subislly  21505  ptclsg  21639  qtopcld  21737  kqcldsat  21757  qustgplem  22144  tsmssubm  22166  ustuqtop  22270  utop2nei  22274  blval2  22587  caucfil  23300  ioorinv  23564  mbfss  23633  iblss2  23792  dvivthlem1  23991  lhop1  23997  deg1leb  24075  reeff1o  24421  sincosq3sgn  24473  sincosq4sgn  24474  dcubic  24794  efrlim  24917  fsumharmonic  24959  isppw  25061  issqf  25083  fsumdvdsmul  25142  ppiub  25150  lgsdinn0  25291  tglngne  25666  tgelrnln  25746  axlowdimlem14  26056  nbgrssovtx  26480  nbgrssovtxOLD  26483  clwwlknclwwlkdif  27127  eupth2lem2  27399  fusgr2wsp2nb  27516  h2hlm  28177  isch2  28420  ch0pss  28644  nmcfnlbi  29251  jplem1  29467  hatomistici  29561  mdsymlem5  29606  cdjreui  29631  reuxfr4d  29669  dfimafnf  29776  funcnvmpt  29808  fpwrelmap  29848  nn0min  29907  isarchi  30076  ordtconnlem1  30310  esumfsup  30472  esumpcvgval  30480  measvuni  30617  aean  30647  eulerpartlemgh  30780  ballotlemsima  30917  sgn3da  30943  bnj1468  31254  subfacp1lem2a  31500  subfacp1lem6  31505  eldm3  31989  onsuct0  32777  bj-restsn  33367  ptrest  33741  ptrecube  33742  poimirlem2  33744  poimirlem23  33765  sdclem2  33870  fdc  33873  fdc1  33874  istotbnd3  33902  sstotbnd  33906  prdstotbnd  33925  rrncmslem  33963  brinxprnres  34402  alrmomodm  34466  br1cossxrnres  34540  lub0N  34998  glb0N  35002  cdlemefrs29bpre0  36205  dvhb1dimN  36795  dvhopellsm  36927  dibord  36969  dochnel2  37202  mapdvalc  37439  mapdval4N  37442  diophin  37862  diophun  37863  diophrex  37865  3rexfrabdioph  37887  6rexfrabdioph  37889  7rexfrabdioph  37890  zindbi  38037  rababg  38405  relexpnul  38496  clsk1independent  38870  hashnzfzclim  39047  fveqsb  39182  infxrbnd2  40101  cncfiooicclem1  40624  stoweidlem35  40769  tz6.12-afv  41773  ndmaovg  41784  aacllem  43078
  Copyright terms: Public domain W3C validator