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

Theorem syl113anc 1494
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl3anc.1 (𝜑𝜓)
syl3anc.2 (𝜑𝜒)
syl3anc.3 (𝜑𝜃)
syl3Xanc.4 (𝜑𝜏)
syl23anc.5 (𝜑𝜂)
syl113anc.6 ((𝜓𝜒 ∧ (𝜃𝜏𝜂)) → 𝜁)
Assertion
Ref Expression
syl113anc (𝜑𝜁)

Proof of Theorem syl113anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
63, 4, 53jca 1151 . 2 (𝜑 → (𝜃𝜏𝜂))
7 syl113anc.6 . 2 ((𝜓𝜒 ∧ (𝜃𝜏𝜂)) → 𝜁)
81, 2, 6, 7syl3anc 1483 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  syl123anc  1499  syl213anc  1501  pythagtriplem18  15757  initoeu2  16873  psgnunilem1  18117  mulmarep1gsum1  20594  mulmarep1gsum2  20595  smadiadetlem4  20691  cramerimplem2  20707  cramerlem2  20711  cramer  20714  cnhaus  21376  dishaus  21404  ordthauslem  21405  pthaus  21659  txhaus  21668  xkohaus  21674  regr1lem  21760  methaus  22542  metnrmlem3  22881  f1otrge  25972  axpaschlem  26040  wwlksnwwlksnon  27059  wwlksnwwlksnonOLD  27061  n4cyclfrgr  27472  br8d  29753  lt2addrd  29849  xlt2addrd  29856  br8  31973  br4  31975  nosupres  32179  nosupbnd1lem1  32180  nosupbnd2  32188  btwnxfr  32489  lineext  32509  brsegle  32541  brsegle2  32542  lfl0  34847  lfladd  34848  lflsub  34849  lflmul  34850  lflnegcl  34857  lflvscl  34859  lkrlss  34877  3dimlem3  35243  3dimlem4  35246  3dim3  35251  2llnm3N  35351  2lplnja  35401  4atex  35858  4atex3  35863  trlval4  35970  cdleme7c  36027  cdleme7d  36028  cdleme7ga  36030  cdleme21h  36116  cdleme21i  36117  cdleme21j  36118  cdleme21  36119  cdleme32d  36226  cdleme32f  36228  cdleme35h2  36239  cdleme38m  36245  cdleme40m  36249  cdlemg8  36413  cdlemg11a  36419  cdlemg10a  36422  cdlemg12b  36426  cdlemg12d  36428  cdlemg12f  36430  cdlemg12g  36431  cdlemg15a  36437  cdlemg16  36439  cdlemg16z  36441  cdlemg18a  36460  cdlemg24  36470  cdlemg29  36487  cdlemg33b  36489  cdlemg38  36497  cdlemg39  36498  cdlemg40  36499  cdlemg44b  36514  cdlemj2  36604  cdlemk7  36630  cdlemk12  36632  cdlemk12u  36654  cdlemk32  36679  cdlemk25-3  36686  cdlemk34  36692  cdlemkid3N  36715  cdlemkid4  36716  cdlemk11t  36728  cdlemk53  36739  cdlemk55b  36742  cdleml3N  36760  hdmapln1  37688
  Copyright terms: Public domain W3C validator