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

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

Proof of Theorem sylan9bb
StepHypRef Expression
1 sylan9bb.1 . . 3
21adantr 465 . 2
3 sylan9bb.2 . . 3
43adantl 466 . 2
52, 4bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  sylan9bbr  700  bi2anan9  873  baibd  909  rbaibd  910  syl3an9b  1297  nanbi12  1356  sbcom2  2189  2sb5rf  2195  2sb6rf  2196  ax12eq  2271  ax12el  2272  eqeq12  2476  eleq12  2533  sbhypf  3156  ceqsrex2v  3235  sseq12  3526  2ralsng  4066  rexprg  4079  rextpg  4081  breq12  4457  reusv2lem5  4657  opelopabg  4770  brabg  4771  opelopab2  4773  ralxpf  5154  feq23  5721  f00  5772  fconstg  5777  f1oeq23  5815  f1o00  5853  fnelfp  6099  fnelnfp  6101  isofrlem  6236  f1oiso  6247  riota1a  6277  cbvmpt2x  6375  caovord  6486  caovord3  6488  f1oweALT  6784  oaordex  7226  oaass  7229  odi  7247  findcard2s  7781  unfilem1  7804  suppeqfsuppbi  7863  oieu  7985  r1pw  8284  carddomi2  8372  isacn  8446  cdadom2  8588  axdc2  8850  alephval2  8968  fpwwe2cbv  9029  fpwwe2lem2  9031  fpwwecbv  9043  fpwwelem  9044  canthwelem  9049  canthwe  9050  distrlem4pr  9425  axpre-sup  9567  nn0ind-raph  10989  elfz  11707  elfzp12  11786  expeq0  12196  leiso  12508  wrd2ind  12703  shftfib  12905  absdvdsb  14002  dvdsabsb  14003  unbenlem  14426  isprs  15559  isdrs  15563  pltval  15590  lublecllem  15618  istos  15665  isdlat  15823  znfld  18599  tgss2  19489  isopn2  19533  cnpf2  19751  lmbr  19759  isreg2  19878  fclsrest  20525  qustgplem  20619  ustuqtoplem  20742  xmetec  20937  nmogelb  21223  metdstri  21355  tchcph  21680  ulmval  22775  iscgrg  23904  eupath2lem1  24977  eigrei  26753  eigorthi  26756  jplem1  27187  superpos  27273  chrelati  27283  br8d  27463  issiga  28111  eulerpartlemgvv  28315  dfrtrclrec2  29066  br8  29185  br6  29186  br4  29187  brsegle  29758  nndivsub  29922  wl-2sb6d  30008  mblfinlem2  30052  cnambfre  30063  itgaddnclem2  30074  ftc1anclem1  30090  topfne  30172  tailfb  30195  filnetlem1  30196  grpokerinj  30347  rngoisoval  30380  smprngopr  30449  rexrabdioph  30727  nzss  31222  iotasbc2  31327  uhg0e  32376  cbvmpt2x2  32925  bj-elequ12  34239  2llnjN  35291  2lplnj  35344  elpadd0  35533  lauteq  35819  lpolconN  37214
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