Theorem syl6bir 229

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

Step	Hyp	Ref	Expression
1		syl6bir.1	. . 3
2	1	biimprd 223	. 2
3		syl6bir.2	. 2
4	2, 3	syl6 33	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  19.21t  1904  ax12  2234  axext3  2437  tppreqb  4171  reusv6OLD  4663  ordelinel  4981  issref  5385  sotri2  5401  sotri3  5402  somincom  5409  fnun  5692  fvmpti  5955  ovigg  6423  ndmovg  6458  onint  6630  ordsuc  6649  tfindsg  6695  findsg  6727  zfrep6  6768  extmptsuppeq  6943  tfrlem9  7073  tfr3  7087  omlimcl  7246  oneo  7249  nnneo  7319  pssnn  7758  inficl  7905  dfac2  8532  axdc2lem  8849  axextnd  8987  canthp1lem2  9052  gchinf  9056  inatsk  9177  indpi  9306  ltaddpr2  9434  reclem2pr  9447  supsrlem  9509  axrrecex  9561  zeo  10973  nn0ind-raph  10989  fzm1  11787  fzind2  11924  bcpasc  12399  pr2pwpr  12520  bitsfzo  14085  bezoutlem1  14176  algcvgblem  14206  qredeq  14247  prmreclem2  14435  ramtcl2  14529  divsfval  14944  joinval  15635  meetval  15649  gsumval3OLD  16908  gsumval3  16911  pgpfac1lem3a  17127  fiinopn  19410  restntr  19683  lly1stc  19997  dgradd2  22665  dgrcolem2  22671  asinneg  23217  ftalem2  23347  ftalem4  23349  ftalem5  23350  bpos1lem  23557  wlkdvspthlem  24609  fargshiftf1  24637  wlknwwlknsur  24712  wlkiswwlksur  24719  clwlkfoclwwlk  24845  hashnbgravdg  24913  cusgraisrusgra  24938  frgrareg  25117  frgraregord013  25118  rngoueqz  25432  h1de2ctlem  26473  pjclem4a  27117  pj3lem1  27125  chrelat2i  27284  sumdmdii  27334  elim2if  27422  axextdist  29232  funtransport  29681  areacirc  30112  isdmn3  30471  iotavalb  31337  ralnralall  32294  bnj1468  33904  bnj517  33943  bj-19.21t  34403  bj-projval  34554  lkrlspeqN  34896  hlrelat2  35127  ps-1  35201  dalem54  35450  cdleme42c  36198  dihmeetlem6  37036

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 185