Theorem syl121anc 1377

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 511	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl121anc.5	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	1, 4, 5, 6	syl3anc 1373	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:  syl122anc  1381  fsnunf2  7206  tfisi  7880  fnsuppeq0  8217  ttrclss  9760  ttrclselem2  9766  axdc4lem  10495  div32d  12066  div13d  12067  expdivd  14200  swrdsbslen  14702  sumeven  16424  sumodd  16425  pcqmul  16891  pcid  16911  pcneg  16912  pc2dvds  16917  pcz  16919  pcaddlem  16926  pcadd  16927  pcmpt2  16931  pcbc  16938  qexpz  16939  expnprm  16940  sylow1lem1  19616  ringurd  20182  lspsneleq  21117  lspsneq  21124  lspfixed  21130  frlmsslss2  21795  chmatval  22835  chpmat1dlem  22841  chpdmatlem2  22845  ucncn  24294  ucnextcn  24313  ssblex  24438  prdsxmslem2  24542  ncvs1  25191  voliunlem1  25585  deg1mul3le  26156  deg1pw  26160  fta1blem  26210  bcmono  27321  dchrisum0flblem1  27552  dchrisum0flblem2  27553  pntibndlem1  27633  pntlemr  27646  nosupbnd1  27759  noinfbnd1  27774  noetalem1  27786  slerec  27864  finsumvtxdg2sstep  29567  umgr3cyclex  30202  nv1  30694  resf1o  32741  omndmul3  33090  symgcntz  33105  cycpmco2lem6  33151  tocyccntz  33164  deg1vr  33614  rtelextdg2lem  33767  measun  34212  measvuni  34215  measunl  34217  btwnconn1lem14  36101  segcon2  36106  seglelin  36117  neibastop3  36363  upixp  37736  fdc  37752  eqlkr3  39102  lkrshp  39106  lfl1dim  39122  lfl1dim2N  39123  eqlkr4  39166  2llnneN  39411  3dim2  39470  4atlem3  39598  4atlem11  39611  4atlem12  39614  pexmidlem4N  39975  lhp2at0nle  40037  lhple  40044  ltrnideq  40177  cdlemd9  40208  cdleme0ex2N  40226  cdleme0moN  40227  cdleme11a  40262  cdleme30a  40380  cdlemefs32sn1aw  40416  cdleme43fsv1snlem  40422  cdlemefs31fv1  40426  cdlemefs45eN  40433  cdleme41sn3a  40435  cdleme35h  40458  cdleme36a  40462  cdleme40m  40469  cdleme40n  40470  cdleme41sn3aw  40476  cdleme42h  40484  cdleme42k  40486  cdleme42mN  40489  cdleme43cN  40493  cdleme17d3  40498  cdleme48fvg  40502  cdlemeg47rv2  40512  cdlemeg46c  40515  cdlemeg46sfg  40522  cdlemeg46rjgN  40524  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemeg46gfv  40532  cdlemeg46gfre  40534  cdlemeg49lebilem  40541  cdleme50trn2  40553  cdlemg2kq  40604  cdlemb3  40608  cdlemg4f  40617  cdlemg9a  40634  cdlemg9b  40635  cdlemg9  40636  cdlemg11aq  40640  cdlemg12a  40645  cdlemg12b  40646  cdlemg12c  40647  cdlemg12d  40648  cdlemg12f  40650  cdlemg12g  40651  cdlemg12  40652  cdlemg13a  40653  cdlemg16  40659  cdlemg17e  40667  cdlemg17f  40668  cdlemg17g  40669  cdlemg17ir  40672  cdlemg17  40679  cdlemg18b  40681  cdlemg18c  40682  cdlemg33e  40712  trlcoabs2N  40724  trlcocnvat  40726  trlcolem  40728  trlco  40729  cdlemg44  40735  cdlemg47  40738  ltrncom  40740  tendococl  40774  tendoplcl  40783  tendoplcom  40784  tendoplass  40785  tendodi1  40786  tendodi2  40787  tendo0pl  40793  tendoipl  40799  cdlemh1  40817  cdlemi2  40821  tendo0mul  40828  tendo0mulr  40829  cdlemk2  40834  cdlemk3  40835  cdlemk4  40836  cdlemk6  40839  cdlemk8  40840  cdlemk12  40852  cdlemkole  40855  cdlemk14  40856  cdlemk15  40857  cdlemk5u  40863  cdlemk6u  40864  cdlemk12u  40874  cdlemkfid1N  40923  cdlemk19x  40945  cdlemk48  40952  cdlemk53a  40957  cdlemk56  40973  cdleml2N  40979  cdleml3N  40980  cdleml6  40983  cdleml7  40984  dva1dim  40987  dia2dimlem4  41069  dvhlveclem  41110  doca2N  41128  djajN  41139  cdlemn2a  41198  cdlemn3  41199  dihordlem6  41215  dihord5apre  41264  dihglbcpreN  41302  dihmeetcN  41304  dihmeetbN  41305  dihmeetlem10N  41318  dihmeetlem12N  41320  dihmeetlem15N  41323  dihmeetALTN  41329  dih1dimatlem0  41330  dihjatcclem3  41422  dihjatcclem4  41423  mapdpglem22  41695  hdmap14lem1a  41868  eldioph2b  42774  jm2.19lem4  43004  jm2.19  43005  jm2.26a  43012  jm2.26  43014  hbtlem2  43136  fnchoice  45034  stoweidlem42  46057  stoweidlem59  46074  fourierdlem42  46164  zplusmodne  47345  minusmod5ne  47351