Theorem syl122anc 1504

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  divdiv32d  11152  divcan5d  11153  divcan7d  11155  divdiv1d  11158  divdiv2d  11159  seqcoll  13537  cau3lem  14471  eqsqrtd  14484  isercolllem2  14773  isercoll  14775  summolem2a  14823  divrcnv  14958  prodmolem2a  15037  prmind2  15770  divnumden  15827  pceulem  15921  pcqmul  15929  pcqdiv  15933  pcexp  15935  pcaddlem  15963  pcbc  15975  prmodvdslcmf  16122  latledi  17442  latjjdi  17456  latjjdir  17457  sylow1lem1  18364  sylow1lem5  18368  efgred2  18519  abladdsub4  18572  ablpnpcan  18578  ghmplusg  18602  frgpnabllem2  18630  isabvd  19176  lmodvs1  19247  lspsolvlem  19502  evlslem1  19875  frgpcyg  20281  ip2di  20348  mdetuni0  20795  cpmadugsumlemB  21049  elptr2  21748  blss2ps  22578  blss2  22579  blssps  22599  blss  22600  xmeter  22608  metdcnlem  23009  lebnumii  23135  minveclem2  23594  pjthlem1  23605  volfiniun  23713  dvfsumrlimge0  24192  lgsdi  25472  ax5seglem3  26230  ax5seglem6  26233  axcontlem8  26270  eengtrkg  26285  vacn  28104  minvecolem2  28286  minvecolem4  28291  disjabrex  29942  disjabrexf  29943  slmdvs1  30318  slmd0vs  30322  orngsqr  30349  ornglmulle  30350  orngrmulle  30351  orngmullt  30354  suborng  30360  madjusmdetlem1  30438  cgrcomand  32637  cgrcomr  32643  cgrcomland  32645  cgrcomrand  32646  cgrtriv  32648  cgrid2  32649  ofscom  32653  cgrextend  32654  segconeq  32656  btwntriv2  32658  btwnexch3and  32667  btwnouttr2  32668  btwnouttr  32670  btwnexch  32671  btwnexchand  32672  btwndiff  32673  ifscgr  32690  cgrsub  32691  cgrxfr  32701  lineext  32722  endofsegid  32731  btwnconn1lem2  32734  btwnconn1lem3  32735  btwnconn1lem4  32736  btwnconn1lem5  32737  btwnconn1lem7  32739  btwnconn1lem8  32740  btwnconn1lem10  32742  btwnconn1lem11  32743  btwnconn1lem13  32745  btwnconn1lem14  32746  btwnconn3  32749  midofsegid  32750  segcon2  32751  brsegle2  32755  seglecgr12im  32756  seglecgr12  32757  seglerflx  32758  seglemin  32759  segletr  32760  btwnsegle  32763  colinbtwnle  32764  btwnoutside  32771  broutsideof3  32772  outsideoftr  32775  outsideofeq  32776  outsidele  32778  lineunray  32793  lineelsb2  32794  lfladdcl  35146  lshpkrlem4  35188  latmmdiN  35309  latmmdir  35310  hlatj4  35449  4atlem4b  35675  4atlem11  35684  4atlem12  35687  dalem2  35736  dalem-cly  35746  dalem10  35748  dalem23  35771  dalem38  35785  dalem44  35791  dalem55  35802  cdlema1N  35866  paddclN  35917  pmapjoin  35927  dalawlem3  35948  dalawlem5  35950  dalawlem7  35952  dalawlem8  35953  dalawlem11  35956  dalawlem12  35957  lhpexle3lem  36086  4atexlemc  36144  trlnidat  36248  arglem1N  36265  cdlemd9  36281  cdleme0moN  36300  cdleme11c  36336  cdleme11h  36341  cdleme11  36345  cdleme16c  36355  cdleme16f  36358  cdlemeda  36373  cdleme20l2  36396  cdlemefs32sn1aw  36489  cdleme43fsv1snlem  36495  cdleme41sn3a  36508  cdleme32fva  36512  cdleme32b  36517  cdleme32c  36518  cdleme32e  36520  cdleme40m  36542  cdleme40n  36543  cdleme42e  36554  cdleme48d  36610  cdlemf2  36637  cdlemf  36638  cdlemg2fv2  36675  cdlemg7fvbwN  36682  cdlemg7fvN  36699  cdlemg9a  36707  cdlemg9b  36708  cdlemg10a  36715  cdlemg12b  36719  cdlemg17b  36737  cdlemg31d  36775  cdlemg33b0  36776  cdlemg33a  36781  ltrnco  36794  ltrncom  36813  cdlemh  36892  cdlemk3  36908  cdlemk12  36925  cdlemk12u  36947  cdlemkfid1N  36996  cdlemk51  37028  cdlemk54  37033  cdlemk43N  37038  cdlemk35u  37039  cdlemk55u1  37040  cdlemk39u1  37042  cdlemk19u1  37044  dia2dimlem10  37148  dvhgrp  37182  dvh0g  37186  cdlemm10N  37193  diblsmopel  37246  cdlemn4  37273  cdlemn6  37277  cdlemn7  37278  dihordlem7  37289  dihord1  37293  dihord2pre  37300  dihvalcqat  37314  dihopelvalcpre  37323  dihord5apre  37337  dihord  37339  dih1  37361  dihglbcpreN  37375  dihjatc1  37386  dihmeetlem13N  37394  dihmeetALTN  37402  dihjatcclem1  37493  baerlem3lem1  37782  pellfundex  38294  rmxypairf1o  38319  rmxycomplete  38325  rmxyneg  38328  rmxyadd  38329  rmxy1  38330  rmxy0  38331  jm2.22  38405  proot1mul  38620  deg1mhm  38628  stoweidlem7  41018  stoweidlem36  41047