Theorem syl122anc 1406

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  divdiv32d  12099  divcan5d  12100  divcan7d  12102  divdiv1d  12105  divdiv2d  12106  seqcoll  14589  cau3lem  15502  eqsqrtd  15515  isercolllem2  15813  isercoll  15815  summolem2a  15861  divrcnv  16001  prodmolem2a  16081  prmind2  16840  divnumden  16904  pceulem  17003  pcqmul  17011  pcqdiv  17015  pcexp  17017  pcaddlem  17046  pcbc  17058  prmodvdslcmf  17205  latledi  18631  latjjdi  18645  latjjdir  18646  sylow1lem1  19792  sylow1lem5  19796  efgred2  19947  abladdsub4  20005  ablpnpcan  20013  ghmplusg  20040  frgpnabllem2  20068  isdomn4  20947  isabvd  21049  orngsqr  21103  ornglmulle  21104  orngrmulle  21105  orngmullt  21108  suborng  21113  lmodvs1  21145  lspsolvlem  21400  isprmidlc  21608  ssdifidlprm  21622  frgpcyg  21859  ip2di  21927  evlslem1  22371  mdetuni0  22916  cpmadugsumlemB  23172  elptr2  23873  blss2ps  24702  blss2  24703  blssps  24723  blss  24724  xmeter  24732  metdcnlem  25136  lebnumii  25267  minveclem2  25727  pjthlem1  25738  volfiniun  25848  dvfsumrlimge0  26330  lgsdi  27643  cofcut1d  28289  prlngeq  29417  ax5seglem3  29491  ax5seglem6  29494  axcontlem8  29531  eengtrkg  29546  vacn  31278  minvecolem2  31459  minvecolem4  31464  disjabrex  33158  disjabrexf  33159  2ndresdju  33225  fnpreimac  33246  cmn4d  33575  gsummulsubdishift1  33611  slmdvs1  33763  slmd0vs  33767  rlocaddval  33812  domnprodn0  33821  q1pdir  34117  madjusmdetlem1  34441  cgrcomand  36726  cgrcomr  36732  cgrcomland  36734  cgrcomrand  36735  cgrtriv  36737  cgrid2  36738  ofscom  36742  cgrextend  36743  segconeq  36745  btwntriv2  36747  btwnexch3and  36756  btwnouttr2  36757  btwnouttr  36759  btwnexch  36760  btwnexchand  36761  btwndiff  36762  ifscgr  36779  cgrsub  36780  cgrxfr  36790  lineext  36811  endofsegid  36820  btwnconn1lem2  36823  btwnconn1lem3  36824  btwnconn1lem4  36825  btwnconn1lem5  36826  btwnconn1lem7  36828  btwnconn1lem8  36829  btwnconn1lem10  36831  btwnconn1lem11  36832  btwnconn1lem13  36834  btwnconn1lem14  36835  btwnconn3  36838  midofsegid  36839  segcon2  36840  brsegle2  36844  seglecgr12im  36845  seglecgr12  36846  seglerflx  36847  seglemin  36848  segletr  36849  btwnsegle  36852  colinbtwnle  36853  btwnoutside  36860  broutsideof3  36861  outsideoftr  36864  outsideofeq  36865  outsidele  36867  lineunray  36882  lineelsb2  36883  lfladdcl  40096  lshpkrlem4  40138  latmmdiN  40259  latmmdir  40260  hlatj4  40399  4atlem4b  40625  4atlem11  40634  4atlem12  40637  dalem2  40686  dalem-cly  40696  dalem10  40698  dalem23  40721  dalem38  40735  dalem44  40741  dalem55  40752  cdlema1N  40816  paddclN  40867  pmapjoin  40877  dalawlem3  40898  dalawlem5  40900  dalawlem7  40902  dalawlem8  40903  dalawlem11  40906  dalawlem12  40907  lhpexle3lem  41036  4atexlemc  41094  trlnidat  41198  arglem1N  41215  cdlemd9  41231  cdleme0moN  41250  cdleme11c  41286  cdleme11h  41291  cdleme11  41295  cdleme16c  41305  cdleme16f  41308  cdlemeda  41323  cdleme20l2  41346  cdlemefs32sn1aw  41439  cdleme43fsv1snlem  41445  cdleme41sn3a  41458  cdleme32fva  41462  cdleme32b  41467  cdleme32c  41468  cdleme32e  41470  cdleme40m  41492  cdleme40n  41493  cdleme42e  41504  cdleme48d  41560  cdlemf2  41587  cdlemf  41588  cdlemg2fv2  41625  cdlemg7fvbwN  41632  cdlemg7fvN  41649  cdlemg9a  41657  cdlemg9b  41658  cdlemg10a  41665  cdlemg12b  41669  cdlemg17b  41687  cdlemg31d  41725  cdlemg33b0  41726  cdlemg33a  41731  ltrnco  41744  ltrncom  41763  cdlemh  41842  cdlemk3  41858  cdlemk12  41875  cdlemk12u  41897  cdlemkfid1N  41946  cdlemk51  41978  cdlemk54  41983  cdlemk43N  41988  cdlemk35u  41989  cdlemk55u1  41990  cdlemk39u1  41992  cdlemk19u1  41994  dia2dimlem10  42098  dvhgrp  42132  dvh0g  42136  cdlemm10N  42143  diblsmopel  42196  cdlemn4  42223  cdlemn6  42227  cdlemn7  42228  dihordlem7  42239  dihord1  42243  dihord2pre  42250  dihvalcqat  42264  dihopelvalcpre  42273  dihord5apre  42287  dihord  42289  dih1  42311  dihglbcpreN  42325  dihjatc1  42336  dihmeetlem13N  42344  dihmeetALTN  42352  dihjatcclem1  42443  baerlem3lem1  42732  domnexpgn0cl  43549  pellfundex  43846  rmxypairf1o  43871  rmxycomplete  43877  rmxyneg  43880  rmxyadd  43881  rmxy1  43882  rmxy0  43883  jm2.22  43955  proot1mul  44154  deg1mhm  44160  stoweidlem7  46961  stoweidlem36  46990