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

Theorem sylan9bbr 511
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 510 . 2 ((𝜑𝜃) → (𝜓𝜏))
43ancoms 459 1 ((𝜃𝜑) → (𝜓𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  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 208  df-an 397
This theorem is referenced by:  bimsc1  840  pm5.75  1024  sbcom2  2160  sbal1  2570  sbal2  2571  sbal2OLD  2572  raaan2  4467  mpteq12f  5146  otthg  5374  fmptsng  6928  f1oiso  7098  mpoeq123  7220  elovmporab  7385  elovmporab1w  7386  elovmporab1  7387  ovmpt3rabdm  7398  elovmpt3rab1  7399  tfindsg  7568  findsg  7602  dfoprab4f  7750  opiota  7753  fmpox  7761  oalimcl  8181  oeeui  8223  nnmword  8254  isinf  8725  elfi  8871  brwdomn0  9027  alephval3  9530  dfac2b  9550  fin17  9810  isfin7-2  9812  ltmpi  10320  addclprlem1  10432  distrlem4pr  10442  1idpr  10445  qreccl  12363  0fz1  12922  zmodid2  13262  ccatrcl1  13943  eqwrds3  14320  divgcdcoprm0  16004  sscntz  18401  gexdvds  18645  cnprest  21832  txrest  22174  ptrescn  22182  flimrest  22526  txflf  22549  fclsrest  22567  tsmssubm  22685  mbfi1fseqlem4  24253  2sq2  25942  axcontlem7  26689  uhgreq12g  26783  nbuhgr2vtx1edgb  27067  wlkcomp  27345  uhgrwkspthlem2  27468  clwlkcomp  27493  wlknwwlksnbij  27599  hashecclwwlkn1  27789  umgrhashecclwwlk  27790  numclwwlk1lem2fo  28070  ubthlem1  28580  pjimai  29886  atcv1  30090  chirredi  30104  bj-restsn  34273  fvineqsneu  34580  pibt2  34586  wl-sbcom2d-lem1  34681  wl-sbalnae  34684  ptrest  34777  poimirlem28  34806  heicant  34813  ftc1anclem1  34853  sbeqi  35324  ralbi12f  35325  iineq12f  35329  brcnvepres  35415  nzss  40533  or2expropbilem1  43152  ich2exprop  43484  ichnreuop  43485  ichreuopeq  43486  reuopreuprim  43539  rngcinv  44154  rngcinvALTV  44166  ringcinv  44205  ringcinvALTV  44229  snlindsntorlem  44427  itscnhlc0xyqsol  44654
  Copyright terms: Public domain W3C validator