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  11919  divcan5d  11920  divcan7d  11922  divdiv1d  11925  divdiv2d  11926  seqcoll  14368  cau3lem  15259  eqsqrtd  15272  isercolllem2  15570  isercoll  15572  summolem2a  15619  divrcnv  15756  prodmolem2a  15838  prmind2  16593  divnumden  16656  pceulem  16754  pcqmul  16762  pcqdiv  16766  pcexp  16768  pcaddlem  16797  pcbc  16809  prmodvdslcmf  16956  latledi  18380  latjjdi  18394  latjjdir  18395  sylow1lem1  19508  sylow1lem5  19512  efgred2  19663  abladdsub4  19721  ablpnpcan  19729  ghmplusg  19756  frgpnabllem2  19784  isdomn4  20629  isabvd  20725  orngsqr  20779  ornglmulle  20780  orngrmulle  20781  orngmullt  20784  suborng  20789  lmodvs1  20821  lspsolvlem  21077  frgpcyg  21508  ip2di  21576  evlslem1  22015  mdetuni0  22534  cpmadugsumlemB  22787  elptr2  23487  blss2ps  24316  blss2  24317  blssps  24337  blss  24338  xmeter  24346  metdcnlem  24750  lebnumii  24890  minveclem2  25351  pjthlem1  25362  volfiniun  25473  dvfsumrlimge0  25962  lgsdi  27270  cofcut1d  27863  ax5seglem3  28907  ax5seglem6  28910  axcontlem8  28947  eengtrkg  28962  vacn  30669  minvecolem2  30850  minvecolem4  30855  disjabrex  32557  disjabrexf  32558  2ndresdju  32626  fnpreimac  32648  cmn4d  33008  slmdvs1  33184  slmd0vs  33188  rlocaddval  33230  domnprodn0  33237  isprmidlc  33407  ssdifidlprm  33418  q1pdir  33558  madjusmdetlem1  33835  cgrcomand  36024  cgrcomr  36030  cgrcomland  36032  cgrcomrand  36033  cgrtriv  36035  cgrid2  36036  ofscom  36040  cgrextend  36041  segconeq  36043  btwntriv2  36045  btwnexch3and  36054  btwnouttr2  36055  btwnouttr  36057  btwnexch  36058  btwnexchand  36059  btwndiff  36060  ifscgr  36077  cgrsub  36078  cgrxfr  36088  lineext  36109  endofsegid  36118  btwnconn1lem2  36121  btwnconn1lem3  36122  btwnconn1lem4  36123  btwnconn1lem5  36124  btwnconn1lem7  36126  btwnconn1lem8  36127  btwnconn1lem10  36129  btwnconn1lem11  36130  btwnconn1lem13  36132  btwnconn1lem14  36133  btwnconn3  36136  midofsegid  36137  segcon2  36138  brsegle2  36142  seglecgr12im  36143  seglecgr12  36144  seglerflx  36145  seglemin  36146  segletr  36147  btwnsegle  36150  colinbtwnle  36151  btwnoutside  36158  broutsideof3  36159  outsideoftr  36162  outsideofeq  36163  outsidele  36165  lineunray  36180  lineelsb2  36181  lfladdcl  39109  lshpkrlem4  39151  latmmdiN  39272  latmmdir  39273  hlatj4  39412  4atlem4b  39638  4atlem11  39647  4atlem12  39650  dalem2  39699  dalem-cly  39709  dalem10  39711  dalem23  39734  dalem38  39748  dalem44  39754  dalem55  39765  cdlema1N  39829  paddclN  39880  pmapjoin  39890  dalawlem3  39911  dalawlem5  39913  dalawlem7  39915  dalawlem8  39916  dalawlem11  39919  dalawlem12  39920  lhpexle3lem  40049  4atexlemc  40107  trlnidat  40211  arglem1N  40228  cdlemd9  40244  cdleme0moN  40263  cdleme11c  40299  cdleme11h  40304  cdleme11  40308  cdleme16c  40318  cdleme16f  40321  cdlemeda  40336  cdleme20l2  40359  cdlemefs32sn1aw  40452  cdleme43fsv1snlem  40458  cdleme41sn3a  40471  cdleme32fva  40475  cdleme32b  40480  cdleme32c  40481  cdleme32e  40483  cdleme40m  40505  cdleme40n  40506  cdleme42e  40517  cdleme48d  40573  cdlemf2  40600  cdlemf  40601  cdlemg2fv2  40638  cdlemg7fvbwN  40645  cdlemg7fvN  40662  cdlemg9a  40670  cdlemg9b  40671  cdlemg10a  40678  cdlemg12b  40682  cdlemg17b  40700  cdlemg31d  40738  cdlemg33b0  40739  cdlemg33a  40744  ltrnco  40757  ltrncom  40776  cdlemh  40855  cdlemk3  40871  cdlemk12  40888  cdlemk12u  40910  cdlemkfid1N  40959  cdlemk51  40991  cdlemk54  40996  cdlemk43N  41001  cdlemk35u  41002  cdlemk55u1  41003  cdlemk39u1  41005  cdlemk19u1  41007  dia2dimlem10  41111  dvhgrp  41145  dvh0g  41149  cdlemm10N  41156  diblsmopel  41209  cdlemn4  41236  cdlemn6  41240  cdlemn7  41241  dihordlem7  41252  dihord1  41256  dihord2pre  41263  dihvalcqat  41277  dihopelvalcpre  41286  dihord5apre  41300  dihord  41302  dih1  41324  dihglbcpreN  41338  dihjatc1  41349  dihmeetlem13N  41357  dihmeetALTN  41365  dihjatcclem1  41456  baerlem3lem1  41745  domnexpgn0cl  42555  pellfundex  42918  rmxypairf1o  42943  rmxycomplete  42949  rmxyneg  42952  rmxyadd  42953  rmxy1  42954  rmxy0  42955  jm2.22  43027  proot1mul  43226  deg1mhm  43232  stoweidlem7  46044  stoweidlem36  46073