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

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

Proof of Theorem syl221anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
53, 4jca 554 . 2 (𝜑 → (𝜃𝜏))
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl221anc.6 . 2 (((𝜓𝜒) ∧ (𝜃𝜏) ∧ 𝜂) → 𝜁)
81, 2, 5, 6, 7syl211anc 1329 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  syl222anc  1339  vtocldf  3245  f1oprswap  6142  dmdcand  10782  modmul12d  12672  modnegd  12673  modadd12d  12674  exprec  12849  splval2  13453  eulerthlem2  15422  fermltl  15424  odzdvds  15435  efgredleme  18088  efgredlemc  18090  blssps  22152  blss  22153  metequiv2  22238  met1stc  22249  met2ndci  22250  metdstri  22577  xlebnum  22687  caubl  23029  divcxp  24350  cxple2a  24362  cxplead  24384  cxplt2d  24389  cxple2d  24390  mulcxpd  24391  ang180  24461  wilthlem2  24712  lgslem4  24942  lgsvalmod  24958  lgsmod  24965  lgsdir2lem4  24970  lgsdirprm  24973  lgsne0  24977  lgseisen  25021  ax5seglem9  25734  xrsmulgzz  29487  heiborlem8  33284  cdlemd4  35003  cdleme15a  35076  cdleme17b  35089  cdleme25a  35156  cdleme25c  35158  cdleme25dN  35159  cdleme26ee  35163  tendococl  35575  tendodi1  35587  tendodi2  35588  cdlemi  35623  tendocan  35627  cdlemk5a  35638  cdlemk5  35639  cdlemk10  35646  cdlemk5u  35664  cdlemkfid1N  35724  pellexlem6  36913  rpexpmord  37028  acongeq  37065  jm2.25  37081  stoweidlem42  39592  stoweidlem51  39601  ldepspr  41576
  Copyright terms: Public domain W3C validator