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

Theorem syl6bir 244
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 238 . 2 (𝜑 → (𝜓𝜒))
3 syl6bir.2 . 2 (𝜒𝜃)
42, 3syl6 35 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:  19.21tOLDOLD  2230  19.21tOLD  2375  axext3  2753  ralnralall  4219  elinsn  4382  tppreqb  4471  issref  5650  sotri2  5666  sotri3  5667  somincom  5671  ordelinelOLD  5969  fnun  6137  fvmpti  6423  ovigg  6928  ndmovg  6964  onint  7142  ordsuc  7161  tfindsg  7207  findsg  7240  zfrep6  7281  extmptsuppeq  7470  tfrlem9  7634  tfr3  7648  omlimcl  7812  oneo  7815  nnneo  7885  pssnn  8334  inficl  8487  updjud  8960  dfac2b  9153  dfac2OLD  9155  axdc2lem  9472  axextnd  9615  canthp1lem2  9677  gchinf  9681  inatsk  9802  indpi  9931  ltaddpr2  10059  reclem2pr  10072  supsrlem  10134  axrrecex  10186  zeo  11665  nn0ind-raph  11679  fzm1  12627  fzind2  12794  addmodlteq  12953  bcpasc  13312  pr2pwpr  13463  oddnn02np1  15280  oddge22np1  15281  evennn02n  15282  evennn2n  15283  bitsfzo  15365  bezoutlem1  15464  algcvgblem  15498  coprmdvds1  15573  qredeq  15578  prmreclem2  15828  ramtcl2  15922  divsfval  16415  joinval  17213  meetval  17227  gsumval3  18515  pgpfac1lem3a  18683  fiinopn  20926  restntr  21207  lly1stc  21520  dgradd2  24244  dgrcolem2  24250  asinneg  24834  ftalem2  25021  ftalem4  25023  ftalem5  25024  bpos1lem  25228  zabsle1  25242  lgsqrmodndvds  25299  incistruhgr  26195  fusgrfis  26445  uhgrnbgr0nb  26473  cusgrrusgr  26712  wlkswwlksf1o  27013  wlknwwlksnsurOLD  27024  wlkwwlksurOLD  27032  isclwwlknx  27191  clwwlknwwlksnb  27212  clwlksfoclwwlkOLD  27244  clwlknf1oclwwlknlem1  27252  frgrwopreglem3  27496  frgrreg  27593  frgrregord013  27594  h1de2ctlem  28754  pjclem4a  29397  pj3lem1  29405  chrelat2i  29564  sumdmdii  29614  elim2if  29701  bnj1468  31254  bnj517  31293  axextdist  32041  funtransport  32475  bj-19.21t  33152  bj-projval  33315  areacirc  33837  rngoueqz  34071  isdmn3  34205  ax12fromc15  34713  lkrlspeqN  34980  hlrelat2  35211  ps-1  35285  dalem54  35534  cdleme42c  36281  dihmeetlem6  37119  frege124d  38579  uneqsn  38847  iotavalb  39157  iccpartnel  41902  fargshiftf1  41905  pwdif  42029  gbowge7  42179  sbgoldbwt  42193  bgoldbtbndlem1  42221  uspgrsprf1  42283
  Copyright terms: Public domain W3C validator