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  2131  19.19  2135  sbcom2  2473  sbal2  2489  necon1bbid  2862  rspc2gv  3352  elabgt  3379  sbceq1a  3479  sbcralt  3543  sbccsb2  4038  disjxun  4683  dfres3  5433  xp11  5604  ressn  5709  fnssresb  6041  dmfco  6311  dffo4  6415  f1ompt  6422  funressn  6466  elunirnALT  6550  fliftf  6605  resoprab2  6799  elrnmpt2res  6816  ralrnmpt2  6817  iunpw  7020  ordunisuc2  7086  tfis  7096  tfinds  7101  dfom2  7109  fun11iun  7168  opiota  7273  1stconst  7310  2ndconst  7311  fnsuppeq0  7368  iinon  7482  dfsmo2  7489  oeeui  7727  omabs  7772  brecop  7883  ixpsnf1o  7990  boxcutc  7993  ac6sfi  8245  wemapwe  8632  sdom2en01  9162  ac6num  9339  zorn2lem7  9362  ttukeylem6  9374  alephval2  9432  fpwwe2  9503  fpwwe  9506  nqereu  9789  suplem2pr  9913  map2psrpr  9969  supsrlem  9970  fimaxre3  11008  infm3  11020  crne0  11051  nn1suc  11079  xmulneg1  12137  supxrbnd1  12189  supxrbnd2  12190  iccneg  12331  wrdmap  13368  wrdind  13522  rtrclreclem3  13844  cnpart  14024  sqrt00  14048  lo1resb  14339  o1resb  14341  absefib  14972  efieq1re  14973  sadadd2lem2  15219  saddisjlem  15233  prmind2  15445  isprm7  15467  mreacs  16366  issubc  16542  isfunc  16571  pospo  17020  mrcmndind  17413  eqgval  17690  resscntz  17810  frgpuplem  18231  qusabl  18314  dmdprd  18443  dprdcntz2  18483  dprd2d2  18489  isnzr2  19311  mpfind  19584  gsummoncoe1  19722  pf1ind  19767  chrdvds  19924  chrcong  19925  znleval  19951  isphld  20047  smadiadetr  20529  mp2pm2mplem4  20662  isclo  20939  ist1-2  21199  isnrm2  21210  bwth  21261  nconnsubb  21274  subislly  21332  ptclsg  21466  qtopcld  21564  kqcldsat  21584  qustgplem  21971  tsmssubm  21993  ustuqtop  22097  utop2nei  22101  blval2  22414  caucfil  23127  ioorinv  23390  mbfss  23458  iblss2  23617  dvivthlem1  23816  lhop1  23822  deg1leb  23900  reeff1o  24246  sincosq3sgn  24297  sincosq4sgn  24298  dcubic  24618  efrlim  24741  fsumharmonic  24783  isppw  24885  issqf  24907  fsumdvdsmul  24966  ppiub  24974  lgsdinn0  25115  tglngne  25490  tgelrnln  25570  axlowdimlem14  25880  nbgrssovtx  26302  nbgrssovtxOLD  26305  clwwlknclwwlkdif  26945  eupth2lem2  27197  fusgr2wsp2nb  27314  h2hlm  27965  isch2  28208  ch0pss  28432  nmcfnlbi  29039  jplem1  29255  hatomistici  29349  mdsymlem5  29394  cdjreui  29419  reuxfr4d  29457  dfimafnf  29564  funcnvmpt  29596  fpwrelmap  29636  nn0min  29695  isarchi  29864  ordtconnlem1  30098  esumfsup  30260  esumpcvgval  30268  measvuni  30405  aean  30435  eulerpartlemgh  30568  ballotlemsima  30705  sgn3da  30731  bnj1468  31042  subfacp1lem2a  31288  subfacp1lem6  31293  eldm3  31777  onsuct0  32565  bj-restsn  33160  ptrest  33538  ptrecube  33539  poimirlem2  33541  poimirlem23  33562  sdclem2  33668  fdc  33671  fdc1  33672  istotbnd3  33700  sstotbnd  33704  prdstotbnd  33723  rrncmslem  33761  brinxprnres  34200  alrmomodm  34264  br1cossxrnres  34338  lub0N  34794  glb0N  34798  cdlemefrs29bpre0  36001  dvhb1dimN  36591  dvhopellsm  36723  dibord  36765  dochnel2  36998  mapdvalc  37235  mapdval4N  37238  diophin  37653  diophun  37654  diophrex  37656  3rexfrabdioph  37678  6rexfrabdioph  37680  7rexfrabdioph  37681  zindbi  37828  rababg  38196  relexpnul  38287  clsk1independent  38661  hashnzfzclim  38838  fveqsb  38974  infxrbnd2  39898  cncfiooicclem1  40424  stoweidlem35  40570  tz6.12-afv  41574  ndmaovg  41585  aacllem  42875
 Copyright terms: Public domain W3C validator