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

Theorem syl6bir 245
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 239 . 2 (𝜑 → (𝜓𝜒))
3 syl6bir.2 . 2 (𝜒𝜃)
42, 3syl6 35 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  19.21tOLDOLD  2242  19.21tOLD  2389  axext3  2793  ralnralall  4280  elinsn  4444  tppreqb  4533  idrefOLD  5727  sotri2  5743  sotri3  5744  somincom  5748  fnun  6211  fvmpti  6505  ovigg  7014  ndmovg  7050  onint  7228  ordsuc  7247  tfindsg  7293  findsg  7326  zfrep6  7367  extmptsuppeq  7556  tfrlem9  7720  tfr3  7734  omlimcl  7898  oneo  7901  nnneo  7971  pssnn  8420  inficl  8573  updjud  9046  dfac2b  9239  dfac2OLD  9241  axdc2lem  9558  axextnd  9701  canthp1lem2  9763  gchinf  9767  inatsk  9888  indpi  10017  ltaddpr2  10145  reclem2pr  10158  supsrlem  10220  axrrecex  10272  zeo  11732  nn0ind-raph  11746  fzm1  12646  fzind2  12813  addmodlteq  12972  bcpasc  13331  pr2pwpr  13481  oddnn02np1  15295  oddge22np1  15296  evennn02n  15297  evennn2n  15298  bitsfzo  15379  bezoutlem1  15478  algcvgblem  15512  coprmdvds1  15587  qredeq  15592  prmreclem2  15841  ramtcl2  15935  divsfval  16415  joinval  17213  meetval  17227  gsumval3  18512  pgpfac1lem3a  18680  fiinopn  20923  restntr  21204  lly1stc  21517  dgradd2  24244  dgrcolem2  24250  asinneg  24833  ftalem2  25020  ftalem4  25022  ftalem5  25023  bpos1lem  25227  zabsle1  25241  lgsqrmodndvds  25298  incistruhgr  26194  fusgrfis  26444  uhgrnbgr0nb  26472  cusgrrusgr  26711  wlkswwlksf1o  27012  wlknwwlksnsurOLD  27023  wlkwwlksurOLD  27031  isclwwlknx  27190  clwwlknwwlksnb  27211  clwlksfoclwwlkOLD  27243  clwlknf1oclwwlknlem1  27251  frgrwopreglem3  27495  frgrreg  27588  frgrregord013  27589  h1de2ctlem  28748  pjclem4a  29391  pj3lem1  29399  chrelat2i  29558  sumdmdii  29608  elim2if  29694  bnj1468  31244  bnj517  31283  axextdist  32030  funtransport  32464  bj-19.21t  33132  bj-projval  33296  areacirc  33819  rngoueqz  34052  isdmn3  34186  ax12fromc15  34686  lkrlspeqN  34953  hlrelat2  35185  ps-1  35259  dalem54  35508  cdleme42c  36254  dihmeetlem6  37091  frege124d  38554  uneqsn  38822  iotavalb  39131  afv2orxorb  41818  iccpartnel  41950  fargshiftf1  41953  pwdif  42077  gbowge7  42227  sbgoldbwt  42241  bgoldbtbndlem1  42269  uspgrsprf1  42324
  Copyright terms: Public domain W3C validator