Theorem syl121anc 1487

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl121anc.5	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl121anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl121anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	2, 3	jca 503	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl121anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	1, 4, 5, 6	syl3anc 1483	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  syl122anc  1491  fsnunf2  6686  tfisi  7297  fnsuppeq0  7567  axdc4lem  9571  div32d  11118  div13d  11119  expdivd  13264  swrdsbslen  13691  sumeven  15349  sumodd  15350  pcqmul  15794  pcid  15813  pcneg  15814  pc2dvds  15819  pcz  15821  pcaddlem  15828  pcadd  15829  pcmpt2  15833  pcbc  15840  qexpz  15841  expnprm  15842  sylow1lem1  18233  lspsneleq  19341  lspsneq  19348  lspfixed  19354  lspfixedOLD  19355  frlmsslss2  20344  chmatval  20867  chpmat1dlem  20873  chpdmatlem2  20877  ucncn  22322  ucnextcn  22341  ssblex  22466  prdsxmslem2  22567  ncvs1  23189  voliunlem1  23553  deg1mul3le  24112  deg1pw  24116  fta1blem  24164  bcmono  25238  dchrisum0flblem1  25433  dchrisum0flblem2  25434  pntibndlem1  25514  pntlemr  25527  finsumvtxdg2sstep  26695  clwlksfclwwlkOLD  27258  umgr3cyclex  27378  nv1  27880  resf1o  29854  omndmul3  30060  rngurd  30135  measun  30621  measvuni  30624  measunl  30626  nosupbnd1  32202  slerec  32265  btwnconn1lem14  32549  segcon2  32554  seglelin  32565  neibastop3  32699  upixp  33854  fdc  33870  eqlkr3  34899  lkrshp  34903  lfl1dim  34919  lfl1dim2N  34920  eqlkr4  34963  2llnneN  35207  3dim2  35266  4atlem3  35394  4atlem11  35407  4atlem12  35410  pexmidlem4N  35771  lhp2at0nle  35833  lhple  35840  ltrnideq  35973  cdlemd9  36004  cdleme0ex2N  36022  cdleme0moN  36023  cdleme11a  36058  cdleme30a  36176  cdlemefs32sn1aw  36212  cdleme43fsv1snlem  36218  cdlemefs31fv1  36222  cdlemefs45eN  36229  cdleme41sn3a  36231  cdleme35h  36254  cdleme36a  36258  cdleme40m  36265  cdleme40n  36266  cdleme41sn3aw  36272  cdleme42h  36280  cdleme42k  36282  cdleme42mN  36285  cdleme43cN  36289  cdleme17d3  36294  cdleme48fvg  36298  cdlemeg47rv2  36308  cdlemeg46c  36311  cdlemeg46sfg  36318  cdlemeg46rjgN  36320  cdlemeg46rgv  36326  cdlemeg46req  36327  cdlemeg46gfv  36328  cdlemeg46gfre  36330  cdlemeg49lebilem  36337  cdleme50trn2  36349  cdlemg2kq  36400  cdlemb3  36404  cdlemg4f  36413  cdlemg9a  36430  cdlemg9b  36431  cdlemg9  36432  cdlemg11aq  36436  cdlemg12a  36441  cdlemg12b  36442  cdlemg12c  36443  cdlemg12d  36444  cdlemg12f  36446  cdlemg12g  36447  cdlemg12  36448  cdlemg13a  36449  cdlemg16  36455  cdlemg17e  36463  cdlemg17f  36464  cdlemg17g  36465  cdlemg17ir  36468  cdlemg17  36475  cdlemg18b  36477  cdlemg18c  36478  cdlemg33e  36508  trlcoabs2N  36520  trlcocnvat  36522  trlcolem  36524  trlco  36525  cdlemg44  36531  cdlemg47  36534  ltrncom  36536  tendococl  36570  tendoplcl  36579  tendoplcom  36580  tendoplass  36581  tendodi1  36582  tendodi2  36583  tendo0pl  36589  tendoipl  36595  cdlemh1  36613  cdlemi2  36617  tendo0mul  36624  tendo0mulr  36625  cdlemk2  36630  cdlemk3  36631  cdlemk4  36632  cdlemk6  36635  cdlemk8  36636  cdlemk12  36648  cdlemkole  36651  cdlemk14  36652  cdlemk15  36653  cdlemk5u  36659  cdlemk6u  36660  cdlemk12u  36670  cdlemkfid1N  36719  cdlemk19x  36741  cdlemk48  36748  cdlemk53a  36753  cdlemk56  36769  cdleml2N  36775  cdleml3N  36776  cdleml6  36779  cdleml7  36780  dva1dim  36783  dia2dimlem4  36865  dvhlveclem  36906  doca2N  36924  djajN  36935  cdlemn2a  36994  cdlemn3  36995  dihordlem6  37011  dihord5apre  37060  dihglbcpreN  37098  dihmeetcN  37100  dihmeetbN  37101  dihmeetlem10N  37114  dihmeetlem12N  37116  dihmeetlem15N  37119  dihmeetALTN  37125  dih1dimatlem0  37126  dihjatcclem3  37218  dihjatcclem4  37219  mapdpglem22  37491  hdmap14lem1a  37664  eldioph2b  37845  jm2.19lem4  38077  jm2.19  38078  jm2.26a  38085  jm2.26  38087  hbtlem2  38212  fnchoice  39699  stoweidlem42  40755  stoweidlem59  40772  fourierdlem42  40862