Theorem syl122anc 1381

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  divdiv32d  11942  divcan5d  11943  divcan7d  11945  divdiv1d  11948  divdiv2d  11949  seqcoll  14387  cau3lem  15278  eqsqrtd  15291  isercolllem2  15589  isercoll  15591  summolem2a  15638  divrcnv  15775  prodmolem2a  15857  prmind2  16612  divnumden  16675  pceulem  16773  pcqmul  16781  pcqdiv  16785  pcexp  16787  pcaddlem  16816  pcbc  16828  prmodvdslcmf  16975  latledi  18400  latjjdi  18414  latjjdir  18415  sylow1lem1  19527  sylow1lem5  19531  efgred2  19682  abladdsub4  19740  ablpnpcan  19748  ghmplusg  19775  frgpnabllem2  19803  isdomn4  20649  isabvd  20745  orngsqr  20799  ornglmulle  20800  orngrmulle  20801  orngmullt  20804  suborng  20809  lmodvs1  20841  lspsolvlem  21097  frgpcyg  21528  ip2di  21596  evlslem1  22037  mdetuni0  22565  cpmadugsumlemB  22818  elptr2  23518  blss2ps  24347  blss2  24348  blssps  24368  blss  24369  xmeter  24377  metdcnlem  24781  lebnumii  24921  minveclem2  25382  pjthlem1  25393  volfiniun  25504  dvfsumrlimge0  25993  lgsdi  27301  cofcut1d  27917  ax5seglem3  29004  ax5seglem6  29007  axcontlem8  29044  eengtrkg  29059  vacn  30769  minvecolem2  30950  minvecolem4  30955  disjabrex  32657  disjabrexf  32658  2ndresdju  32727  fnpreimac  32749  cmn4d  33114  gsummulsubdishift1  33151  slmdvs1  33302  slmd0vs  33306  rlocaddval  33350  domnprodn0  33357  isprmidlc  33528  ssdifidlprm  33539  q1pdir  33684  madjusmdetlem1  33984  cgrcomand  36185  cgrcomr  36191  cgrcomland  36193  cgrcomrand  36194  cgrtriv  36196  cgrid2  36197  ofscom  36201  cgrextend  36202  segconeq  36204  btwntriv2  36206  btwnexch3and  36215  btwnouttr2  36216  btwnouttr  36218  btwnexch  36219  btwnexchand  36220  btwndiff  36221  ifscgr  36238  cgrsub  36239  cgrxfr  36249  lineext  36270  endofsegid  36279  btwnconn1lem2  36282  btwnconn1lem3  36283  btwnconn1lem4  36284  btwnconn1lem5  36285  btwnconn1lem7  36287  btwnconn1lem8  36288  btwnconn1lem10  36290  btwnconn1lem11  36291  btwnconn1lem13  36293  btwnconn1lem14  36294  btwnconn3  36297  midofsegid  36298  segcon2  36299  brsegle2  36303  seglecgr12im  36304  seglecgr12  36305  seglerflx  36306  seglemin  36307  segletr  36308  btwnsegle  36311  colinbtwnle  36312  btwnoutside  36319  broutsideof3  36320  outsideoftr  36323  outsideofeq  36324  outsidele  36326  lineunray  36341  lineelsb2  36342  lfladdcl  39327  lshpkrlem4  39369  latmmdiN  39490  latmmdir  39491  hlatj4  39630  4atlem4b  39856  4atlem11  39865  4atlem12  39868  dalem2  39917  dalem-cly  39927  dalem10  39929  dalem23  39952  dalem38  39966  dalem44  39972  dalem55  39983  cdlema1N  40047  paddclN  40098  pmapjoin  40108  dalawlem3  40129  dalawlem5  40131  dalawlem7  40133  dalawlem8  40134  dalawlem11  40137  dalawlem12  40138  lhpexle3lem  40267  4atexlemc  40325  trlnidat  40429  arglem1N  40446  cdlemd9  40462  cdleme0moN  40481  cdleme11c  40517  cdleme11h  40522  cdleme11  40526  cdleme16c  40536  cdleme16f  40539  cdlemeda  40554  cdleme20l2  40577  cdlemefs32sn1aw  40670  cdleme43fsv1snlem  40676  cdleme41sn3a  40689  cdleme32fva  40693  cdleme32b  40698  cdleme32c  40699  cdleme32e  40701  cdleme40m  40723  cdleme40n  40724  cdleme42e  40735  cdleme48d  40791  cdlemf2  40818  cdlemf  40819  cdlemg2fv2  40856  cdlemg7fvbwN  40863  cdlemg7fvN  40880  cdlemg9a  40888  cdlemg9b  40889  cdlemg10a  40896  cdlemg12b  40900  cdlemg17b  40918  cdlemg31d  40956  cdlemg33b0  40957  cdlemg33a  40962  ltrnco  40975  ltrncom  40994  cdlemh  41073  cdlemk3  41089  cdlemk12  41106  cdlemk12u  41128  cdlemkfid1N  41177  cdlemk51  41209  cdlemk54  41214  cdlemk43N  41219  cdlemk35u  41220  cdlemk55u1  41221  cdlemk39u1  41223  cdlemk19u1  41225  dia2dimlem10  41329  dvhgrp  41363  dvh0g  41367  cdlemm10N  41374  diblsmopel  41427  cdlemn4  41454  cdlemn6  41458  cdlemn7  41459  dihordlem7  41470  dihord1  41474  dihord2pre  41481  dihvalcqat  41495  dihopelvalcpre  41504  dihord5apre  41518  dihord  41520  dih1  41542  dihglbcpreN  41556  dihjatc1  41567  dihmeetlem13N  41575  dihmeetALTN  41583  dihjatcclem1  41674  baerlem3lem1  41963  domnexpgn0cl  42774  pellfundex  43124  rmxypairf1o  43149  rmxycomplete  43155  rmxyneg  43158  rmxyadd  43159  rmxy1  43160  rmxy0  43161  jm2.22  43233  proot1mul  43432  deg1mhm  43438  stoweidlem7  46247  stoweidlem36  46276