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

Theorem syl6bir 254
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 248 . 2 (𝜑 → (𝜓𝜒))
3 syl6bir.2 . 2 (𝜒𝜃)
42, 3syl6 35 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  ralnralall  4477  elinsn  4672  tppreqb  4766  sotri2  6084  sotri3  6085  somincom  6089  fnun  6615  fvmpti  6948  ovigg  7501  ndmovg  7538  onint  7726  ordsucOLD  7750  tfindsg  7798  findsg  7837  zfrep6  7888  poxp2  8076  extmptsuppeq  8120  tfrlem9  8332  tfr3  8346  omlimcl  8526  oneo  8529  nnneo  8602  pssnn  9115  onomeneq  9175  pssnnOLD  9212  inficl  9366  frmin  9690  updjud  9875  dfac2b  10071  axdc2lem  10389  axextnd  10532  canthp1lem2  10594  gchinf  10598  inatsk  10719  indpi  10848  ltaddpr2  10976  reclem2pr  10989  supsrlem  11052  axrrecex  11104  zeo  12594  nn0ind-raph  12608  fzm1  13527  fzind2  13696  addmodlteq  13857  bcpasc  14227  pr2pwpr  14384  swrdnnn0nd  14550  pwdif  15758  oddnn02np1  16235  oddge22np1  16236  evennn02n  16237  evennn2n  16238  bitsfzo  16320  bezoutlem1  16425  algcvgblem  16458  coprmdvds1  16533  qredeq  16538  prmreclem2  16794  ramtcl2  16888  divsfval  17434  joinval  18271  meetval  18285  gsumval3  19689  pgpfac1lem3a  19860  fiinopn  22266  restntr  22549  lly1stc  22863  dgradd2  25645  dgrcolem2  25651  asinneg  26252  ftalem2  26439  ftalem4  26441  ftalem5  26442  bpos1lem  26646  zabsle1  26660  lgsqrmodndvds  26717  incistruhgr  28072  fusgrfis  28320  uhgrnbgr0nb  28344  cusgrrusgr  28571  wlkswwlksf1o  28866  isclwwlknx  29022  clwwlknwwlksnb  29041  clwlknf1oclwwlknlem1  29067  frgrwopreglem3  29300  frgrreg  29380  frgrregord013  29381  h1de2ctlem  30539  pjclem4a  31182  pj3lem1  31190  chrelat2i  31349  sumdmdii  31399  elim2if  31509  bnj1468  33515  bnj517  33554  acycgrislfgr  33803  axextdist  34430  funtransport  34662  bj-19.21t0  35341  bj-projval  35513  areacirc  36217  rngoueqz  36445  isdmn3  36579  ax12fromc15  37413  lkrlspeqN  37679  hlrelat2  37912  ps-1  37986  dalem54  38235  cdleme42c  38981  dihmeetlem6  39818  oe0suclim  41655  sdomne0  41773  sdomne0d  41774  frege124d  42121  uneqsn  42385  iotavalb  42798  natglobalincr  45202  2reuimp  45433  afv2orxorb  45546  iccpartnel  45716  fargshiftf1  45719  gbowge7  46041  sbgoldbwt  46055  bgoldbtbndlem1  46083  uspgrsprf1  46135
  Copyright terms: Public domain W3C validator