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  2072  19.21tOLD  2211  ax12OLD  2339  axext3  2602  ralnralall  4071  elinsn  4236  tppreqb  4327  issref  5497  sotri2  5513  sotri3  5514  somincom  5518  ordelinelOLD  5814  fnun  5985  fvmpti  6268  ovigg  6766  ndmovg  6802  onint  6980  ordsuc  6999  tfindsg  7045  findsg  7078  zfrep6  7119  extmptsuppeq  7304  tfrlem9  7466  tfr3  7480  omlimcl  7643  oneo  7646  nnneo  7716  pssnn  8163  inficl  8316  dfac2  8938  axdc2lem  9255  axextnd  9398  canthp1lem2  9460  gchinf  9464  inatsk  9585  indpi  9714  ltaddpr2  9842  reclem2pr  9855  supsrlem  9917  axrrecex  9969  zeo  11448  nn0ind-raph  11462  fzm1  12404  fzind2  12569  addmodlteq  12728  bcpasc  13091  pr2pwpr  13244  oddnn02np1  15053  oddge22np1  15054  evennn02n  15055  evennn2n  15056  bitsfzo  15138  bezoutlem1  15237  algcvgblem  15271  coprmdvds1  15346  qredeq  15352  prmreclem2  15602  ramtcl2  15696  divsfval  16188  joinval  16986  meetval  17000  gsumval3  18289  pgpfac1lem3a  18456  fiinopn  20687  restntr  20967  lly1stc  21280  dgradd2  24005  dgrcolem2  24011  asinneg  24594  ftalem2  24781  ftalem4  24783  ftalem5  24784  bpos1lem  24988  zabsle1  25002  lgsqrmodndvds  25059  incistruhgr  25955  fusgrfis  26203  uhgrnbgr0nb  26231  cusgrrusgr  26458  wlkpwwlkf1ouspgr  26746  wlknwwlksnsur  26757  wlkwwlksur  26764  clwlksfoclwwlk  26943  frgrwopreglem3  27156  frgrreg  27222  frgrregord013  27223  h1de2ctlem  28384  pjclem4a  29027  pj3lem1  29035  chrelat2i  29194  sumdmdii  29244  elim2if  29335  bnj1468  30890  bnj517  30929  axextdist  31679  funtransport  32113  bj-19.21t  32792  bj-projval  32959  areacirc  33476  rngoueqz  33710  isdmn3  33844  ax12fromc15  34009  lkrlspeqN  34277  hlrelat2  34508  ps-1  34582  dalem54  34831  cdleme42c  35579  dihmeetlem6  36417  frege124d  37872  uneqsn  38141  iotavalb  38451  iccpartnel  41138  fargshiftf1  41141  pwdif  41266  gbowge7  41416  sbgoldbwt  41430  bgoldbtbndlem1  41458  uspgrsprf1  41520
  Copyright terms: Public domain W3C validator