Theorem syl122anc 1406

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  divdiv32d  12121  divcan5d  12122  divcan7d  12124  divdiv1d  12127  divdiv2d  12128  seqcoll  14612  cau3lem  15527  eqsqrtd  15540  isercolllem2  15838  isercoll  15840  summolem2a  15886  divrcnv  16026  prodmolem2a  16106  prmind2  16865  divnumden  16929  pceulem  17028  pcqmul  17036  pcqdiv  17040  pcexp  17042  pcaddlem  17071  pcbc  17083  prmodvdslcmf  17230  latledi  18656  latjjdi  18670  latjjdir  18671  sylow1lem1  19817  sylow1lem5  19821  efgred2  19972  abladdsub4  20030  ablpnpcan  20038  ghmplusg  20065  frgpnabllem2  20093  isdomn4  20972  isabvd  21074  orngsqr  21128  ornglmulle  21129  orngrmulle  21130  orngmullt  21133  suborng  21138  lmodvs1  21170  lspsolvlem  21425  isprmidlc  21633  ssdifidlprm  21647  frgpcyg  21884  ip2di  21952  evlslem1  22396  mdetuni0  22941  cpmadugsumlemB  23197  elptr2  23898  blss2ps  24727  blss2  24728  blssps  24748  blss  24749  xmeter  24757  metdcnlem  25161  lebnumii  25292  minveclem2  25752  pjthlem1  25763  volfiniun  25873  dvfsumrlimge0  26355  lgsdi  27666  cofcut1d  28312  prlngeq  29440  ax5seglem3  29514  ax5seglem6  29517  axcontlem8  29554  eengtrkg  29569  vacn  31301  minvecolem2  31482  minvecolem4  31487  disjabrex  33223  disjabrexf  33224  2ndresdju  33290  fnpreimac  33311  cmn4d  33639  gsummulsubdishift1  33675  slmdvs1  33827  slmd0vs  33831  rlocaddval  33876  domnprodn0  33885  q1pdir  34181  madjusmdetlem1  34505  cgrcomand  36848  cgrcomr  36854  cgrcomland  36856  cgrcomrand  36857  cgrtriv  36859  cgrid2  36860  ofscom  36864  cgrextend  36865  segconeq  36867  btwntriv2  36869  btwnexch3and  36878  btwnouttr2  36879  btwnouttr  36881  btwnexch  36882  btwnexchand  36883  btwndiff  36884  ifscgr  36901  cgrsub  36902  cgrxfr  36912  lineext  36933  endofsegid  36942  btwnconn1lem2  36945  btwnconn1lem3  36946  btwnconn1lem4  36947  btwnconn1lem5  36948  btwnconn1lem7  36950  btwnconn1lem8  36951  btwnconn1lem10  36953  btwnconn1lem11  36954  btwnconn1lem13  36956  btwnconn1lem14  36957  btwnconn3  36960  midofsegid  36961  segcon2  36962  brsegle2  36966  seglecgr12im  36967  seglecgr12  36968  seglerflx  36969  seglemin  36970  segletr  36971  btwnsegle  36974  colinbtwnle  36975  btwnoutside  36982  broutsideof3  36983  outsideoftr  36986  outsideofeq  36987  outsidele  36989  lineunray  37004  lineelsb2  37005  lfladdcl  40221  lshpkrlem4  40263  latmmdiN  40384  latmmdir  40385  hlatj4  40524  4atlem4b  40750  4atlem11  40759  4atlem12  40762  dalem2  40811  dalem-cly  40821  dalem10  40823  dalem23  40846  dalem38  40860  dalem44  40866  dalem55  40877  cdlema1N  40941  paddclN  40992  pmapjoin  41002  dalawlem3  41023  dalawlem5  41025  dalawlem7  41027  dalawlem8  41028  dalawlem11  41031  dalawlem12  41032  lhpexle3lem  41161  4atexlemc  41219  trlnidat  41323  arglem1N  41340  cdlemd9  41356  cdleme0moN  41375  cdleme11c  41411  cdleme11h  41416  cdleme11  41420  cdleme16c  41430  cdleme16f  41433  cdlemeda  41448  cdleme20l2  41471  cdlemefs32sn1aw  41564  cdleme43fsv1snlem  41570  cdleme41sn3a  41583  cdleme32fva  41587  cdleme32b  41592  cdleme32c  41593  cdleme32e  41595  cdleme40m  41617  cdleme40n  41618  cdleme42e  41629  cdleme48d  41685  cdlemf2  41712  cdlemf  41713  cdlemg2fv2  41750  cdlemg7fvbwN  41757  cdlemg7fvN  41774  cdlemg9a  41782  cdlemg9b  41783  cdlemg10a  41790  cdlemg12b  41794  cdlemg17b  41812  cdlemg31d  41850  cdlemg33b0  41851  cdlemg33a  41856  ltrnco  41869  ltrncom  41888  cdlemh  41967  cdlemk3  41983  cdlemk12  42000  cdlemk12u  42022  cdlemkfid1N  42071  cdlemk51  42103  cdlemk54  42108  cdlemk43N  42113  cdlemk35u  42114  cdlemk55u1  42115  cdlemk39u1  42117  cdlemk19u1  42119  dia2dimlem10  42223  dvhgrp  42257  dvh0g  42261  cdlemm10N  42268  diblsmopel  42321  cdlemn4  42348  cdlemn6  42352  cdlemn7  42353  dihordlem7  42364  dihord1  42368  dihord2pre  42375  dihvalcqat  42389  dihopelvalcpre  42398  dihord5apre  42412  dihord  42414  dih1  42436  dihglbcpreN  42450  dihjatc1  42461  dihmeetlem13N  42469  dihmeetALTN  42477  dihjatcclem1  42568  baerlem3lem1  42857  domnexpgn0cl  43677  pellfundex  43986  rmxypairf1o  44011  rmxycomplete  44017  rmxyneg  44020  rmxyadd  44021  rmxy1  44022  rmxy0  44023  jm2.22  44095  proot1mul  44289  deg1mhm  44295  stoweidlem7  47110  stoweidlem36  47139