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

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl222anc  1388  vtocldf  3517  f1oprswap  6812  dmdcand  11947  modmul12d  13850  modnegd  13851  modadd12d  13852  exprec  14028  rpexpmord  14093  splval2  14681  dvdsmodexp  16189  eulerthlem2  16711  fermltl  16713  odzdvds  16725  fnpr2o  17479  efgredleme  19640  efgredlemc  19642  blssps  24328  blss  24329  metequiv2  24414  met1stc  24425  met2ndci  24426  metdstri  24756  xlebnum  24880  caubl  25224  divcxp  26612  cxple2a  26624  cxplead  26646  cxplt2d  26651  cxple2d  26652  mulcxpd  26653  ang180  26740  wilthlem2  26995  lgsvalmod  27243  lgsmod  27250  lgsdir2lem4  27255  lgsdirprm  27258  lgsne0  27262  lgseisen  27306  conway  27728  ax5seglem9  28900  fzm1ne1  32744  xrsmulgzz  32976  linds2eq  33328  heiborlem8  37797  cdlemd4  40180  cdleme15a  40253  cdleme17b  40266  cdleme25a  40332  cdleme25c  40334  cdleme25dN  40335  cdleme26ee  40339  tendococl  40751  tendodi1  40763  tendodi2  40764  cdlemi  40799  tendocan  40803  cdlemk5a  40814  cdlemk5  40815  cdlemk10  40822  cdlemk5u  40840  cdlemkfid1N  40900  pellexlem6  42807  acongeq  42956  jm2.25  42972  stoweidlem42  46024  stoweidlem51  46033  ldepspr  48459