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

Theorem sylan9bb 732
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 480 . 2 ((𝜑𝜃) → (𝜓𝜒))
3 sylan9bb.2 . . 3 (𝜃 → (𝜒𝜏))
43adantl 481 . 2 ((𝜑𝜃) → (𝜒𝜏))
52, 4bitrd 267 1 ((𝜑𝜃) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  sylan9bbr  733  bi2anan9  913  baibd  946  rbaibd  947  syl3an9b  1389  nanbi12  1449  sbcom2  2433  2sb5rf  2439  2sb6rf  2440  eqeq12  2623  eleq12  2678  sbhypf  3226  ceqsrex2v  3308  sseq12  3591  2ralsng  4167  rexprg  4182  rextpg  4184  breq12  4588  reusv2lem5  4799  opelopabg  4918  brabg  4919  opelopabgf  4920  opelopab2  4921  rbropapd  4939  ralxpf  5190  feq23  5942  f00  6000  fconstg  6005  f1oeq23  6043  f1o00  6083  fnelfp  6346  fnelnfp  6348  isofrlem  6490  f1oiso  6501  riota1a  6530  cbvmpt2x  6631  caovord  6743  caovord3  6745  f1oweALT  7043  oaordex  7525  oaass  7528  odi  7546  findcard2s  8086  unfilem1  8109  suppeqfsuppbi  8172  oieu  8327  r1pw  8591  carddomi2  8679  isacn  8750  cdadom2  8892  axdc2  9154  alephval2  9273  fpwwe2cbv  9331  fpwwe2lem2  9333  fpwwecbv  9345  fpwwelem  9346  canthwelem  9351  canthwe  9352  distrlem4pr  9727  axpre-sup  9869  nn0ind-raph  11353  xnn0xadd0  11949  elfz  12203  elfzp12  12288  expeq0  12752  leiso  13100  wrd2ind  13329  trcleq12lem  13580  dfrtrclrec2  13645  shftfib  13660  absdvdsb  14838  dvdsabsb  14839  dvdsabseq  14873  unbenlem  15450  isprs  16753  isdrs  16757  pltval  16783  lublecllem  16811  istos  16858  isdlat  17016  znfld  19728  tgss2  20602  isopn2  20646  cnpf2  20864  lmbr  20872  isreg2  20991  fclsrest  21638  qustgplem  21734  ustuqtoplem  21853  xmetec  22049  nmogelb  22330  metdstri  22462  tchcph  22844  ulmval  23938  2lgslem1a  24916  iscgrg  25207  eupath2lem1  26504  eigrei  28077  eigorthi  28080  jplem1  28511  superpos  28597  chrelati  28607  br8d  28802  issiga  29501  eulerpartlemgvv  29765  br8  30899  br6  30900  br4  30901  brsegle  31385  topfne  31519  tailfb  31542  filnetlem1  31543  nndivsub  31626  bj-elequ12  31855  bj-rest10  32222  isbasisrelowllem1  32379  isbasisrelowllem2  32380  wl-2sb6d  32520  curf  32557  curunc  32561  poimirlem26  32605  mblfinlem2  32617  cnambfre  32628  itgaddnclem2  32639  ftc1anclem1  32655  grpokerinj  32862  rngoisoval  32946  smprngopr  33021  ax12eq  33244  ax12el  33245  2llnjN  33871  2lplnj  33924  elpadd0  34113  lauteq  34399  lpolconN  35794  rexrabdioph  36376  eliunov2  36990  nzss  37538  iotasbc2  37643  istrlson  40914  ispthson  40948  isspthson  40949  elwwlks2on  41162  eupth2lem1  41386  cbvmpt2x2  41907
  Copyright terms: Public domain W3C validator