Theorem syl122anc 1378

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 1374	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  12065  divcan5d  12066  divcan7d  12068  divdiv1d  12071  divdiv2d  12072  seqcoll  14499  cau3lem  15389  eqsqrtd  15402  isercolllem2  15698  isercoll  15700  summolem2a  15747  divrcnv  15884  prodmolem2a  15966  prmind2  16718  divnumden  16781  pceulem  16878  pcqmul  16886  pcqdiv  16890  pcexp  16892  pcaddlem  16921  pcbc  16933  prmodvdslcmf  17080  latledi  18534  latjjdi  18548  latjjdir  18549  sylow1lem1  19630  sylow1lem5  19634  efgred2  19785  abladdsub4  19843  ablpnpcan  19851  ghmplusg  19878  frgpnabllem2  19906  isdomn4  20732  isabvd  20829  lmodvs1  20904  lspsolvlem  21161  frgpcyg  21609  ip2di  21676  evlslem1  22123  mdetuni0  22642  cpmadugsumlemB  22895  elptr2  23597  blss2ps  24428  blss2  24429  blssps  24449  blss  24450  xmeter  24458  metdcnlem  24871  lebnumii  25011  minveclem2  25473  pjthlem1  25484  volfiniun  25595  dvfsumrlimge0  26085  lgsdi  27392  cofcut1d  27969  ax5seglem3  28960  ax5seglem6  28963  axcontlem8  29000  eengtrkg  29015  vacn  30722  minvecolem2  30903  minvecolem4  30908  disjabrex  32601  disjabrexf  32602  2ndresdju  32665  fnpreimac  32687  cmn4d  33019  slmdvs1  33208  slmd0vs  33212  rlocaddval  33254  domnprodn0  33261  orngsqr  33313  ornglmulle  33314  orngrmulle  33315  orngmullt  33318  suborng  33324  isprmidlc  33454  ssdifidlprm  33465  q1pdir  33602  madjusmdetlem1  33787  cgrcomand  35972  cgrcomr  35978  cgrcomland  35980  cgrcomrand  35981  cgrtriv  35983  cgrid2  35984  ofscom  35988  cgrextend  35989  segconeq  35991  btwntriv2  35993  btwnexch3and  36002  btwnouttr2  36003  btwnouttr  36005  btwnexch  36006  btwnexchand  36007  btwndiff  36008  ifscgr  36025  cgrsub  36026  cgrxfr  36036  lineext  36057  endofsegid  36066  btwnconn1lem2  36069  btwnconn1lem3  36070  btwnconn1lem4  36071  btwnconn1lem5  36072  btwnconn1lem7  36074  btwnconn1lem8  36075  btwnconn1lem10  36077  btwnconn1lem11  36078  btwnconn1lem13  36080  btwnconn1lem14  36081  btwnconn3  36084  midofsegid  36085  segcon2  36086  brsegle2  36090  seglecgr12im  36091  seglecgr12  36092  seglerflx  36093  seglemin  36094  segletr  36095  btwnsegle  36098  colinbtwnle  36099  btwnoutside  36106  broutsideof3  36107  outsideoftr  36110  outsideofeq  36111  outsidele  36113  lineunray  36128  lineelsb2  36129  lfladdcl  39052  lshpkrlem4  39094  latmmdiN  39215  latmmdir  39216  hlatj4  39355  4atlem4b  39582  4atlem11  39591  4atlem12  39594  dalem2  39643  dalem-cly  39653  dalem10  39655  dalem23  39678  dalem38  39692  dalem44  39698  dalem55  39709  cdlema1N  39773  paddclN  39824  pmapjoin  39834  dalawlem3  39855  dalawlem5  39857  dalawlem7  39859  dalawlem8  39860  dalawlem11  39863  dalawlem12  39864  lhpexle3lem  39993  4atexlemc  40051  trlnidat  40155  arglem1N  40172  cdlemd9  40188  cdleme0moN  40207  cdleme11c  40243  cdleme11h  40248  cdleme11  40252  cdleme16c  40262  cdleme16f  40265  cdlemeda  40280  cdleme20l2  40303  cdlemefs32sn1aw  40396  cdleme43fsv1snlem  40402  cdleme41sn3a  40415  cdleme32fva  40419  cdleme32b  40424  cdleme32c  40425  cdleme32e  40427  cdleme40m  40449  cdleme40n  40450  cdleme42e  40461  cdleme48d  40517  cdlemf2  40544  cdlemf  40545  cdlemg2fv2  40582  cdlemg7fvbwN  40589  cdlemg7fvN  40606  cdlemg9a  40614  cdlemg9b  40615  cdlemg10a  40622  cdlemg12b  40626  cdlemg17b  40644  cdlemg31d  40682  cdlemg33b0  40683  cdlemg33a  40688  ltrnco  40701  ltrncom  40720  cdlemh  40799  cdlemk3  40815  cdlemk12  40832  cdlemk12u  40854  cdlemkfid1N  40903  cdlemk51  40935  cdlemk54  40940  cdlemk43N  40945  cdlemk35u  40946  cdlemk55u1  40947  cdlemk39u1  40949  cdlemk19u1  40951  dia2dimlem10  41055  dvhgrp  41089  dvh0g  41093  cdlemm10N  41100  diblsmopel  41153  cdlemn4  41180  cdlemn6  41184  cdlemn7  41185  dihordlem7  41196  dihord1  41200  dihord2pre  41207  dihvalcqat  41221  dihopelvalcpre  41230  dihord5apre  41244  dihord  41246  dih1  41268  dihglbcpreN  41282  dihjatc1  41293  dihmeetlem13N  41301  dihmeetALTN  41309  dihjatcclem1  41400  baerlem3lem1  41689  domnexpgn0cl  42509  pellfundex  42873  rmxypairf1o  42899  rmxycomplete  42905  rmxyneg  42908  rmxyadd  42909  rmxy1  42910  rmxy0  42911  jm2.22  42983  proot1mul  43182  deg1mhm  43188  stoweidlem7  45962  stoweidlem36  45991