Theorem syl122anc 1402

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

Hypotheses

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

Assertion

Ref	Expression
syl122anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl122anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	4, 5	jca 520	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl122anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl121anc 1398	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  divdiv32d  12007  divcan5d  12008  divcan7d  12010  divdiv1d  12013  divdiv2d  12014  seqcoll  14491  cau3lem  15396  eqsqrtd  15409  isercolllem2  15707  isercoll  15709  summolem2a  15756  divrcnv  15896  prodmolem2a  15978  prmind2  16733  divnumden  16797  pceulem  16895  pcqmul  16903  pcqdiv  16907  pcexp  16909  pcaddlem  16938  pcbc  16950  prmodvdslcmf  17097  latledi  18523  latjjdi  18537  latjjdir  18538  sylow1lem1  19659  sylow1lem5  19663  efgred2  19814  abladdsub4  19872  ablpnpcan  19880  ghmplusg  19907  frgpnabllem2  19935  isdomn4  20791  isabvd  20884  orngsqr  20938  ornglmulle  20939  orngrmulle  20940  orngmullt  20943  suborng  20948  lmodvs1  20980  lspsolvlem  21235  isprmidlc  21434  ssdifidlprm  21446  frgpcyg  21683  ip2di  21751  evlslem1  22193  mdetuni0  22739  cpmadugsumlemB  22992  elptr2  23692  blss2ps  24521  blss2  24522  blssps  24542  blss  24543  xmeter  24551  metdcnlem  24955  lebnumii  25086  minveclem2  25546  pjthlem1  25557  volfiniun  25667  dvfsumrlimge0  26150  lgsdi  27456  cofcut1d  28072  ax5seglem3  29190  ax5seglem6  29193  axcontlem8  29230  eengtrkg  29245  vacn  30955  minvecolem2  31136  minvecolem4  31141  disjabrex  32837  disjabrexf  32838  2ndresdju  32906  fnpreimac  32927  cmn4d  33265  gsummulsubdishift1  33301  slmdvs1  33453  slmd0vs  33457  rlocaddval  33502  domnprodn0  33511  q1pdir  33810  madjusmdetlem1  34134  cgrcomand  36354  cgrcomr  36360  cgrcomland  36362  cgrcomrand  36363  cgrtriv  36365  cgrid2  36366  ofscom  36370  cgrextend  36371  segconeq  36373  btwntriv2  36375  btwnexch3and  36384  btwnouttr2  36385  btwnouttr  36387  btwnexch  36388  btwnexchand  36389  btwndiff  36390  ifscgr  36407  cgrsub  36408  cgrxfr  36418  lineext  36439  endofsegid  36448  btwnconn1lem2  36451  btwnconn1lem3  36452  btwnconn1lem4  36453  btwnconn1lem5  36454  btwnconn1lem7  36456  btwnconn1lem8  36457  btwnconn1lem10  36459  btwnconn1lem11  36460  btwnconn1lem13  36462  btwnconn1lem14  36463  btwnconn3  36466  midofsegid  36467  segcon2  36468  brsegle2  36472  seglecgr12im  36473  seglecgr12  36474  seglerflx  36475  seglemin  36476  segletr  36477  btwnsegle  36480  colinbtwnle  36481  btwnoutside  36488  broutsideof3  36489  outsideoftr  36492  outsideofeq  36493  outsidele  36495  lineunray  36510  lineelsb2  36511  lfladdcl  39707  lshpkrlem4  39749  latmmdiN  39870  latmmdir  39871  hlatj4  40010  4atlem4b  40236  4atlem11  40245  4atlem12  40248  dalem2  40297  dalem-cly  40307  dalem10  40309  dalem23  40332  dalem38  40346  dalem44  40352  dalem55  40363  cdlema1N  40427  paddclN  40478  pmapjoin  40488  dalawlem3  40509  dalawlem5  40511  dalawlem7  40513  dalawlem8  40514  dalawlem11  40517  dalawlem12  40518  lhpexle3lem  40647  4atexlemc  40705  trlnidat  40809  arglem1N  40826  cdlemd9  40842  cdleme0moN  40861  cdleme11c  40897  cdleme11h  40902  cdleme11  40906  cdleme16c  40916  cdleme16f  40919  cdlemeda  40934  cdleme20l2  40957  cdlemefs32sn1aw  41050  cdleme43fsv1snlem  41056  cdleme41sn3a  41069  cdleme32fva  41073  cdleme32b  41078  cdleme32c  41079  cdleme32e  41081  cdleme40m  41103  cdleme40n  41104  cdleme42e  41115  cdleme48d  41171  cdlemf2  41198  cdlemf  41199  cdlemg2fv2  41236  cdlemg7fvbwN  41243  cdlemg7fvN  41260  cdlemg9a  41268  cdlemg9b  41269  cdlemg10a  41276  cdlemg12b  41280  cdlemg17b  41298  cdlemg31d  41336  cdlemg33b0  41337  cdlemg33a  41342  ltrnco  41355  ltrncom  41374  cdlemh  41453  cdlemk3  41469  cdlemk12  41486  cdlemk12u  41508  cdlemkfid1N  41557  cdlemk51  41589  cdlemk54  41594  cdlemk43N  41599  cdlemk35u  41600  cdlemk55u1  41601  cdlemk39u1  41603  cdlemk19u1  41605  dia2dimlem10  41709  dvhgrp  41743  dvh0g  41747  cdlemm10N  41754  diblsmopel  41807  cdlemn4  41834  cdlemn6  41838  cdlemn7  41839  dihordlem7  41850  dihord1  41854  dihord2pre  41861  dihvalcqat  41875  dihopelvalcpre  41884  dihord5apre  41898  dihord  41900  dih1  41922  dihglbcpreN  41936  dihjatc1  41947  dihmeetlem13N  41955  dihmeetALTN  41963  dihjatcclem1  42054  baerlem3lem1  42343  domnexpgn0cl  43153  pellfundex  43475  rmxypairf1o  43500  rmxycomplete  43506  rmxyneg  43509  rmxyadd  43510  rmxy1  43511  rmxy0  43512  jm2.22  43584  proot1mul  43783  deg1mhm  43789  stoweidlem7  46579  stoweidlem36  46608