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  2112  19.21tOLD  2249  ax12OLD  2372  axext3  2633  ralnralall  4113  elinsn  4277  tppreqb  4368  issref  5544  sotri2  5560  sotri3  5561  somincom  5565  ordelinelOLD  5864  fnun  6035  fvmpti  6320  ovigg  6823  ndmovg  6859  onint  7037  ordsuc  7056  tfindsg  7102  findsg  7135  zfrep6  7176  extmptsuppeq  7364  tfrlem9  7526  tfr3  7540  omlimcl  7703  oneo  7706  nnneo  7776  pssnn  8219  inficl  8372  dfac2  8991  axdc2lem  9308  axextnd  9451  canthp1lem2  9513  gchinf  9517  inatsk  9638  indpi  9767  ltaddpr2  9895  reclem2pr  9908  supsrlem  9970  axrrecex  10022  zeo  11501  nn0ind-raph  11515  fzm1  12458  fzind2  12626  addmodlteq  12785  bcpasc  13148  pr2pwpr  13299  oddnn02np1  15119  oddge22np1  15120  evennn02n  15121  evennn2n  15122  bitsfzo  15204  bezoutlem1  15303  algcvgblem  15337  coprmdvds1  15412  qredeq  15418  prmreclem2  15668  ramtcl2  15762  divsfval  16254  joinval  17052  meetval  17066  gsumval3  18354  pgpfac1lem3a  18521  fiinopn  20754  restntr  21034  lly1stc  21347  dgradd2  24069  dgrcolem2  24075  asinneg  24658  ftalem2  24845  ftalem4  24847  ftalem5  24848  bpos1lem  25052  zabsle1  25066  lgsqrmodndvds  25123  incistruhgr  26019  fusgrfis  26267  uhgrnbgr0nb  26295  cusgrrusgr  26533  wlkpwwlkf1ouspgr  26833  wlknwwlksnsur  26844  wlkwwlksur  26851  isclwwlknx  26998  clwwlknwwlksnb  27019  clwlksfoclwwlk  27050  frgrwopreglem3  27294  frgrreg  27381  frgrregord013  27382  h1de2ctlem  28542  pjclem4a  29185  pj3lem1  29193  chrelat2i  29352  sumdmdii  29402  elim2if  29489  bnj1468  31042  bnj517  31081  axextdist  31829  funtransport  32263  bj-19.21t  32942  bj-projval  33109  areacirc  33635  rngoueqz  33869  isdmn3  34003  ax12fromc15  34509  lkrlspeqN  34776  hlrelat2  35007  ps-1  35081  dalem54  35330  cdleme42c  36077  dihmeetlem6  36915  frege124d  38370  uneqsn  38638  iotavalb  38948  iccpartnel  41699  fargshiftf1  41702  pwdif  41826  gbowge7  41976  sbgoldbwt  41990  bgoldbtbndlem1  42018  uspgrsprf1  42080
 Copyright terms: Public domain W3C validator