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  2471  2sb6rf  2472  eqeqan12d  2751  eqeq12OLD  2756  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  7330  cbvmpox  7444  caovord  7559  caovord3  7561  f1oweALT  7897  oaordex  8497  oaass  8500  odi  8518  findcard2s  9067  unfilem1  9212  suppeqfsuppbi  9277  oieu  9433  r1pw  9739  carddomi2  9864  isacn  9938  djudom2  10077  axdc2  10343  alephval2  10466  fpwwe2cbv  10524  fpwwe2lem2  10526  fpwwecbv  10538  fpwwelem  10539  canthwelem  10544  canthwe  10545  distrlem4pr  10920  axpre-sup  11063  nn0ind-raph  12561  elpq  12854  xnn0xadd0  13120  elfz  13384  elfzp12  13474  expeq0  13952  leiso  14312  wrd2ind  14569  trcleq12lem  14838  dfrtrclrec2  14903  shftfib  14917  absdvdsb  16117  dvdsabsb  16118  dvdsabseq  16155  unbenlem  16740  isprs  18146  isdrs  18150  pltval  18181  lublecllem  18209  istos  18267  isdlat  18371  znfld  20920  tgss2  22289  isopn2  22335  cnpf2  22553  lmbr  22561  isreg2  22680  fclsrest  23327  qustgplem  23424  ustuqtoplem  23543  xmetec  23739  nmogelb  24032  metdstri  24166  tcphcph  24553  ulmval  25691  2lgslem1a  26691  elmade  27149  iscgrg  27283  istrlson  28484  ispthson  28519  isspthson  28520  elwwlks2on  28733  eupth2lem1  28991  eigrei  30605  eigorthi  30608  jplem1  31039  superpos  31125  chrelati  31135  br8d  31358  issiga  32523  eulerpartlemgvv  32788  cplgredgex  33526  acycgrcycl  33553  br8  34145  br6  34146  br4  34147  brsegle  34631  topfne  34764  tailfb  34787  filnetlem1  34788  nndivsub  34867  bj-elequ12  35081  bj-rest10  35497  isbasisrelowllem1  35764  isbasisrelowllem2  35765  fvineqsnf1  35819  wl-2sb6d  35951  curf  35994  curunc  35998  poimirlem26  36042  mblfinlem2  36054  cnambfre  36064  itgaddnclem2  36075  ftc1anclem1  36089  grpokerinj  36290  rngoisoval  36374  smprngopr  36449  parteq12  37176  ax12eq  37341  ax12el  37342  2llnjN  37968  2lplnj  38021  elpadd0  38210  lauteq  38496  lpolconN  39888  rexrabdioph  41026  eliunov2  41862  nzss  42508  iotasbc2  42611  or2expropbilem2  45168  elsetpreimafvbi  45484  reuopreuprim  45619  cbvmpox2  46312  naryfvalel  46617  line2x  46741
  Copyright terms: Public domain W3C validator