Theorem syl122anc 1382

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 1378	1 ⊢ (𝜑 → 𝜁)

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

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 1089

This theorem is referenced by:  divdiv32d  11956  divcan5d  11957  divcan7d  11959  divdiv1d  11962  divdiv2d  11963  seqcoll  14426  cau3lem  15317  eqsqrtd  15330  isercolllem2  15628  isercoll  15630  summolem2a  15677  divrcnv  15817  prodmolem2a  15899  prmind2  16654  divnumden  16718  pceulem  16816  pcqmul  16824  pcqdiv  16828  pcexp  16830  pcaddlem  16859  pcbc  16871  prmodvdslcmf  17018  latledi  18443  latjjdi  18457  latjjdir  18458  sylow1lem1  19573  sylow1lem5  19577  efgred2  19728  abladdsub4  19786  ablpnpcan  19794  ghmplusg  19821  frgpnabllem2  19849  isdomn4  20693  isabvd  20789  orngsqr  20843  ornglmulle  20844  orngrmulle  20845  orngmullt  20848  suborng  20853  lmodvs1  20885  lspsolvlem  21140  frgpcyg  21553  ip2di  21621  evlslem1  22060  mdetuni0  22586  cpmadugsumlemB  22839  elptr2  23539  blss2ps  24368  blss2  24369  blssps  24389  blss  24390  xmeter  24398  metdcnlem  24802  lebnumii  24933  minveclem2  25393  pjthlem1  25404  volfiniun  25514  dvfsumrlimge0  25997  lgsdi  27297  cofcut1d  27913  ax5seglem3  29000  ax5seglem6  29003  axcontlem8  29040  eengtrkg  29055  vacn  30765  minvecolem2  30946  minvecolem4  30951  disjabrex  32652  disjabrexf  32653  2ndresdju  32722  fnpreimac  32743  cmn4d  33092  gsummulsubdishift1  33129  slmdvs1  33281  slmd0vs  33285  rlocaddval  33329  domnprodn0  33336  isprmidlc  33507  ssdifidlprm  33518  q1pdir  33663  madjusmdetlem1  33971  cgrcomand  36173  cgrcomr  36179  cgrcomland  36181  cgrcomrand  36182  cgrtriv  36184  cgrid2  36185  ofscom  36189  cgrextend  36190  segconeq  36192  btwntriv2  36194  btwnexch3and  36203  btwnouttr2  36204  btwnouttr  36206  btwnexch  36207  btwnexchand  36208  btwndiff  36209  ifscgr  36226  cgrsub  36227  cgrxfr  36237  lineext  36258  endofsegid  36267  btwnconn1lem2  36270  btwnconn1lem3  36271  btwnconn1lem4  36272  btwnconn1lem5  36273  btwnconn1lem7  36275  btwnconn1lem8  36276  btwnconn1lem10  36278  btwnconn1lem11  36279  btwnconn1lem13  36281  btwnconn1lem14  36282  btwnconn3  36285  midofsegid  36286  segcon2  36287  brsegle2  36291  seglecgr12im  36292  seglecgr12  36293  seglerflx  36294  seglemin  36295  segletr  36296  btwnsegle  36299  colinbtwnle  36300  btwnoutside  36307  broutsideof3  36308  outsideoftr  36311  outsideofeq  36312  outsidele  36314  lineunray  36329  lineelsb2  36330  lfladdcl  39517  lshpkrlem4  39559  latmmdiN  39680  latmmdir  39681  hlatj4  39820  4atlem4b  40046  4atlem11  40055  4atlem12  40058  dalem2  40107  dalem-cly  40117  dalem10  40119  dalem23  40142  dalem38  40156  dalem44  40162  dalem55  40173  cdlema1N  40237  paddclN  40288  pmapjoin  40298  dalawlem3  40319  dalawlem5  40321  dalawlem7  40323  dalawlem8  40324  dalawlem11  40327  dalawlem12  40328  lhpexle3lem  40457  4atexlemc  40515  trlnidat  40619  arglem1N  40636  cdlemd9  40652  cdleme0moN  40671  cdleme11c  40707  cdleme11h  40712  cdleme11  40716  cdleme16c  40726  cdleme16f  40729  cdlemeda  40744  cdleme20l2  40767  cdlemefs32sn1aw  40860  cdleme43fsv1snlem  40866  cdleme41sn3a  40879  cdleme32fva  40883  cdleme32b  40888  cdleme32c  40889  cdleme32e  40891  cdleme40m  40913  cdleme40n  40914  cdleme42e  40925  cdleme48d  40981  cdlemf2  41008  cdlemf  41009  cdlemg2fv2  41046  cdlemg7fvbwN  41053  cdlemg7fvN  41070  cdlemg9a  41078  cdlemg9b  41079  cdlemg10a  41086  cdlemg12b  41090  cdlemg17b  41108  cdlemg31d  41146  cdlemg33b0  41147  cdlemg33a  41152  ltrnco  41165  ltrncom  41184  cdlemh  41263  cdlemk3  41279  cdlemk12  41296  cdlemk12u  41318  cdlemkfid1N  41367  cdlemk51  41399  cdlemk54  41404  cdlemk43N  41409  cdlemk35u  41410  cdlemk55u1  41411  cdlemk39u1  41413  cdlemk19u1  41415  dia2dimlem10  41519  dvhgrp  41553  dvh0g  41557  cdlemm10N  41564  diblsmopel  41617  cdlemn4  41644  cdlemn6  41648  cdlemn7  41649  dihordlem7  41660  dihord1  41664  dihord2pre  41671  dihvalcqat  41685  dihopelvalcpre  41694  dihord5apre  41708  dihord  41710  dih1  41732  dihglbcpreN  41746  dihjatc1  41757  dihmeetlem13N  41765  dihmeetALTN  41773  dihjatcclem1  41864  baerlem3lem1  42153  domnexpgn0cl  42968  pellfundex  43314  rmxypairf1o  43339  rmxycomplete  43345  rmxyneg  43348  rmxyadd  43349  rmxy1  43350  rmxy0  43351  jm2.22  43423  proot1mul  43622  deg1mhm  43628  stoweidlem7  46435  stoweidlem36  46464