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

Theorem sylan9bb 512
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 483 . 2 ((𝜑𝜃) → (𝜓𝜒))
3 sylan9bb.2 . . 3 (𝜃 → (𝜒𝜏))
43adantl 484 . 2 ((𝜑𝜃) → (𝜒𝜏))
52, 4bitrd 281 1 ((𝜑𝜃) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398
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 209  df-an 399
This theorem is referenced by:  sylan9bbr  513  baibd  542  syl3an9b  1430  nanbi12  1493  sbcom2  2167  2sb5rf  2495  2sb6rf  2496  eqeq12  2838  eleq12  2905  sbhypf  3555  ceqsrex2v  3654  vtocl2dOLD  3934  sseq12  3997  csbie2df  4395  2ralsng  4619  rexprgf  4634  rextpg  4638  breq12  5074  reusv2lem5  5306  opelopabg  5428  brabg  5429  opelopabgf  5430  opelopab2  5431  rbropapd  5452  ralxpf  5720  feq23  6501  f00  6564  fconstg  6569  f1oeq23  6610  f1o00  6652  fnelfp  6940  fnelnfp  6942  isofrlem  7096  f1oiso  7107  riota1a  7139  cbvmpox  7250  caovord  7362  caovord3  7364  f1oweALT  7676  oaordex  8187  oaass  8190  odi  8208  findcard2s  8762  unfilem1  8785  suppeqfsuppbi  8850  oieu  9006  r1pw  9277  carddomi2  9402  isacn  9473  djudom2  9612  axdc2  9874  alephval2  9997  fpwwe2cbv  10055  fpwwe2lem2  10057  fpwwecbv  10069  fpwwelem  10070  canthwelem  10075  canthwe  10076  distrlem4pr  10451  axpre-sup  10594  nn0ind-raph  12085  elpq  12377  xnn0xadd0  12643  elfz  12901  elfzp12  12989  expeq0  13462  leiso  13820  wrd2ind  14088  trcleq12lem  14356  dfrtrclrec2  14419  shftfib  14434  absdvdsb  15631  dvdsabsb  15632  dvdsabseq  15666  unbenlem  16247  isprs  17543  isdrs  17547  pltval  17573  lublecllem  17601  istos  17648  isdlat  17806  znfld  20710  tgss2  21598  isopn2  21643  cnpf2  21861  lmbr  21869  isreg2  21988  fclsrest  22635  qustgplem  22732  ustuqtoplem  22851  xmetec  23047  nmogelb  23328  metdstri  23462  tcphcph  23843  ulmval  24971  2lgslem1a  25970  iscgrg  26301  istrlson  27491  ispthson  27526  isspthson  27527  elwwlks2on  27741  eupth2lem1  28000  eigrei  29614  eigorthi  29617  jplem1  30048  superpos  30134  chrelati  30144  br8d  30364  issiga  31375  eulerpartlemgvv  31638  cplgredgex  32371  acycgrcycl  32398  br8  32996  br6  32997  br4  32998  brsegle  33573  topfne  33706  tailfb  33729  filnetlem1  33730  nndivsub  33809  bj-elequ12  34016  bj-rest10  34383  isbasisrelowllem1  34640  isbasisrelowllem2  34641  fvineqsnf1  34695  wl-2sb6d  34798  curf  34874  curunc  34878  poimirlem26  34922  mblfinlem2  34934  cnambfre  34944  itgaddnclem2  34955  ftc1anclem1  34971  grpokerinj  35175  rngoisoval  35259  smprngopr  35334  ax12eq  36081  ax12el  36082  2llnjN  36707  2lplnj  36760  elpadd0  36949  lauteq  37235  lpolconN  38627  rexrabdioph  39397  eliunov2  40030  nzss  40655  iotasbc2  40758  or2expropbilem2  43275  elsetpreimafvbi  43558  reuopreuprim  43695  cbvmpox2  44391  line2x  44748
  Copyright terms: Public domain W3C validator