Theorem syl221anc 1399

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 519	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl221anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)
8	1, 2, 5, 6, 7	syl211anc 1394	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  syl222anc  1404  vtocldf  3525  f1oprswap  6846  dmdcand  11989  modmul12d  13931  modnegd  13932  modadd12d  13933  exprec  14109  rpexpmord  14174  splval2  14763  dvdsmodexp  16284  eulerthlem2  16807  fermltl  16809  odzdvds  16821  fnpr2o  17577  efgredleme  19773  efgredlemc  19775  blssps  24471  blss  24472  metequiv2  24557  met1stc  24568  met2ndci  24569  metdstri  24899  xlebnum  25014  caubl  25357  divcxp  26739  cxple2a  26751  cxplead  26773  cxplt2d  26778  cxple2d  26779  mulcxpd  26780  ang180  26866  wilthlem2  27120  lgsvalmod  27367  lgsmod  27374  lgsdir2lem4  27379  lgsdirprm  27382  lgsne0  27386  lgseisen  27430  conway  27859  ax5seglem9  29094  fzm1ne1  32950  xrsmulgzz  33147  linds2eq  33527  heiborlem8  38277  cdlemd4  40785  cdleme15a  40858  cdleme17b  40871  cdleme25a  40937  cdleme25c  40939  cdleme25dN  40940  cdleme26ee  40944  tendococl  41356  tendodi1  41368  tendodi2  41369  cdlemi  41404  tendocan  41408  cdlemk5a  41419  cdlemk5  41420  cdlemk10  41427  cdlemk5u  41445  cdlemkfid1N  41505  pellexlem6  43371  acongeq  43520  jm2.25  43536  stoweidlem42  46576  stoweidlem51  46585  ldepspr  49055