MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylan9bbr Unicode version

Theorem sylan9bbr 700
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
Hypotheses
Ref Expression
sylan9bbr.1
sylan9bbr.2
Assertion
Ref Expression
sylan9bbr

Proof of Theorem sylan9bbr
StepHypRef Expression
1 sylan9bbr.1 . . 3
2 sylan9bbr.2 . . 3
31, 2sylan9bb 699 . 2
43ancoms 453 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  pm5.75  937  sbcom2  2189  sbal1  2204  sbal2  2205  2eu6OLD  2384  mpteq12f  4528  fmptsng  6092  fconstfvOLD  6134  f1oiso  6247  mpt2eq123  6356  elovmpt2rab  6521  elovmpt2rab1  6522  ovmpt3rabdm  6535  elovmpt3rab1  6536  tfindsg  6695  findsg  6727  dfoprab4f  6858  opiota  6859  fmpt2x  6866  oalimcl  7228  oeeui  7270  nnmword  7301  isinf  7753  elfi  7893  brwdomn0  8016  alephval3  8512  dfac2  8532  fin17  8795  isfin7-2  8797  ltmpi  9303  addclprlem1  9415  distrlem4pr  9425  1idpr  9428  qreccl  11231  0fz1  11734  zmodid2  12024  hashle00  12465  hashfzdm  12498  hashfirdm  12500  xpnnenOLD  13943  dvdseq  14033  sscntz  16364  gexdvds  16604  cnprest  19790  txrest  20132  ptrescn  20140  flimrest  20484  txflf  20507  fclsrest  20525  tsmssubm  20644  mbfi1fseqlem4  22125  axcontlem7  24273  hashecclwwlkn1  24834  usghashecclwwlk  24835  numclwlk1lem2fo  25095  ubthlem1  25786  pjimai  27095  atcv1  27299  chirredi  27313  wl-sbcom2d-lem1  30009  wl-sbalnae  30012  ptrest  30048  heicant  30049  ftc1anclem1  30090  sbeqi  30568  ralbi12f  30569  iineq12f  30573  nzss  31222  raaan2  32180  uhgeq12g  32370  usgpredgv  32399  usgpredgvALT  32400  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  snlindsntorlem  33071
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  df-an 371
  Copyright terms: Public domain W3C validator