Theorem syl122anc 1380

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  divdiv32d  12015  divcan5d  12016  divcan7d  12018  divdiv1d  12021  divdiv2d  12022  seqcoll  14425  cau3lem  15301  eqsqrtd  15314  isercolllem2  15612  isercoll  15614  summolem2a  15661  divrcnv  15798  prodmolem2a  15878  prmind2  16622  divnumden  16684  pceulem  16778  pcqmul  16786  pcqdiv  16790  pcexp  16792  pcaddlem  16821  pcbc  16833  prmodvdslcmf  16980  latledi  18430  latjjdi  18444  latjjdir  18445  sylow1lem1  19466  sylow1lem5  19470  efgred2  19621  abladdsub4  19679  ablpnpcan  19687  ghmplusg  19714  frgpnabllem2  19742  isabvd  20428  lmodvs1  20500  lspsolvlem  20755  isdomn4  20918  frgpcyg  21129  ip2di  21194  evlslem1  21645  mdetuni0  22123  cpmadugsumlemB  22376  elptr2  23078  blss2ps  23909  blss2  23910  blssps  23930  blss  23931  xmeter  23939  metdcnlem  24352  lebnumii  24482  minveclem2  24943  pjthlem1  24954  volfiniun  25064  dvfsumrlimge0  25547  lgsdi  26837  cofcut1d  27408  ax5seglem3  28189  ax5seglem6  28192  axcontlem8  28229  eengtrkg  28244  vacn  29947  minvecolem2  30128  minvecolem4  30133  disjabrex  31813  disjabrexf  31814  2ndresdju  31874  fnpreimac  31896  slmdvs1  32365  slmd0vs  32369  orngsqr  32422  ornglmulle  32423  orngrmulle  32424  orngmullt  32427  suborng  32433  isprmidlc  32566  madjusmdetlem1  32807  cgrcomand  34963  cgrcomr  34969  cgrcomland  34971  cgrcomrand  34972  cgrtriv  34974  cgrid2  34975  ofscom  34979  cgrextend  34980  segconeq  34982  btwntriv2  34984  btwnexch3and  34993  btwnouttr2  34994  btwnouttr  34996  btwnexch  34997  btwnexchand  34998  btwndiff  34999  ifscgr  35016  cgrsub  35017  cgrxfr  35027  lineext  35048  endofsegid  35057  btwnconn1lem2  35060  btwnconn1lem3  35061  btwnconn1lem4  35062  btwnconn1lem5  35063  btwnconn1lem7  35065  btwnconn1lem8  35066  btwnconn1lem10  35068  btwnconn1lem11  35069  btwnconn1lem13  35071  btwnconn1lem14  35072  btwnconn3  35075  midofsegid  35076  segcon2  35077  brsegle2  35081  seglecgr12im  35082  seglecgr12  35083  seglerflx  35084  seglemin  35085  segletr  35086  btwnsegle  35089  colinbtwnle  35090  btwnoutside  35097  broutsideof3  35098  outsideoftr  35101  outsideofeq  35102  outsidele  35104  lineunray  35119  lineelsb2  35120  lfladdcl  37941  lshpkrlem4  37983  latmmdiN  38104  latmmdir  38105  hlatj4  38244  4atlem4b  38471  4atlem11  38480  4atlem12  38483  dalem2  38532  dalem-cly  38542  dalem10  38544  dalem23  38567  dalem38  38581  dalem44  38587  dalem55  38598  cdlema1N  38662  paddclN  38713  pmapjoin  38723  dalawlem3  38744  dalawlem5  38746  dalawlem7  38748  dalawlem8  38749  dalawlem11  38752  dalawlem12  38753  lhpexle3lem  38882  4atexlemc  38940  trlnidat  39044  arglem1N  39061  cdlemd9  39077  cdleme0moN  39096  cdleme11c  39132  cdleme11h  39137  cdleme11  39141  cdleme16c  39151  cdleme16f  39154  cdlemeda  39169  cdleme20l2  39192  cdlemefs32sn1aw  39285  cdleme43fsv1snlem  39291  cdleme41sn3a  39304  cdleme32fva  39308  cdleme32b  39313  cdleme32c  39314  cdleme32e  39316  cdleme40m  39338  cdleme40n  39339  cdleme42e  39350  cdleme48d  39406  cdlemf2  39433  cdlemf  39434  cdlemg2fv2  39471  cdlemg7fvbwN  39478  cdlemg7fvN  39495  cdlemg9a  39503  cdlemg9b  39504  cdlemg10a  39511  cdlemg12b  39515  cdlemg17b  39533  cdlemg31d  39571  cdlemg33b0  39572  cdlemg33a  39577  ltrnco  39590  ltrncom  39609  cdlemh  39688  cdlemk3  39704  cdlemk12  39721  cdlemk12u  39743  cdlemkfid1N  39792  cdlemk51  39824  cdlemk54  39829  cdlemk43N  39834  cdlemk35u  39835  cdlemk55u1  39836  cdlemk39u1  39838  cdlemk19u1  39840  dia2dimlem10  39944  dvhgrp  39978  dvh0g  39982  cdlemm10N  39989  diblsmopel  40042  cdlemn4  40069  cdlemn6  40073  cdlemn7  40074  dihordlem7  40085  dihord1  40089  dihord2pre  40096  dihvalcqat  40110  dihopelvalcpre  40119  dihord5apre  40133  dihord  40135  dih1  40157  dihglbcpreN  40171  dihjatc1  40182  dihmeetlem13N  40190  dihmeetALTN  40198  dihjatcclem1  40289  baerlem3lem1  40578  pellfundex  41624  rmxypairf1o  41650  rmxycomplete  41656  rmxyneg  41659  rmxyadd  41660  rmxy1  41661  rmxy0  41662  jm2.22  41734  proot1mul  41941  deg1mhm  41949  stoweidlem7  44723  stoweidlem36  44752