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

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

Proof of Theorem syl221anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
53, 4jca 515 . 2 (𝜑 → (𝜃𝜏))
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl221anc.6 . 2 (((𝜓𝜒) ∧ (𝜃𝜏) ∧ 𝜂) → 𝜁)
81, 2, 5, 6, 7syl211anc 1373 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:  syl222anc  1383  vtocldf  3506  f1oprswap  6637  dmdcand  11438  modmul12d  13292  modnegd  13293  modadd12d  13294  exprec  13470  rpexpmord  13532  splval2  14114  dvdsmodexp  15611  eulerthlem2  16113  fermltl  16115  odzdvds  16126  fnpr2o  16826  efgredleme  18865  efgredlemc  18867  blssps  23035  blss  23036  metequiv2  23121  met1stc  23132  met2ndci  23133  metdstri  23460  xlebnum  23574  caubl  23916  divcxp  25282  cxple2a  25294  cxplead  25316  cxplt2d  25321  cxple2d  25322  mulcxpd  25323  ang180  25404  wilthlem2  25658  lgsvalmod  25904  lgsmod  25911  lgsdir2lem4  25916  lgsdirprm  25919  lgsne0  25923  lgseisen  25967  ax5seglem9  26735  fzm1ne1  30542  xrsmulgzz  30716  linds2eq  30999  conway  33378  etasslt  33388  heiborlem8  35255  cdlemd4  37496  cdleme15a  37569  cdleme17b  37582  cdleme25a  37648  cdleme25c  37650  cdleme25dN  37651  cdleme26ee  37655  tendococl  38067  tendodi1  38079  tendodi2  38080  cdlemi  38115  tendocan  38119  cdlemk5a  38130  cdlemk5  38131  cdlemk10  38138  cdlemk5u  38156  cdlemkfid1N  38216  pellexlem6  39768  acongeq  39917  jm2.25  39933  stoweidlem42  42677  stoweidlem51  42686  ldepspr  44875
  Copyright terms: Public domain W3C validator