Theorem syl221anc 1383

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

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

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 1091

This theorem is referenced by:  syl222anc  1388  vtocldf  3462  f1oprswap  6693  dmdcand  11620  modmul12d  13481  modnegd  13482  modadd12d  13483  exprec  13659  rpexpmord  13721  splval2  14305  dvdsmodexp  15804  eulerthlem2  16316  fermltl  16318  odzdvds  16329  fnpr2o  17034  efgredleme  19105  efgredlemc  19107  blssps  23294  blss  23295  metequiv2  23380  met1stc  23391  met2ndci  23392  metdstri  23720  xlebnum  23834  caubl  24177  divcxp  25547  cxple2a  25559  cxplead  25581  cxplt2d  25586  cxple2d  25587  mulcxpd  25588  ang180  25669  wilthlem2  25923  lgsvalmod  26169  lgsmod  26176  lgsdir2lem4  26181  lgsdirprm  26184  lgsne0  26188  lgseisen  26232  ax5seglem9  27000  fzm1ne1  30802  xrsmulgzz  30978  linds2eq  31261  conway  33687  heiborlem8  35670  cdlemd4  37909  cdleme15a  37982  cdleme17b  37995  cdleme25a  38061  cdleme25c  38063  cdleme25dN  38064  cdleme26ee  38068  tendococl  38480  tendodi1  38492  tendodi2  38493  cdlemi  38528  tendocan  38532  cdlemk5a  38543  cdlemk5  38544  cdlemk10  38551  cdlemk5u  38569  cdlemkfid1N  38629  pellexlem6  40311  acongeq  40460  jm2.25  40476  stoweidlem42  43212  stoweidlem51  43221  ldepspr  45441