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

Theorem syl221anc 1374
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 512 . 2 (𝜑 → (𝜃𝜏))
6 syl23anc.5 . 2 (𝜑𝜂)
7 syl221anc.6 . 2 (((𝜓𝜒) ∧ (𝜃𝜏) ∧ 𝜂) → 𝜁)
81, 2, 5, 6, 7syl211anc 1369 1 (𝜑𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1080
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  df-3an 1082
This theorem is referenced by:  syl222anc  1379  vtocldf  3498  f1oprswap  6526  dmdcand  11293  modmul12d  13143  modnegd  13144  modadd12d  13145  exprec  13320  rpexpmord  13382  splval2  13955  dvdsmodexp  15448  eulerthlem2  15948  fermltl  15950  odzdvds  15961  fnpr2o  16659  efgredleme  18596  efgredlemc  18598  blssps  22717  blss  22718  metequiv2  22803  met1stc  22814  met2ndci  22815  metdstri  23142  xlebnum  23252  caubl  23594  divcxp  24951  cxple2a  24963  cxplead  24985  cxplt2d  24990  cxple2d  24991  mulcxpd  24992  ang180  25073  wilthlem2  25328  lgsvalmod  25574  lgsmod  25581  lgsdir2lem4  25586  lgsdirprm  25589  lgsne0  25593  lgseisen  25637  ax5seglem9  26406  xrsmulgzz  30339  linds2eq  30587  conway  32873  etasslt  32883  heiborlem8  34628  cdlemd4  36868  cdleme15a  36941  cdleme17b  36954  cdleme25a  37020  cdleme25c  37022  cdleme25dN  37023  cdleme26ee  37027  tendococl  37439  tendodi1  37451  tendodi2  37452  cdlemi  37487  tendocan  37491  cdlemk5a  37502  cdlemk5  37503  cdlemk10  37510  cdlemk5u  37528  cdlemkfid1N  37588  pellexlem6  38916  acongeq  39065  jm2.25  39081  stoweidlem42  41869  stoweidlem51  41878  ldepspr  44008
  Copyright terms: Public domain W3C validator