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

Theorem sylan9bbr 733
 Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
Hypotheses
Ref Expression
sylan9bbr.1 (𝜑 → (𝜓𝜒))
sylan9bbr.2 (𝜃 → (𝜒𝜏))
Assertion
Ref Expression
sylan9bbr ((𝜃𝜑) → (𝜓𝜏))

Proof of Theorem sylan9bbr
StepHypRef Expression
1 sylan9bbr.1 . . 3 (𝜑 → (𝜓𝜒))
2 sylan9bbr.2 . . 3 (𝜃 → (𝜒𝜏))
31, 2sylan9bb 732 . 2 ((𝜑𝜃) → (𝜓𝜏))
43ancoms 468 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:  pm5.75  974  pm5.75OLD  975  sbcom2  2433  sbal1  2448  sbal2  2449  mpteq12f  4661  otthg  4880  fmptsng  6339  f1oiso  6501  mpt2eq123  6612  elovmpt2rab  6778  elovmpt2rab1  6779  ovmpt3rabdm  6790  elovmpt3rab1  6791  tfindsg  6952  findsg  6985  dfoprab4f  7117  opiota  7118  fmpt2x  7125  oalimcl  7527  oeeui  7569  nnmword  7600  isinf  8058  elfi  8202  brwdomn0  8357  alephval3  8816  dfac2  8836  fin17  9099  isfin7-2  9101  ltmpi  9605  addclprlem1  9717  distrlem4pr  9727  1idpr  9730  qreccl  11684  0fz1  12232  zmodid2  12560  ccatrcl1  13229  eqwrds3  13552  divgcdcoprm0  15217  sscntz  17582  gexdvds  17822  cnprest  20903  txrest  21244  ptrescn  21252  flimrest  21597  txflf  21620  fclsrest  21638  tsmssubm  21756  mbfi1fseqlem4  23291  axcontlem7  25650  uhgreq12g  25731  hashecclwwlkn1  26361  usghashecclwwlk  26362  numclwlk1lem2fo  26622  ubthlem1  27110  pjimai  28419  atcv1  28623  chirredi  28637  bj-restsn  32216  wl-sbcom2d-lem1  32521  wl-sbalnae  32524  ptrest  32578  poimirlem28  32607  heicant  32614  ftc1anclem1  32655  sbeqi  33138  ralbi12f  33139  iineq12f  33143  nzss  37538  raaan2  39824  nbuhgr2vtx1edgb  40574  1wlkcomp  40835  uhgr1wlkspthlem2  40960  clWlkcomp  40986  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  av-numclwlk1lem2fo  41525  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848  snlindsntorlem  42053
 Copyright terms: Public domain W3C validator