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

Theorem syl5bbr 269
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 209 . 2 (𝜑𝜓)
3 syl5bbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5bb 267 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 191
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 192
This theorem is referenced by:  3bitr3g  297  biass  368  19.16  2090  19.19  2092  sbcom2  2328  sbal2  2344  necon1bbid  2716  elabgt  3205  sbceq1a  3302  sbcralt  3364  sbccsb2  3834  disjxun  4432  xp11  5322  ressn  5423  fnssresb  5743  dmfco  6006  dffo4  6105  f1ompt  6111  funressn  6145  elunirnALT  6228  fliftf  6279  resoprab2  6468  elrnmpt2res  6485  ralrnmpt2  6486  iunpw  6682  ordunisuc2  6748  tfis  6758  tfinds  6763  dfom2  6771  fun11iun  6830  opiota  6929  1stconst  6963  2ndconst  6964  fnsuppeq0  7021  iinon  7136  dfsmo2  7143  oeeui  7380  omabs  7425  brecop  7538  ixpsnf1o  7645  boxcutc  7648  ac6sfi  7900  wemapwe  8287  sdom2en01  8817  ac6num  8994  zorn2lem7  9017  ttukeylem6  9029  alephval2  9082  fpwwe2  9153  fpwwe  9156  nqereu  9439  suplem2pr  9563  map2psrpr  9619  supsrlem  9620  fimaxre3  10642  infm3  10657  crne0  10691  nn1suc  10719  xmulneg1  11650  supxrbnd1  11702  supxrbnd2  11703  iccneg  11849  wrdmap  12830  wrdind  12966  rtrclreclem3  13283  cnpart  13463  sqrt00  13487  lo1resb  13788  o1resb  13790  absefib  14412  efieq1re  14413  sadadd2lem2  14586  saddisjlem  14600  prmind2  14797  mreacs  15730  issubc  15906  isfunc  15935  pospo  16384  mrcmndind  16773  eqgval  17026  resscntz  17146  frgpuplem  17583  qusabl  17664  dmdprd  17791  dprdcntz2  17831  dprd2d2  17837  isnzr2  18646  mpfind  18918  gsummoncoe1  19056  pf1ind  19101  chrdvds  19257  chrcong  19258  znleval  19283  isphld  19379  smadiadetr  19858  mp2pm2mplem4  19991  isclo  20260  ist1-2  20520  isnrm2  20531  bwth  20582  nconsubb  20595  subislly  20653  ptclsg  20787  qtopcld  20885  kqcldsat  20905  qustgplem  21293  tsmssubm  21315  ustuqtop  21419  utop2nei  21423  blval2  21735  caucfil  22412  ioorinv  22688  ioorinvOLD  22693  mbfss  22763  iblss2  22924  dvivthlem1  23121  lhop1  23127  deg1leb  23205  reeff1o  23563  sincosq3sgn  23616  sincosq4sgn  23617  dcubic  23933  efrlim  24056  fsumharmonic  24098  isppw  24202  issqf  24224  fsumdvdsmul  24285  ppiub  24293  lgsdinn0  24429  tglngne  24756  tgelrnln  24836  axlowdimlem14  25146  uhgraop  25192  eupath2lem2  25866  h2hlm  26796  isch2  27039  ch0pss  27261  nmcfnlbi  27868  jplem1  28084  hatomistici  28178  mdsymlem5  28223  cdjreui  28248  reuxfr4d  28287  dfimafnf  28391  funcnvmpt  28428  fpwrelmap  28474  nn0min  28540  isarchi  28654  ordtconlem1  28885  esumfsup  29046  esumpcvgval  29054  measvuni  29191  aean  29221  eulerpartlemgh  29365  ballotlemsima  29502  ballotlemsimaOLD  29540  sgn3da  29566  bnj1468  29809  subfacp1lem2a  30055  subfacp1lem6  30060  ghomf1olem  30464  dfres3  30550  eldm3  30553  onsuct0  31250  bj-restsn  31815  ptrest  32177  ptrecube  32178  poimirlem2  32180  poimirlem23  32201  sdclem2  32308  fdc  32311  fdc1  32312  istotbnd3  32340  sstotbnd  32344  prdstotbnd  32363  rrncmslem  32401  lub0N  32995  glb0N  32999  cdlemefrs29bpre0  34203  dvhb1dimN  34793  dvhopellsm  34925  dibord  34967  dochnel2  35200  mapdvalc  35437  mapdval4N  35440  diophin  35855  diophun  35856  diophrex  35858  3rexfrabdioph  35880  6rexfrabdioph  35882  7rexfrabdioph  35883  zindbi  36034  rababg  36418  relexpnul  36509  isprm7  37017  hashnzfzclim  37028  fveqsb  37163  infxrbnd2  37968  cncfiooicclem1  38180  stoweidlem35  38332  tz6.12-afv  39195  ndmaovg  39206  nbgrssovtx  39986  eupth2lem2  40787  fusgr2wsp2nb  40898  aacllem  41727
  Copyright terms: Public domain W3C validator