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

Theorem syl5bbr 272
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 212 . 2 (𝜑𝜓)
3 syl5bbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5bb 270 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  3bitr3g  300  biass  372  19.16  2079  19.19  2083  sbcom2  2432  sbal2  2448  necon1bbid  2820  elabgt  3315  sbceq1a  3412  sbcralt  3476  sbccsb2  3956  disjxun  4575  xp11  5474  ressn  5574  fnssresb  5903  dmfco  6167  dffo4  6268  f1ompt  6275  funressn  6309  elunirnALT  6392  fliftf  6443  resoprab2  6633  elrnmpt2res  6650  ralrnmpt2  6651  iunpw  6847  ordunisuc2  6913  tfis  6923  tfinds  6928  dfom2  6936  fun11iun  6996  opiota  7095  1stconst  7129  2ndconst  7130  fnsuppeq0  7187  iinon  7301  dfsmo2  7308  oeeui  7546  omabs  7591  brecop  7704  ixpsnf1o  7811  boxcutc  7814  ac6sfi  8066  wemapwe  8454  sdom2en01  8984  ac6num  9161  zorn2lem7  9184  ttukeylem6  9196  alephval2  9250  fpwwe2  9321  fpwwe  9324  nqereu  9607  suplem2pr  9731  map2psrpr  9787  supsrlem  9788  fimaxre3  10819  infm3  10831  crne0  10860  nn1suc  10888  xmulneg1  11928  supxrbnd1  11979  supxrbnd2  11980  iccneg  12120  wrdmap  13137  wrdind  13274  rtrclreclem3  13594  cnpart  13774  sqrt00  13798  lo1resb  14089  o1resb  14091  absefib  14713  efieq1re  14714  sadadd2lem2  14956  saddisjlem  14970  prmind2  15182  isprm7  15204  mreacs  16088  issubc  16264  isfunc  16293  pospo  16742  mrcmndind  17135  eqgval  17412  resscntz  17533  frgpuplem  17954  qusabl  18037  dmdprd  18166  dprdcntz2  18206  dprd2d2  18212  isnzr2  19030  mpfind  19303  gsummoncoe1  19441  pf1ind  19486  chrdvds  19640  chrcong  19641  znleval  19667  isphld  19763  smadiadetr  20242  mp2pm2mplem4  20375  isclo  20643  ist1-2  20903  isnrm2  20914  bwth  20965  nconsubb  20978  subislly  21036  ptclsg  21170  qtopcld  21268  kqcldsat  21288  qustgplem  21676  tsmssubm  21698  ustuqtop  21802  utop2nei  21806  blval2  22118  caucfil  22807  ioorinv  23067  mbfss  23136  iblss2  23295  dvivthlem1  23492  lhop1  23498  deg1leb  23576  reeff1o  23922  sincosq3sgn  23973  sincosq4sgn  23974  dcubic  24290  efrlim  24413  fsumharmonic  24455  isppw  24557  issqf  24579  fsumdvdsmul  24638  ppiub  24646  lgsdinn0  24787  tglngne  25163  tgelrnln  25243  axlowdimlem14  25553  uhgraop  25599  eupath2lem2  26271  h2hlm  27027  isch2  27270  ch0pss  27494  nmcfnlbi  28101  jplem1  28317  hatomistici  28411  mdsymlem5  28456  cdjreui  28481  reuxfr4d  28520  dfimafnf  28623  funcnvmpt  28657  fpwrelmap  28702  nn0min  28760  isarchi  28873  ordtconlem1  29104  esumfsup  29265  esumpcvgval  29273  measvuni  29410  aean  29440  eulerpartlemgh  29573  ballotlemsima  29710  sgn3da  29736  bnj1468  29976  subfacp1lem2a  30222  subfacp1lem6  30227  dfres3  30708  eldm3  30711  onsuct0  31416  bj-restsn  32012  ptrest  32374  ptrecube  32375  poimirlem2  32377  poimirlem23  32398  sdclem2  32504  fdc  32507  fdc1  32508  istotbnd3  32536  sstotbnd  32540  prdstotbnd  32559  rrncmslem  32597  lub0N  33290  glb0N  33294  cdlemefrs29bpre0  34498  dvhb1dimN  35088  dvhopellsm  35220  dibord  35262  dochnel2  35495  mapdvalc  35732  mapdval4N  35735  diophin  36150  diophun  36151  diophrex  36153  3rexfrabdioph  36175  6rexfrabdioph  36177  7rexfrabdioph  36178  zindbi  36325  rababg  36694  relexpnul  36785  clsk1independent  37160  hashnzfzclim  37339  fveqsb  37474  infxrbnd2  38323  cncfiooicclem1  38576  stoweidlem35  38725  tz6.12-afv  39700  ndmaovg  39711  nbgrssovtx  40581  eupth2lem2  41382  fusgr2wsp2nb  41493  aacllem  42312
  Copyright terms: Public domain W3C validator