Theorem syl122anc 1404

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  divdiv32d  12018  divcan5d  12019  divcan7d  12021  divdiv1d  12024  divdiv2d  12025  seqcoll  14503  cau3lem  15408  eqsqrtd  15421  isercolllem2  15719  isercoll  15721  summolem2a  15768  divrcnv  15908  prodmolem2a  15990  prmind2  16745  divnumden  16809  pceulem  16907  pcqmul  16915  pcqdiv  16919  pcexp  16921  pcaddlem  16950  pcbc  16962  prmodvdslcmf  17109  latledi  18535  latjjdi  18549  latjjdir  18550  sylow1lem1  19670  sylow1lem5  19674  efgred2  19825  abladdsub4  19883  ablpnpcan  19891  ghmplusg  19918  frgpnabllem2  19946  isdomn4  20802  isabvd  20895  orngsqr  20949  ornglmulle  20950  orngrmulle  20951  orngmullt  20954  suborng  20959  lmodvs1  20991  lspsolvlem  21246  isprmidlc  21445  ssdifidlprm  21457  frgpcyg  21694  ip2di  21762  evlslem1  22204  mdetuni0  22749  cpmadugsumlemB  23002  elptr2  23702  blss2ps  24531  blss2  24532  blssps  24552  blss  24553  xmeter  24561  metdcnlem  24965  lebnumii  25096  minveclem2  25556  pjthlem1  25567  volfiniun  25677  dvfsumrlimge0  26160  lgsdi  27466  cofcut1d  28082  ax5seglem3  29224  ax5seglem6  29227  axcontlem8  29264  eengtrkg  29279  vacn  30989  minvecolem2  31170  minvecolem4  31175  disjabrex  32870  disjabrexf  32871  2ndresdju  32937  fnpreimac  32958  cmn4d  33295  gsummulsubdishift1  33331  slmdvs1  33483  slmd0vs  33487  rlocaddval  33532  domnprodn0  33541  q1pdir  33840  madjusmdetlem1  34164  cgrcomand  36418  cgrcomr  36424  cgrcomland  36426  cgrcomrand  36427  cgrtriv  36429  cgrid2  36430  ofscom  36434  cgrextend  36435  segconeq  36437  btwntriv2  36439  btwnexch3and  36448  btwnouttr2  36449  btwnouttr  36451  btwnexch  36452  btwnexchand  36453  btwndiff  36454  ifscgr  36471  cgrsub  36472  cgrxfr  36482  lineext  36503  endofsegid  36512  btwnconn1lem2  36515  btwnconn1lem3  36516  btwnconn1lem4  36517  btwnconn1lem5  36518  btwnconn1lem7  36520  btwnconn1lem8  36521  btwnconn1lem10  36523  btwnconn1lem11  36524  btwnconn1lem13  36526  btwnconn1lem14  36527  btwnconn3  36530  midofsegid  36531  segcon2  36532  brsegle2  36536  seglecgr12im  36537  seglecgr12  36538  seglerflx  36539  seglemin  36540  segletr  36541  btwnsegle  36544  colinbtwnle  36545  btwnoutside  36552  broutsideof3  36553  outsideoftr  36556  outsideofeq  36557  outsidele  36559  lineunray  36574  lineelsb2  36575  lfladdcl  39772  lshpkrlem4  39814  latmmdiN  39935  latmmdir  39936  hlatj4  40075  4atlem4b  40301  4atlem11  40310  4atlem12  40313  dalem2  40362  dalem-cly  40372  dalem10  40374  dalem23  40397  dalem38  40411  dalem44  40417  dalem55  40428  cdlema1N  40492  paddclN  40543  pmapjoin  40553  dalawlem3  40574  dalawlem5  40576  dalawlem7  40578  dalawlem8  40579  dalawlem11  40582  dalawlem12  40583  lhpexle3lem  40712  4atexlemc  40770  trlnidat  40874  arglem1N  40891  cdlemd9  40907  cdleme0moN  40926  cdleme11c  40962  cdleme11h  40967  cdleme11  40971  cdleme16c  40981  cdleme16f  40984  cdlemeda  40999  cdleme20l2  41022  cdlemefs32sn1aw  41115  cdleme43fsv1snlem  41121  cdleme41sn3a  41134  cdleme32fva  41138  cdleme32b  41143  cdleme32c  41144  cdleme32e  41146  cdleme40m  41168  cdleme40n  41169  cdleme42e  41180  cdleme48d  41236  cdlemf2  41263  cdlemf  41264  cdlemg2fv2  41301  cdlemg7fvbwN  41308  cdlemg7fvN  41325  cdlemg9a  41333  cdlemg9b  41334  cdlemg10a  41341  cdlemg12b  41345  cdlemg17b  41363  cdlemg31d  41401  cdlemg33b0  41402  cdlemg33a  41407  ltrnco  41420  ltrncom  41439  cdlemh  41518  cdlemk3  41534  cdlemk12  41551  cdlemk12u  41573  cdlemkfid1N  41622  cdlemk51  41654  cdlemk54  41659  cdlemk43N  41664  cdlemk35u  41665  cdlemk55u1  41666  cdlemk39u1  41668  cdlemk19u1  41670  dia2dimlem10  41774  dvhgrp  41808  dvh0g  41812  cdlemm10N  41819  diblsmopel  41872  cdlemn4  41899  cdlemn6  41903  cdlemn7  41904  dihordlem7  41915  dihord1  41919  dihord2pre  41926  dihvalcqat  41940  dihopelvalcpre  41949  dihord5apre  41963  dihord  41965  dih1  41987  dihglbcpreN  42001  dihjatc1  42012  dihmeetlem13N  42020  dihmeetALTN  42028  dihjatcclem1  42119  baerlem3lem1  42408  domnexpgn0cl  43220  pellfundex  43542  rmxypairf1o  43567  rmxycomplete  43573  rmxyneg  43576  rmxyadd  43577  rmxy1  43578  rmxy0  43579  jm2.22  43651  proot1mul  43850  deg1mhm  43856  stoweidlem7  46650  stoweidlem36  46679