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  11990  divcan5d  11991  divcan7d  11993  divdiv1d  11996  divdiv2d  11997  seqcoll  14436  cau3lem  15328  eqsqrtd  15341  isercolllem2  15639  isercoll  15641  summolem2a  15688  divrcnv  15825  prodmolem2a  15907  prmind2  16662  divnumden  16725  pceulem  16823  pcqmul  16831  pcqdiv  16835  pcexp  16837  pcaddlem  16866  pcbc  16878  prmodvdslcmf  17025  latledi  18443  latjjdi  18457  latjjdir  18458  sylow1lem1  19535  sylow1lem5  19539  efgred2  19690  abladdsub4  19748  ablpnpcan  19756  ghmplusg  19783  frgpnabllem2  19811  isdomn4  20632  isabvd  20728  lmodvs1  20803  lspsolvlem  21059  frgpcyg  21490  ip2di  21557  evlslem1  21996  mdetuni0  22515  cpmadugsumlemB  22768  elptr2  23468  blss2ps  24298  blss2  24299  blssps  24319  blss  24320  xmeter  24328  metdcnlem  24732  lebnumii  24872  minveclem2  25333  pjthlem1  25344  volfiniun  25455  dvfsumrlimge0  25944  lgsdi  27252  cofcut1d  27836  ax5seglem3  28865  ax5seglem6  28868  axcontlem8  28905  eengtrkg  28920  vacn  30630  minvecolem2  30811  minvecolem4  30816  disjabrex  32518  disjabrexf  32519  2ndresdju  32580  fnpreimac  32602  cmn4d  32980  slmdvs1  33180  slmd0vs  33184  rlocaddval  33226  domnprodn0  33233  orngsqr  33289  ornglmulle  33290  orngrmulle  33291  orngmullt  33294  suborng  33300  isprmidlc  33425  ssdifidlprm  33436  q1pdir  33575  madjusmdetlem1  33824  cgrcomand  35986  cgrcomr  35992  cgrcomland  35994  cgrcomrand  35995  cgrtriv  35997  cgrid2  35998  ofscom  36002  cgrextend  36003  segconeq  36005  btwntriv2  36007  btwnexch3and  36016  btwnouttr2  36017  btwnouttr  36019  btwnexch  36020  btwnexchand  36021  btwndiff  36022  ifscgr  36039  cgrsub  36040  cgrxfr  36050  lineext  36071  endofsegid  36080  btwnconn1lem2  36083  btwnconn1lem3  36084  btwnconn1lem4  36085  btwnconn1lem5  36086  btwnconn1lem7  36088  btwnconn1lem8  36089  btwnconn1lem10  36091  btwnconn1lem11  36092  btwnconn1lem13  36094  btwnconn1lem14  36095  btwnconn3  36098  midofsegid  36099  segcon2  36100  brsegle2  36104  seglecgr12im  36105  seglecgr12  36106  seglerflx  36107  seglemin  36108  segletr  36109  btwnsegle  36112  colinbtwnle  36113  btwnoutside  36120  broutsideof3  36121  outsideoftr  36124  outsideofeq  36125  outsidele  36127  lineunray  36142  lineelsb2  36143  lfladdcl  39071  lshpkrlem4  39113  latmmdiN  39234  latmmdir  39235  hlatj4  39374  4atlem4b  39601  4atlem11  39610  4atlem12  39613  dalem2  39662  dalem-cly  39672  dalem10  39674  dalem23  39697  dalem38  39711  dalem44  39717  dalem55  39728  cdlema1N  39792  paddclN  39843  pmapjoin  39853  dalawlem3  39874  dalawlem5  39876  dalawlem7  39878  dalawlem8  39879  dalawlem11  39882  dalawlem12  39883  lhpexle3lem  40012  4atexlemc  40070  trlnidat  40174  arglem1N  40191  cdlemd9  40207  cdleme0moN  40226  cdleme11c  40262  cdleme11h  40267  cdleme11  40271  cdleme16c  40281  cdleme16f  40284  cdlemeda  40299  cdleme20l2  40322  cdlemefs32sn1aw  40415  cdleme43fsv1snlem  40421  cdleme41sn3a  40434  cdleme32fva  40438  cdleme32b  40443  cdleme32c  40444  cdleme32e  40446  cdleme40m  40468  cdleme40n  40469  cdleme42e  40480  cdleme48d  40536  cdlemf2  40563  cdlemf  40564  cdlemg2fv2  40601  cdlemg7fvbwN  40608  cdlemg7fvN  40625  cdlemg9a  40633  cdlemg9b  40634  cdlemg10a  40641  cdlemg12b  40645  cdlemg17b  40663  cdlemg31d  40701  cdlemg33b0  40702  cdlemg33a  40707  ltrnco  40720  ltrncom  40739  cdlemh  40818  cdlemk3  40834  cdlemk12  40851  cdlemk12u  40873  cdlemkfid1N  40922  cdlemk51  40954  cdlemk54  40959  cdlemk43N  40964  cdlemk35u  40965  cdlemk55u1  40966  cdlemk39u1  40968  cdlemk19u1  40970  dia2dimlem10  41074  dvhgrp  41108  dvh0g  41112  cdlemm10N  41119  diblsmopel  41172  cdlemn4  41199  cdlemn6  41203  cdlemn7  41204  dihordlem7  41215  dihord1  41219  dihord2pre  41226  dihvalcqat  41240  dihopelvalcpre  41249  dihord5apre  41263  dihord  41265  dih1  41287  dihglbcpreN  41301  dihjatc1  41312  dihmeetlem13N  41320  dihmeetALTN  41328  dihjatcclem1  41419  baerlem3lem1  41708  domnexpgn0cl  42518  pellfundex  42881  rmxypairf1o  42907  rmxycomplete  42913  rmxyneg  42916  rmxyadd  42917  rmxy1  42918  rmxy0  42919  jm2.22  42991  proot1mul  43190  deg1mhm  43196  stoweidlem7  46012  stoweidlem36  46041