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

Theorem sylan9bb 513
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 484 . 2 ((𝜑𝜃) → (𝜓𝜒))
3 sylan9bb.2 . . 3 (𝜃 → (𝜒𝜏))
43adantl 485 . 2 ((𝜑𝜃) → (𝜒𝜏))
52, 4bitrd 282 1 ((𝜑𝜃) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  sylan9bbr  514  baibd  543  syl3an9b  1436  nanbi12  1499  sbcom2  2167  2sb5rf  2473  2sb6rf  2474  eqeqan12d  2753  eqeq12OLD  2758  eleq12  2829  sbhypf  3482  ceqsrex2v  3580  elabd2  3594  sseq12  3944  csbie2df  4371  2ralsng  4608  rexprgf  4625  rextpg  4631  breq12  5074  reusv2lem5  5311  opelopabg  5435  brabg  5436  opelopabgf  5437  opelopab2  5438  rbropapd  5459  ralxpf  5732  feq23  6550  f00  6622  fconstg  6627  f1oeq23  6673  f1o00  6716  fnelfp  7011  fnelnfp  7013  isofrlem  7170  f1oiso  7181  riota1a  7214  cbvmpox  7325  caovord  7440  caovord3  7442  f1oweALT  7766  oaordex  8309  oaass  8312  odi  8330  findcard2s  8868  unfilem1  8964  suppeqfsuppbi  9028  oieu  9184  r1pw  9490  carddomi2  9615  isacn  9687  djudom2  9826  axdc2  10092  alephval2  10215  fpwwe2cbv  10273  fpwwe2lem2  10275  fpwwecbv  10287  fpwwelem  10288  canthwelem  10293  canthwe  10294  distrlem4pr  10669  axpre-sup  10812  nn0ind-raph  12306  elpq  12600  xnn0xadd0  12866  elfz  13130  elfzp12  13220  expeq0  13697  leiso  14057  wrd2ind  14320  trcleq12lem  14588  dfrtrclrec2  14653  shftfib  14667  absdvdsb  15868  dvdsabsb  15869  dvdsabseq  15906  unbenlem  16493  isprs  17836  isdrs  17840  pltval  17870  lublecllem  17898  istos  17956  isdlat  18060  znfld  20557  tgss2  21915  isopn2  21960  cnpf2  22178  lmbr  22186  isreg2  22305  fclsrest  22952  qustgplem  23049  ustuqtoplem  23168  xmetec  23363  nmogelb  23645  metdstri  23779  tcphcph  24165  ulmval  25303  2lgslem1a  26303  iscgrg  26634  istrlson  27825  ispthson  27860  isspthson  27861  elwwlks2on  28074  eupth2lem1  28332  eigrei  29946  eigorthi  29949  jplem1  30380  superpos  30466  chrelati  30476  br8d  30700  issiga  31823  eulerpartlemgvv  32086  cplgredgex  32825  acycgrcycl  32852  br8  33472  br6  33473  br4  33474  elmade  33821  brsegle  34180  topfne  34313  tailfb  34336  filnetlem1  34337  nndivsub  34416  bj-elequ12  34630  bj-rest10  35029  isbasisrelowllem1  35299  isbasisrelowllem2  35300  fvineqsnf1  35354  wl-2sb6d  35486  curf  35528  curunc  35532  poimirlem26  35576  mblfinlem2  35588  cnambfre  35598  itgaddnclem2  35609  ftc1anclem1  35623  grpokerinj  35824  rngoisoval  35908  smprngopr  35983  ax12eq  36728  ax12el  36729  2llnjN  37354  2lplnj  37407  elpadd0  37596  lauteq  37882  lpolconN  39274  rexrabdioph  40366  eliunov2  41011  nzss  41655  iotasbc2  41758  or2expropbilem2  44244  elsetpreimafvbi  44561  reuopreuprim  44696  cbvmpox2  45389  naryfvalel  45694  line2x  45818
  Copyright terms: Public domain W3C validator