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  2091  19.19  2095  sbcom2  2444  sbal2  2460  necon1bbid  2829  rspc2gv  3310  elabgt  3335  sbceq1a  3433  sbcralt  3497  sbccsb2  3983  disjxun  4621  xp11  5538  ressn  5640  fnssresb  5971  dmfco  6239  dffo4  6341  f1ompt  6348  funressn  6391  elunirnALT  6475  fliftf  6530  resoprab2  6722  elrnmpt2res  6739  ralrnmpt2  6740  iunpw  6940  ordunisuc2  7006  tfis  7016  tfinds  7021  dfom2  7029  fun11iun  7088  opiota  7189  1stconst  7225  2ndconst  7226  fnsuppeq0  7283  iinon  7397  dfsmo2  7404  oeeui  7642  omabs  7687  brecop  7800  ixpsnf1o  7908  boxcutc  7911  ac6sfi  8164  wemapwe  8554  sdom2en01  9084  ac6num  9261  zorn2lem7  9284  ttukeylem6  9296  alephval2  9354  fpwwe2  9425  fpwwe  9428  nqereu  9711  suplem2pr  9835  map2psrpr  9891  supsrlem  9892  fimaxre3  10930  infm3  10942  crne0  10973  nn1suc  11001  xmulneg1  12058  supxrbnd1  12110  supxrbnd2  12111  iccneg  12251  wrdmap  13291  wrdind  13430  rtrclreclem3  13750  cnpart  13930  sqrt00  13954  lo1resb  14245  o1resb  14247  absefib  14872  efieq1re  14873  sadadd2lem2  15115  saddisjlem  15129  prmind2  15341  isprm7  15363  mreacs  16259  issubc  16435  isfunc  16464  pospo  16913  mrcmndind  17306  eqgval  17583  resscntz  17704  frgpuplem  18125  qusabl  18208  dmdprd  18337  dprdcntz2  18377  dprd2d2  18383  isnzr2  19203  mpfind  19476  gsummoncoe1  19614  pf1ind  19659  chrdvds  19816  chrcong  19817  znleval  19843  isphld  19939  smadiadetr  20421  mp2pm2mplem4  20554  isclo  20831  ist1-2  21091  isnrm2  21102  bwth  21153  nconnsubb  21166  subislly  21224  ptclsg  21358  qtopcld  21456  kqcldsat  21476  qustgplem  21864  tsmssubm  21886  ustuqtop  21990  utop2nei  21994  blval2  22307  caucfil  23021  ioorinv  23284  mbfss  23353  iblss2  23512  dvivthlem1  23709  lhop1  23715  deg1leb  23793  reeff1o  24139  sincosq3sgn  24190  sincosq4sgn  24191  dcubic  24507  efrlim  24630  fsumharmonic  24672  isppw  24774  issqf  24796  fsumdvdsmul  24855  ppiub  24863  lgsdinn0  25004  tglngne  25379  tgelrnln  25459  axlowdimlem14  25769  nbgrssovtx  26181  eupth2lem2  26979  fusgr2wsp2nb  27090  h2hlm  27725  isch2  27968  ch0pss  28192  nmcfnlbi  28799  jplem1  29015  hatomistici  29109  mdsymlem5  29154  cdjreui  29179  reuxfr4d  29219  dfimafnf  29320  funcnvmpt  29352  fpwrelmap  29392  nn0min  29450  isarchi  29563  ordtconnlem1  29794  esumfsup  29955  esumpcvgval  29963  measvuni  30100  aean  30130  eulerpartlemgh  30263  ballotlemsima  30400  sgn3da  30426  bnj1468  30677  subfacp1lem2a  30923  subfacp1lem6  30928  dfres3  31410  eldm3  31413  onsuct0  32135  bj-restsn  32725  ptrest  33079  ptrecube  33080  poimirlem2  33082  poimirlem23  33103  sdclem2  33209  fdc  33212  fdc1  33213  istotbnd3  33241  sstotbnd  33245  prdstotbnd  33264  rrncmslem  33302  lub0N  33995  glb0N  33999  cdlemefrs29bpre0  35203  dvhb1dimN  35793  dvhopellsm  35925  dibord  35967  dochnel2  36200  mapdvalc  36437  mapdval4N  36440  diophin  36855  diophun  36856  diophrex  36858  3rexfrabdioph  36880  6rexfrabdioph  36882  7rexfrabdioph  36883  zindbi  37030  rababg  37399  relexpnul  37490  clsk1independent  37865  hashnzfzclim  38042  fveqsb  38178  infxrbnd2  39084  cncfiooicclem1  39441  stoweidlem35  39589  tz6.12-afv  40587  ndmaovg  40598  aacllem  41880
  Copyright terms: Public domain W3C validator