Theorem syl122anc 1397

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 519	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl122anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl121anc 1393	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  divdiv32d  11989  divcan5d  11990  divcan7d  11992  divdiv1d  11995  divdiv2d  11996  seqcoll  14474  cau3lem  15365  eqsqrtd  15378  isercolllem2  15676  isercoll  15678  summolem2a  15725  divrcnv  15865  prodmolem2a  15947  prmind2  16702  divnumden  16766  pceulem  16864  pcqmul  16872  pcqdiv  16876  pcexp  16878  pcaddlem  16907  pcbc  16919  prmodvdslcmf  17066  latledi  18492  latjjdi  18506  latjjdir  18507  sylow1lem1  19621  sylow1lem5  19625  efgred2  19776  abladdsub4  19834  ablpnpcan  19842  ghmplusg  19869  frgpnabllem2  19897  isdomn4  20745  isabvd  20841  orngsqr  20895  ornglmulle  20896  orngrmulle  20897  orngmullt  20900  suborng  20905  lmodvs1  20937  lspsolvlem  21192  frgpcyg  21605  ip2di  21673  evlslem1  22115  mdetuni0  22661  cpmadugsumlemB  22914  elptr2  23614  blss2ps  24443  blss2  24444  blssps  24464  blss  24465  xmeter  24473  metdcnlem  24877  lebnumii  25008  minveclem2  25468  pjthlem1  25479  volfiniun  25589  dvfsumrlimge0  26072  lgsdi  27375  cofcut1d  27991  ax5seglem3  29078  ax5seglem6  29081  axcontlem8  29118  eengtrkg  29133  vacn  30843  minvecolem2  31024  minvecolem4  31029  disjabrex  32731  disjabrexf  32732  2ndresdju  32801  fnpreimac  32822  cmn4d  33171  gsummulsubdishift1  33209  slmdvs1  33361  slmd0vs  33365  rlocaddval  33411  domnprodn0  33420  isprmidlc  33594  ssdifidlprm  33606  q1pdir  33760  madjusmdetlem1  34085  cgrcomand  36305  cgrcomr  36311  cgrcomland  36313  cgrcomrand  36314  cgrtriv  36316  cgrid2  36317  ofscom  36321  cgrextend  36322  segconeq  36324  btwntriv2  36326  btwnexch3and  36335  btwnouttr2  36336  btwnouttr  36338  btwnexch  36339  btwnexchand  36340  btwndiff  36341  ifscgr  36358  cgrsub  36359  cgrxfr  36369  lineext  36390  endofsegid  36399  btwnconn1lem2  36402  btwnconn1lem3  36403  btwnconn1lem4  36404  btwnconn1lem5  36405  btwnconn1lem7  36407  btwnconn1lem8  36408  btwnconn1lem10  36410  btwnconn1lem11  36411  btwnconn1lem13  36413  btwnconn1lem14  36414  btwnconn3  36417  midofsegid  36418  segcon2  36419  brsegle2  36423  seglecgr12im  36424  seglecgr12  36425  seglerflx  36426  seglemin  36427  segletr  36428  btwnsegle  36431  colinbtwnle  36432  btwnoutside  36439  broutsideof3  36440  outsideoftr  36443  outsideofeq  36444  outsidele  36446  lineunray  36461  lineelsb2  36462  lfladdcl  39659  lshpkrlem4  39701  latmmdiN  39822  latmmdir  39823  hlatj4  39962  4atlem4b  40188  4atlem11  40197  4atlem12  40200  dalem2  40249  dalem-cly  40259  dalem10  40261  dalem23  40284  dalem38  40298  dalem44  40304  dalem55  40315  cdlema1N  40379  paddclN  40430  pmapjoin  40440  dalawlem3  40461  dalawlem5  40463  dalawlem7  40465  dalawlem8  40466  dalawlem11  40469  dalawlem12  40470  lhpexle3lem  40599  4atexlemc  40657  trlnidat  40761  arglem1N  40778  cdlemd9  40794  cdleme0moN  40813  cdleme11c  40849  cdleme11h  40854  cdleme11  40858  cdleme16c  40868  cdleme16f  40871  cdlemeda  40886  cdleme20l2  40909  cdlemefs32sn1aw  41002  cdleme43fsv1snlem  41008  cdleme41sn3a  41021  cdleme32fva  41025  cdleme32b  41030  cdleme32c  41031  cdleme32e  41033  cdleme40m  41055  cdleme40n  41056  cdleme42e  41067  cdleme48d  41123  cdlemf2  41150  cdlemf  41151  cdlemg2fv2  41188  cdlemg7fvbwN  41195  cdlemg7fvN  41212  cdlemg9a  41220  cdlemg9b  41221  cdlemg10a  41228  cdlemg12b  41232  cdlemg17b  41250  cdlemg31d  41288  cdlemg33b0  41289  cdlemg33a  41294  ltrnco  41307  ltrncom  41326  cdlemh  41405  cdlemk3  41421  cdlemk12  41438  cdlemk12u  41460  cdlemkfid1N  41509  cdlemk51  41541  cdlemk54  41546  cdlemk43N  41551  cdlemk35u  41552  cdlemk55u1  41553  cdlemk39u1  41555  cdlemk19u1  41557  dia2dimlem10  41661  dvhgrp  41695  dvh0g  41699  cdlemm10N  41706  diblsmopel  41759  cdlemn4  41786  cdlemn6  41790  cdlemn7  41791  dihordlem7  41802  dihord1  41806  dihord2pre  41813  dihvalcqat  41827  dihopelvalcpre  41836  dihord5apre  41850  dihord  41852  dih1  41874  dihglbcpreN  41888  dihjatc1  41899  dihmeetlem13N  41907  dihmeetALTN  41915  dihjatcclem1  42006  baerlem3lem1  42295  domnexpgn0cl  43105  pellfundex  43427  rmxypairf1o  43452  rmxycomplete  43458  rmxyneg  43461  rmxyadd  43462  rmxy1  43463  rmxy0  43464  jm2.22  43536  proot1mul  43735  deg1mhm  43741  stoweidlem7  46545  stoweidlem36  46574