Theorem syl122anc 1387

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  divdiv32d  11954  divcan5d  11955  divcan7d  11957  divdiv1d  11960  divdiv2d  11961  seqcoll  14424  cau3lem  15315  eqsqrtd  15328  isercolllem2  15626  isercoll  15628  summolem2a  15675  divrcnv  15815  prodmolem2a  15897  prmind2  16652  divnumden  16716  pceulem  16814  pcqmul  16822  pcqdiv  16826  pcexp  16828  pcaddlem  16857  pcbc  16869  prmodvdslcmf  17016  latledi  18441  latjjdi  18455  latjjdir  18456  sylow1lem1  19571  sylow1lem5  19575  efgred2  19726  abladdsub4  19784  ablpnpcan  19792  ghmplusg  19819  frgpnabllem2  19847  isdomn4  20695  isabvd  20791  orngsqr  20845  ornglmulle  20846  orngrmulle  20847  orngmullt  20850  suborng  20855  lmodvs1  20887  lspsolvlem  21142  frgpcyg  21555  ip2di  21623  evlslem1  22065  mdetuni0  22611  cpmadugsumlemB  22864  elptr2  23564  blss2ps  24393  blss2  24394  blssps  24414  blss  24415  xmeter  24423  metdcnlem  24827  lebnumii  24958  minveclem2  25418  pjthlem1  25429  volfiniun  25539  dvfsumrlimge0  26022  lgsdi  27322  cofcut1d  27938  ax5seglem3  29025  ax5seglem6  29028  axcontlem8  29065  eengtrkg  29080  vacn  30790  minvecolem2  30971  minvecolem4  30976  disjabrex  32678  disjabrexf  32679  2ndresdju  32748  fnpreimac  32769  cmn4d  33118  gsummulsubdishift1  33156  slmdvs1  33308  slmd0vs  33312  rlocaddval  33356  domnprodn0  33363  isprmidlc  33537  ssdifidlprm  33548  q1pdir  33693  madjusmdetlem1  34018  cgrcomand  36226  cgrcomr  36232  cgrcomland  36234  cgrcomrand  36235  cgrtriv  36237  cgrid2  36238  ofscom  36242  cgrextend  36243  segconeq  36245  btwntriv2  36247  btwnexch3and  36256  btwnouttr2  36257  btwnouttr  36259  btwnexch  36260  btwnexchand  36261  btwndiff  36262  ifscgr  36279  cgrsub  36280  cgrxfr  36290  lineext  36311  endofsegid  36320  btwnconn1lem2  36323  btwnconn1lem3  36324  btwnconn1lem4  36325  btwnconn1lem5  36326  btwnconn1lem7  36328  btwnconn1lem8  36329  btwnconn1lem10  36331  btwnconn1lem11  36332  btwnconn1lem13  36334  btwnconn1lem14  36335  btwnconn3  36338  midofsegid  36339  segcon2  36340  brsegle2  36344  seglecgr12im  36345  seglecgr12  36346  seglerflx  36347  seglemin  36348  segletr  36349  btwnsegle  36352  colinbtwnle  36353  btwnoutside  36360  broutsideof3  36361  outsideoftr  36364  outsideofeq  36365  outsidele  36367  lineunray  36382  lineelsb2  36383  lfladdcl  39570  lshpkrlem4  39612  latmmdiN  39733  latmmdir  39734  hlatj4  39873  4atlem4b  40099  4atlem11  40108  4atlem12  40111  dalem2  40160  dalem-cly  40170  dalem10  40172  dalem23  40195  dalem38  40209  dalem44  40215  dalem55  40226  cdlema1N  40290  paddclN  40341  pmapjoin  40351  dalawlem3  40372  dalawlem5  40374  dalawlem7  40376  dalawlem8  40377  dalawlem11  40380  dalawlem12  40381  lhpexle3lem  40510  4atexlemc  40568  trlnidat  40672  arglem1N  40689  cdlemd9  40705  cdleme0moN  40724  cdleme11c  40760  cdleme11h  40765  cdleme11  40769  cdleme16c  40779  cdleme16f  40782  cdlemeda  40797  cdleme20l2  40820  cdlemefs32sn1aw  40913  cdleme43fsv1snlem  40919  cdleme41sn3a  40932  cdleme32fva  40936  cdleme32b  40941  cdleme32c  40942  cdleme32e  40944  cdleme40m  40966  cdleme40n  40967  cdleme42e  40978  cdleme48d  41034  cdlemf2  41061  cdlemf  41062  cdlemg2fv2  41099  cdlemg7fvbwN  41106  cdlemg7fvN  41123  cdlemg9a  41131  cdlemg9b  41132  cdlemg10a  41139  cdlemg12b  41143  cdlemg17b  41161  cdlemg31d  41199  cdlemg33b0  41200  cdlemg33a  41205  ltrnco  41218  ltrncom  41237  cdlemh  41316  cdlemk3  41332  cdlemk12  41349  cdlemk12u  41371  cdlemkfid1N  41420  cdlemk51  41452  cdlemk54  41457  cdlemk43N  41462  cdlemk35u  41463  cdlemk55u1  41464  cdlemk39u1  41466  cdlemk19u1  41468  dia2dimlem10  41572  dvhgrp  41606  dvh0g  41610  cdlemm10N  41617  diblsmopel  41670  cdlemn4  41697  cdlemn6  41701  cdlemn7  41702  dihordlem7  41713  dihord1  41717  dihord2pre  41724  dihvalcqat  41738  dihopelvalcpre  41747  dihord5apre  41761  dihord  41763  dih1  41785  dihglbcpreN  41799  dihjatc1  41810  dihmeetlem13N  41818  dihmeetALTN  41826  dihjatcclem1  41917  baerlem3lem1  42206  domnexpgn0cl  43016  pellfundex  43338  rmxypairf1o  43363  rmxycomplete  43369  rmxyneg  43372  rmxyadd  43373  rmxy1  43374  rmxy0  43375  jm2.22  43447  proot1mul  43646  deg1mhm  43652  stoweidlem7  46457  stoweidlem36  46486