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

Theorem sylan9bb 510
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 481 . 2 ((𝜑𝜃) → (𝜓𝜒))
3 sylan9bb.2 . . 3 (𝜃 → (𝜒𝜏))
43adantl 482 . 2 ((𝜑𝜃) → (𝜒𝜏))
52, 4bitrd 278 1 ((𝜑𝜃) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396
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  df-an 397
This theorem is referenced by:  sylan9bbr  511  baibd  540  syl3an9b  1434  nanbi12  1501  sbcom2  2161  2sb5rf  2470  2sb6rf  2471  eqeqan12d  2750  eqeq12OLD  2755  eleq12  2827  sbhypfOLD  3506  ceqsrex2v  3606  elabd2  3620  sseq12  3969  csbie2df  4398  2ralsng  4635  rexprgf  4652  rextpg  4658  breq12  5108  reusv2lem5  5355  opelopabg  5493  brabg  5494  opelopabgf  5495  opelopab2  5496  rbropapd  5519  ralxpf  5800  feq23  6649  f00  6721  fconstg  6726  f1oeq23  6772  f1o00  6816  fnelfp  7117  fnelnfp  7119  isofrlem  7281  f1oiso  7292  riota1a  7332  cbvmpox  7446  caovord  7561  caovord3  7563  f1oweALT  7901  oaordex  8501  oaass  8504  odi  8522  findcard2s  9105  unfilem1  9250  suppeqfsuppbi  9315  oieu  9471  r1pw  9777  carddomi2  9902  isacn  9976  djudom2  10115  axdc2  10381  alephval2  10504  fpwwe2cbv  10562  fpwwe2lem2  10564  fpwwecbv  10576  fpwwelem  10577  canthwelem  10582  canthwe  10583  distrlem4pr  10958  axpre-sup  11101  nn0ind-raph  12599  elpq  12892  xnn0xadd0  13158  elfz  13422  elfzp12  13512  expeq0  13990  leiso  14350  wrd2ind  14603  trcleq12lem  14870  dfrtrclrec2  14935  shftfib  14949  absdvdsb  16149  dvdsabsb  16150  dvdsabseq  16187  unbenlem  16772  isprs  18178  isdrs  18182  pltval  18213  lublecllem  18241  istos  18299  isdlat  18403  znfld  20952  tgss2  22321  isopn2  22367  cnpf2  22585  lmbr  22593  isreg2  22712  fclsrest  23359  qustgplem  23456  ustuqtoplem  23575  xmetec  23771  nmogelb  24064  metdstri  24198  tcphcph  24585  ulmval  25723  2lgslem1a  26723  elmade  27181  iscgrg  27340  istrlson  28541  ispthson  28576  isspthson  28577  elwwlks2on  28790  eupth2lem1  29048  eigrei  30662  eigorthi  30665  jplem1  31096  superpos  31182  chrelati  31192  br8d  31415  issiga  32580  eulerpartlemgvv  32845  cplgredgex  33583  acycgrcycl  33610  br8  34199  br6  34200  br4  34201  brsegle  34660  topfne  34793  tailfb  34816  filnetlem1  34817  nndivsub  34896  bj-elequ12  35110  bj-rest10  35526  isbasisrelowllem1  35793  isbasisrelowllem2  35794  fvineqsnf1  35848  wl-2sb6d  35980  curf  36023  curunc  36027  poimirlem26  36071  mblfinlem2  36083  cnambfre  36093  itgaddnclem2  36104  ftc1anclem1  36118  grpokerinj  36319  rngoisoval  36403  smprngopr  36478  parteq12  37205  ax12eq  37370  ax12el  37371  2llnjN  37997  2lplnj  38050  elpadd0  38239  lauteq  38525  lpolconN  39917  rexrabdioph  41055  eliunov2  41893  nzss  42539  iotasbc2  42642  or2expropbilem2  45199  elsetpreimafvbi  45515  reuopreuprim  45650  cbvmpox2  46343  naryfvalel  46648  line2x  46772
  Copyright terms: Public domain W3C validator