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

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

Proof of Theorem syl222anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . 2 (𝜑𝜃)
4 syl3Xanc.4 . 2 (𝜑𝜏)
5 syl23anc.5 . . 3 (𝜑𝜂)
6 syl33anc.6 . . 3 (𝜑𝜁)
75, 6jca 515 . 2 (𝜑 → (𝜂𝜁))
8 syl222anc.7 . 2 (((𝜓𝜒) ∧ (𝜃𝜏) ∧ (𝜂𝜁)) → 𝜎)
91, 2, 3, 4, 7, 8syl221anc 1378 1 (𝜑𝜎)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  3anandis  1468  3anandirs  1469  omopth2  8202  omeu  8203  dfac12lem2  9564  xaddass2  12638  xpncan  12639  divdenle  16085  pockthlem  16237  znidomb  20703  tanord1  25127  ang180lem5  25397  isosctrlem3  25404  log2tlbnd  25529  basellem1  25664  perfectlem2  25812  bposlem6  25871  dchrisum0flblem2  26091  pntpbnd1a  26167  axcontlem8  26763  xlt2addrd  30488  s2f1  30627  xrge0addass  30704  xrge0npcan  30708  submatminr1  31105  carsgclctunlem2  31604  4atexlemntlpq  37276  4atexlemnclw  37278  trlval2  37371  cdleme0moN  37433  cdleme16b  37487  cdleme16c  37488  cdleme16d  37489  cdleme16e  37490  cdleme17c  37496  cdlemeda  37506  cdleme20h  37524  cdleme20j  37526  cdleme20l2  37529  cdleme21c  37535  cdleme21ct  37537  cdleme22aa  37547  cdleme22cN  37550  cdleme22d  37551  cdleme22e  37552  cdleme22eALTN  37553  cdleme23b  37558  cdleme25a  37561  cdleme25dN  37564  cdleme27N  37577  cdleme28a  37578  cdleme28b  37579  cdleme29ex  37582  cdleme32c  37651  cdleme42k  37692  cdlemg2cex  37799  cdlemg2idN  37804  cdlemg31c  37907  cdlemk5a  38043  cdlemk5  38044  congmul  39764  jm2.25lem1  39795  jm2.26  39799  jm2.27a  39802  infleinflem1  41868  stoweidlem42  42550
  Copyright terms: Public domain W3C validator