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

Theorem syl6bir 257
Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)
Hypotheses
Ref Expression
syl6bir.1 (𝜑 → (𝜒𝜓))
syl6bir.2 (𝜒𝜃)
Assertion
Ref Expression
syl6bir (𝜑 → (𝜓𝜃))

Proof of Theorem syl6bir
StepHypRef Expression
1 syl6bir.1 . . 3 (𝜑 → (𝜒𝜓))
21biimprd 251 . 2 (𝜑 → (𝜓𝜒))
3 syl6bir.2 . 2 (𝜒𝜃)
42, 3syl6 35 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  ralnralall  4419  elinsn  4609  tppreqb  4701  sotri2  5960  sotri3  5961  somincom  5965  fnun  6438  fvmpti  6748  ovigg  7278  ndmovg  7315  onint  7494  ordsuc  7513  tfindsg  7559  findsg  7594  zfrep6  7642  extmptsuppeq  7841  tfrlem9  8008  tfr3  8022  omlimcl  8191  oneo  8194  nnneo  8265  pssnn  8724  inficl  8877  updjud  9351  dfac2b  9545  axdc2lem  9863  axextnd  10006  canthp1lem2  10068  gchinf  10072  inatsk  10193  indpi  10322  ltaddpr2  10450  reclem2pr  10463  supsrlem  10526  axrrecex  10578  zeo  12060  nn0ind-raph  12074  fzm1  12986  fzind2  13154  addmodlteq  13313  bcpasc  13681  pr2pwpr  13837  swrdnnn0nd  14013  pwdif  15218  oddnn02np1  15692  oddge22np1  15693  evennn02n  15694  evennn2n  15695  bitsfzo  15777  bezoutlem1  15880  algcvgblem  15914  coprmdvds1  15989  qredeq  15994  prmreclem2  16246  ramtcl2  16340  divsfval  16815  joinval  17610  meetval  17624  gsumval3  19023  pgpfac1lem3a  19194  fiinopn  21509  restntr  21790  lly1stc  22104  dgradd2  24868  dgrcolem2  24874  asinneg  25475  ftalem2  25662  ftalem4  25664  ftalem5  25665  bpos1lem  25869  zabsle1  25883  lgsqrmodndvds  25940  incistruhgr  26875  fusgrfis  27123  uhgrnbgr0nb  27147  cusgrrusgr  27374  wlkswwlksf1o  27668  isclwwlknx  27824  clwwlknwwlksnb  27843  clwlknf1oclwwlknlem1  27869  frgrwopreglem3  28102  frgrreg  28182  frgrregord013  28183  h1de2ctlem  29341  pjclem4a  29984  pj3lem1  29992  chrelat2i  30151  sumdmdii  30201  elim2if  30314  bnj1468  32226  bnj517  32265  acycgrislfgr  32507  axextdist  33152  funtransport  33600  bj-19.21t0  34263  bj-projval  34427  areacirc  35143  rngoueqz  35371  isdmn3  35505  ax12fromc15  36194  lkrlspeqN  36460  hlrelat2  36692  ps-1  36766  dalem54  37015  cdleme42c  37761  dihmeetlem6  38598  frege124d  40449  uneqsn  40713  iotavalb  41121  2reuimp  43658  afv2orxorb  43771  iccpartnel  43942  fargshiftf1  43945  gbowge7  44268  sbgoldbwt  44282  bgoldbtbndlem1  44310  uspgrsprf1  44362
  Copyright terms: Public domain W3C validator