Theorem syl221anc 1379

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

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	3, 4	jca 511	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl221anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 2, 5, 6, 7	syl211anc 1374	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  syl222anc  1384  vtocldf  3491  f1oprswap  6755  dmdcand  11763  modmul12d  13626  modnegd  13627  modadd12d  13628  exprec  13805  rpexpmord  13867  splval2  14451  dvdsmodexp  15952  eulerthlem2  16464  fermltl  16466  odzdvds  16477  fnpr2o  17249  efgredleme  19330  efgredlemc  19332  blssps  23558  blss  23559  metequiv2  23647  met1stc  23658  met2ndci  23659  metdstri  23995  xlebnum  24109  caubl  24453  divcxp  25823  cxple2a  25835  cxplead  25857  cxplt2d  25862  cxple2d  25863  mulcxpd  25864  ang180  25945  wilthlem2  26199  lgsvalmod  26445  lgsmod  26452  lgsdir2lem4  26457  lgsdirprm  26460  lgsne0  26464  lgseisen  26508  ax5seglem9  27286  fzm1ne1  31089  xrsmulgzz  31266  linds2eq  31554  conway  33972  heiborlem8  35955  cdlemd4  38194  cdleme15a  38267  cdleme17b  38280  cdleme25a  38346  cdleme25c  38348  cdleme25dN  38349  cdleme26ee  38353  tendococl  38765  tendodi1  38777  tendodi2  38778  cdlemi  38813  tendocan  38817  cdlemk5a  38828  cdlemk5  38829  cdlemk10  38836  cdlemk5u  38854  cdlemkfid1N  38914  pellexlem6  40636  acongeq  40785  jm2.25  40801  stoweidlem42  43537  stoweidlem51  43546  ldepspr  45766