Theorem syl122anc 1379

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 511	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl122anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl121anc 1375	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:  divdiv32d  12095  divcan5d  12096  divcan7d  12098  divdiv1d  12101  divdiv2d  12102  seqcoll  14513  cau3lem  15403  eqsqrtd  15416  isercolllem2  15714  isercoll  15716  summolem2a  15763  divrcnv  15900  prodmolem2a  15982  prmind2  16732  divnumden  16795  pceulem  16892  pcqmul  16900  pcqdiv  16904  pcexp  16906  pcaddlem  16935  pcbc  16947  prmodvdslcmf  17094  latledi  18547  latjjdi  18561  latjjdir  18562  sylow1lem1  19640  sylow1lem5  19644  efgred2  19795  abladdsub4  19853  ablpnpcan  19861  ghmplusg  19888  frgpnabllem2  19916  isdomn4  20738  isabvd  20835  lmodvs1  20910  lspsolvlem  21167  frgpcyg  21615  ip2di  21682  evlslem1  22129  mdetuni0  22648  cpmadugsumlemB  22901  elptr2  23603  blss2ps  24434  blss2  24435  blssps  24455  blss  24456  xmeter  24464  metdcnlem  24877  lebnumii  25017  minveclem2  25479  pjthlem1  25490  volfiniun  25601  dvfsumrlimge0  26091  lgsdi  27396  cofcut1d  27973  ax5seglem3  28964  ax5seglem6  28967  axcontlem8  29004  eengtrkg  29019  vacn  30726  minvecolem2  30907  minvecolem4  30912  disjabrex  32604  disjabrexf  32605  2ndresdju  32667  fnpreimac  32689  cmn4d  33018  slmdvs1  33199  slmd0vs  33203  rlocaddval  33240  domnprodn0  33247  orngsqr  33299  ornglmulle  33300  orngrmulle  33301  orngmullt  33304  suborng  33310  isprmidlc  33440  ssdifidlprm  33451  q1pdir  33588  madjusmdetlem1  33773  cgrcomand  35955  cgrcomr  35961  cgrcomland  35963  cgrcomrand  35964  cgrtriv  35966  cgrid2  35967  ofscom  35971  cgrextend  35972  segconeq  35974  btwntriv2  35976  btwnexch3and  35985  btwnouttr2  35986  btwnouttr  35988  btwnexch  35989  btwnexchand  35990  btwndiff  35991  ifscgr  36008  cgrsub  36009  cgrxfr  36019  lineext  36040  endofsegid  36049  btwnconn1lem2  36052  btwnconn1lem3  36053  btwnconn1lem4  36054  btwnconn1lem5  36055  btwnconn1lem7  36057  btwnconn1lem8  36058  btwnconn1lem10  36060  btwnconn1lem11  36061  btwnconn1lem13  36063  btwnconn1lem14  36064  btwnconn3  36067  midofsegid  36068  segcon2  36069  brsegle2  36073  seglecgr12im  36074  seglecgr12  36075  seglerflx  36076  seglemin  36077  segletr  36078  btwnsegle  36081  colinbtwnle  36082  btwnoutside  36089  broutsideof3  36090  outsideoftr  36093  outsideofeq  36094  outsidele  36096  lineunray  36111  lineelsb2  36112  lfladdcl  39027  lshpkrlem4  39069  latmmdiN  39190  latmmdir  39191  hlatj4  39330  4atlem4b  39557  4atlem11  39566  4atlem12  39569  dalem2  39618  dalem-cly  39628  dalem10  39630  dalem23  39653  dalem38  39667  dalem44  39673  dalem55  39684  cdlema1N  39748  paddclN  39799  pmapjoin  39809  dalawlem3  39830  dalawlem5  39832  dalawlem7  39834  dalawlem8  39835  dalawlem11  39838  dalawlem12  39839  lhpexle3lem  39968  4atexlemc  40026  trlnidat  40130  arglem1N  40147  cdlemd9  40163  cdleme0moN  40182  cdleme11c  40218  cdleme11h  40223  cdleme11  40227  cdleme16c  40237  cdleme16f  40240  cdlemeda  40255  cdleme20l2  40278  cdlemefs32sn1aw  40371  cdleme43fsv1snlem  40377  cdleme41sn3a  40390  cdleme32fva  40394  cdleme32b  40399  cdleme32c  40400  cdleme32e  40402  cdleme40m  40424  cdleme40n  40425  cdleme42e  40436  cdleme48d  40492  cdlemf2  40519  cdlemf  40520  cdlemg2fv2  40557  cdlemg7fvbwN  40564  cdlemg7fvN  40581  cdlemg9a  40589  cdlemg9b  40590  cdlemg10a  40597  cdlemg12b  40601  cdlemg17b  40619  cdlemg31d  40657  cdlemg33b0  40658  cdlemg33a  40663  ltrnco  40676  ltrncom  40695  cdlemh  40774  cdlemk3  40790  cdlemk12  40807  cdlemk12u  40829  cdlemkfid1N  40878  cdlemk51  40910  cdlemk54  40915  cdlemk43N  40920  cdlemk35u  40921  cdlemk55u1  40922  cdlemk39u1  40924  cdlemk19u1  40926  dia2dimlem10  41030  dvhgrp  41064  dvh0g  41068  cdlemm10N  41075  diblsmopel  41128  cdlemn4  41155  cdlemn6  41159  cdlemn7  41160  dihordlem7  41171  dihord1  41175  dihord2pre  41182  dihvalcqat  41196  dihopelvalcpre  41205  dihord5apre  41219  dihord  41221  dih1  41243  dihglbcpreN  41257  dihjatc1  41268  dihmeetlem13N  41276  dihmeetALTN  41284  dihjatcclem1  41375  baerlem3lem1  41664  domnexpgn0cl  42478  pellfundex  42842  rmxypairf1o  42868  rmxycomplete  42874  rmxyneg  42877  rmxyadd  42878  rmxy1  42879  rmxy0  42880  jm2.22  42952  proot1mul  43155  deg1mhm  43161  stoweidlem7  45928  stoweidlem36  45957