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 1087

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 1089

This theorem is referenced by:  syl222anc  1388  vtocldf  3560  f1oprswap  6892  dmdcand  12072  modmul12d  13966  modnegd  13967  modadd12d  13968  exprec  14144  rpexpmord  14208  splval2  14795  dvdsmodexp  16298  eulerthlem2  16819  fermltl  16821  odzdvds  16833  fnpr2o  17602  efgredleme  19761  efgredlemc  19763  blssps  24434  blss  24435  metequiv2  24523  met1stc  24534  met2ndci  24535  metdstri  24873  xlebnum  24997  caubl  25342  divcxp  26729  cxple2a  26741  cxplead  26763  cxplt2d  26768  cxple2d  26769  mulcxpd  26770  ang180  26857  wilthlem2  27112  lgsvalmod  27360  lgsmod  27367  lgsdir2lem4  27372  lgsdirprm  27375  lgsne0  27379  lgseisen  27423  conway  27844  ax5seglem9  28952  fzm1ne1  32790  xrsmulgzz  33011  linds2eq  33409  heiborlem8  37825  cdlemd4  40203  cdleme15a  40276  cdleme17b  40289  cdleme25a  40355  cdleme25c  40357  cdleme25dN  40358  cdleme26ee  40362  tendococl  40774  tendodi1  40786  tendodi2  40787  cdlemi  40822  tendocan  40826  cdlemk5a  40837  cdlemk5  40838  cdlemk10  40845  cdlemk5u  40863  cdlemkfid1N  40923  pellexlem6  42845  acongeq  42995  jm2.25  43011  stoweidlem42  46057  stoweidlem51  46066  ldepspr  48390