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

Theorem syl5bbr 273
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 213 . 2 (𝜑𝜓)
3 syl5bbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5bb 271 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  3bitr3g  301  biass  373  19.16  2080  19.19  2084  sbcom2  2433  sbal2  2449  necon1bbid  2821  elabgt  3316  sbceq1a  3413  sbcralt  3477  sbccsb2  3957  disjxun  4581  xp11  5488  ressn  5588  fnssresb  5917  dmfco  6182  dffo4  6283  f1ompt  6290  funressn  6331  elunirnALT  6414  fliftf  6465  resoprab2  6655  elrnmpt2res  6672  ralrnmpt2  6673  iunpw  6870  ordunisuc2  6936  tfis  6946  tfinds  6951  dfom2  6959  fun11iun  7019  opiota  7118  1stconst  7152  2ndconst  7153  fnsuppeq0  7210  iinon  7324  dfsmo2  7331  oeeui  7569  omabs  7614  brecop  7727  ixpsnf1o  7834  boxcutc  7837  ac6sfi  8089  wemapwe  8477  sdom2en01  9007  ac6num  9184  zorn2lem7  9207  ttukeylem6  9219  alephval2  9273  fpwwe2  9344  fpwwe  9347  nqereu  9630  suplem2pr  9754  map2psrpr  9810  supsrlem  9811  fimaxre3  10849  infm3  10861  crne0  10890  nn1suc  10918  xmulneg1  11971  supxrbnd1  12023  supxrbnd2  12024  iccneg  12164  wrdmap  13191  wrdind  13328  rtrclreclem3  13648  cnpart  13828  sqrt00  13852  lo1resb  14143  o1resb  14145  absefib  14767  efieq1re  14768  sadadd2lem2  15010  saddisjlem  15024  prmind2  15236  isprm7  15258  mreacs  16142  issubc  16318  isfunc  16347  pospo  16796  mrcmndind  17189  eqgval  17466  resscntz  17587  frgpuplem  18008  qusabl  18091  dmdprd  18220  dprdcntz2  18260  dprd2d2  18266  isnzr2  19084  mpfind  19357  gsummoncoe1  19495  pf1ind  19540  chrdvds  19695  chrcong  19696  znleval  19722  isphld  19818  smadiadetr  20300  mp2pm2mplem4  20433  isclo  20701  ist1-2  20961  isnrm2  20972  bwth  21023  nconsubb  21036  subislly  21094  ptclsg  21228  qtopcld  21326  kqcldsat  21346  qustgplem  21734  tsmssubm  21756  ustuqtop  21860  utop2nei  21864  blval2  22177  caucfil  22889  ioorinv  23150  mbfss  23219  iblss2  23378  dvivthlem1  23575  lhop1  23581  deg1leb  23659  reeff1o  24005  sincosq3sgn  24056  sincosq4sgn  24057  dcubic  24373  efrlim  24496  fsumharmonic  24538  isppw  24640  issqf  24662  fsumdvdsmul  24721  ppiub  24729  lgsdinn0  24870  tglngne  25245  tgelrnln  25325  axlowdimlem14  25635  uhgraop  25833  eupath2lem2  26505  h2hlm  27221  isch2  27464  ch0pss  27688  nmcfnlbi  28295  jplem1  28511  hatomistici  28605  mdsymlem5  28650  cdjreui  28675  reuxfr4d  28714  dfimafnf  28817  funcnvmpt  28851  fpwrelmap  28896  nn0min  28954  isarchi  29067  ordtconlem1  29298  esumfsup  29459  esumpcvgval  29467  measvuni  29604  aean  29634  eulerpartlemgh  29767  ballotlemsima  29904  sgn3da  29930  bnj1468  30170  subfacp1lem2a  30416  subfacp1lem6  30421  dfres3  30902  eldm3  30905  onsuct0  31610  bj-restsn  32216  ptrest  32578  ptrecube  32579  poimirlem2  32581  poimirlem23  32602  sdclem2  32708  fdc  32711  fdc1  32712  istotbnd3  32740  sstotbnd  32744  prdstotbnd  32763  rrncmslem  32801  lub0N  33494  glb0N  33498  cdlemefrs29bpre0  34702  dvhb1dimN  35292  dvhopellsm  35424  dibord  35466  dochnel2  35699  mapdvalc  35936  mapdval4N  35939  diophin  36354  diophun  36355  diophrex  36357  3rexfrabdioph  36379  6rexfrabdioph  36381  7rexfrabdioph  36382  zindbi  36529  rababg  36898  relexpnul  36989  clsk1independent  37364  hashnzfzclim  37543  fveqsb  37678  infxrbnd2  38526  cncfiooicclem1  38779  stoweidlem35  38928  tz6.12-afv  39902  ndmaovg  39913  nbgrssovtx  40586  eupth2lem2  41387  fusgr2wsp2nb  41498  aacllem  42356
  Copyright terms: Public domain W3C validator