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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  divdiv32d  12017  divcan5d  12018  divcan7d  12020  divdiv1d  12023  divdiv2d  12024  seqcoll  14427  cau3lem  15303  eqsqrtd  15316  isercolllem2  15614  isercoll  15616  summolem2a  15663  divrcnv  15800  prodmolem2a  15880  prmind2  16624  divnumden  16686  pceulem  16780  pcqmul  16788  pcqdiv  16792  pcexp  16794  pcaddlem  16823  pcbc  16835  prmodvdslcmf  16982  latledi  18432  latjjdi  18446  latjjdir  18447  sylow1lem1  19468  sylow1lem5  19472  efgred2  19623  abladdsub4  19681  ablpnpcan  19689  ghmplusg  19716  frgpnabllem2  19744  isabvd  20432  lmodvs1  20505  lspsolvlem  20761  isdomn4  20924  frgpcyg  21135  ip2di  21200  evlslem1  21651  mdetuni0  22130  cpmadugsumlemB  22383  elptr2  23085  blss2ps  23916  blss2  23917  blssps  23937  blss  23938  xmeter  23946  metdcnlem  24359  lebnumii  24489  minveclem2  24950  pjthlem1  24961  volfiniun  25071  dvfsumrlimge0  25554  lgsdi  26844  cofcut1d  27417  ax5seglem3  28227  ax5seglem6  28230  axcontlem8  28267  eengtrkg  28282  vacn  29985  minvecolem2  30166  minvecolem4  30171  disjabrex  31851  disjabrexf  31852  2ndresdju  31912  fnpreimac  31934  slmdvs1  32406  slmd0vs  32410  orngsqr  32463  ornglmulle  32464  orngrmulle  32465  orngmullt  32468  suborng  32474  isprmidlc  32611  q1pdir  32719  madjusmdetlem1  32876  cgrcomand  35032  cgrcomr  35038  cgrcomland  35040  cgrcomrand  35041  cgrtriv  35043  cgrid2  35044  ofscom  35048  cgrextend  35049  segconeq  35051  btwntriv2  35053  btwnexch3and  35062  btwnouttr2  35063  btwnouttr  35065  btwnexch  35066  btwnexchand  35067  btwndiff  35068  ifscgr  35085  cgrsub  35086  cgrxfr  35096  lineext  35117  endofsegid  35126  btwnconn1lem2  35129  btwnconn1lem3  35130  btwnconn1lem4  35131  btwnconn1lem5  35132  btwnconn1lem7  35134  btwnconn1lem8  35135  btwnconn1lem10  35137  btwnconn1lem11  35138  btwnconn1lem13  35140  btwnconn1lem14  35141  btwnconn3  35144  midofsegid  35145  segcon2  35146  brsegle2  35150  seglecgr12im  35151  seglecgr12  35152  seglerflx  35153  seglemin  35154  segletr  35155  btwnsegle  35158  colinbtwnle  35159  btwnoutside  35166  broutsideof3  35167  outsideoftr  35170  outsideofeq  35171  outsidele  35173  lineunray  35188  lineelsb2  35189  lfladdcl  38027  lshpkrlem4  38069  latmmdiN  38190  latmmdir  38191  hlatj4  38330  4atlem4b  38557  4atlem11  38566  4atlem12  38569  dalem2  38618  dalem-cly  38628  dalem10  38630  dalem23  38653  dalem38  38667  dalem44  38673  dalem55  38684  cdlema1N  38748  paddclN  38799  pmapjoin  38809  dalawlem3  38830  dalawlem5  38832  dalawlem7  38834  dalawlem8  38835  dalawlem11  38838  dalawlem12  38839  lhpexle3lem  38968  4atexlemc  39026  trlnidat  39130  arglem1N  39147  cdlemd9  39163  cdleme0moN  39182  cdleme11c  39218  cdleme11h  39223  cdleme11  39227  cdleme16c  39237  cdleme16f  39240  cdlemeda  39255  cdleme20l2  39278  cdlemefs32sn1aw  39371  cdleme43fsv1snlem  39377  cdleme41sn3a  39390  cdleme32fva  39394  cdleme32b  39399  cdleme32c  39400  cdleme32e  39402  cdleme40m  39424  cdleme40n  39425  cdleme42e  39436  cdleme48d  39492  cdlemf2  39519  cdlemf  39520  cdlemg2fv2  39557  cdlemg7fvbwN  39564  cdlemg7fvN  39581  cdlemg9a  39589  cdlemg9b  39590  cdlemg10a  39597  cdlemg12b  39601  cdlemg17b  39619  cdlemg31d  39657  cdlemg33b0  39658  cdlemg33a  39663  ltrnco  39676  ltrncom  39695  cdlemh  39774  cdlemk3  39790  cdlemk12  39807  cdlemk12u  39829  cdlemkfid1N  39878  cdlemk51  39910  cdlemk54  39915  cdlemk43N  39920  cdlemk35u  39921  cdlemk55u1  39922  cdlemk39u1  39924  cdlemk19u1  39926  dia2dimlem10  40030  dvhgrp  40064  dvh0g  40068  cdlemm10N  40075  diblsmopel  40128  cdlemn4  40155  cdlemn6  40159  cdlemn7  40160  dihordlem7  40171  dihord1  40175  dihord2pre  40182  dihvalcqat  40196  dihopelvalcpre  40205  dihord5apre  40219  dihord  40221  dih1  40243  dihglbcpreN  40257  dihjatc1  40268  dihmeetlem13N  40276  dihmeetALTN  40284  dihjatcclem1  40375  baerlem3lem1  40664  pellfundex  41706  rmxypairf1o  41732  rmxycomplete  41738  rmxyneg  41741  rmxyadd  41742  rmxy1  41743  rmxy0  41744  jm2.22  41816  proot1mul  42023  deg1mhm  42031  stoweidlem7  44802  stoweidlem36  44831