Theorem syl122anc 1375

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  divdiv32d  11444  divcan5d  11445  divcan7d  11447  divdiv1d  11450  divdiv2d  11451  seqcoll  13825  cau3lem  14717  eqsqrtd  14730  isercolllem2  15025  isercoll  15027  summolem2a  15075  divrcnv  15210  prodmolem2a  15291  prmind2  16032  divnumden  16091  pceulem  16185  pcqmul  16193  pcqdiv  16197  pcexp  16199  pcaddlem  16227  pcbc  16239  prmodvdslcmf  16386  latledi  17702  latjjdi  17716  latjjdir  17717  sylow1lem1  18726  sylow1lem5  18730  efgred2  18882  abladdsub4  18937  ablpnpcan  18943  ghmplusg  18969  frgpnabllem2  18997  isabvd  19594  lmodvs1  19665  lspsolvlem  19917  evlslem1  20298  frgpcyg  20723  ip2di  20788  mdetuni0  21233  cpmadugsumlemB  21485  elptr2  22185  blss2ps  23016  blss2  23017  blssps  23037  blss  23038  xmeter  23046  metdcnlem  23447  lebnumii  23573  minveclem2  24032  pjthlem1  24043  volfiniun  24151  dvfsumrlimge0  24630  lgsdi  25913  ax5seglem3  26720  ax5seglem6  26723  axcontlem8  26760  eengtrkg  26775  vacn  28474  minvecolem2  28655  minvecolem4  28660  disjabrex  30335  disjabrexf  30336  fnpreimac  30419  slmdvs1  30852  slmd0vs  30856  orngsqr  30881  ornglmulle  30882  orngrmulle  30883  orngmullt  30886  suborng  30892  isprmidlc  30967  madjusmdetlem1  31096  cgrcomand  33456  cgrcomr  33462  cgrcomland  33464  cgrcomrand  33465  cgrtriv  33467  cgrid2  33468  ofscom  33472  cgrextend  33473  segconeq  33475  btwntriv2  33477  btwnexch3and  33486  btwnouttr2  33487  btwnouttr  33489  btwnexch  33490  btwnexchand  33491  btwndiff  33492  ifscgr  33509  cgrsub  33510  cgrxfr  33520  lineext  33541  endofsegid  33550  btwnconn1lem2  33553  btwnconn1lem3  33554  btwnconn1lem4  33555  btwnconn1lem5  33556  btwnconn1lem7  33558  btwnconn1lem8  33559  btwnconn1lem10  33561  btwnconn1lem11  33562  btwnconn1lem13  33564  btwnconn1lem14  33565  btwnconn3  33568  midofsegid  33569  segcon2  33570  brsegle2  33574  seglecgr12im  33575  seglecgr12  33576  seglerflx  33577  seglemin  33578  segletr  33579  btwnsegle  33582  colinbtwnle  33583  btwnoutside  33590  broutsideof3  33591  outsideoftr  33594  outsideofeq  33595  outsidele  33597  lineunray  33612  lineelsb2  33613  lfladdcl  36211  lshpkrlem4  36253  latmmdiN  36374  latmmdir  36375  hlatj4  36514  4atlem4b  36740  4atlem11  36749  4atlem12  36752  dalem2  36801  dalem-cly  36811  dalem10  36813  dalem23  36836  dalem38  36850  dalem44  36856  dalem55  36867  cdlema1N  36931  paddclN  36982  pmapjoin  36992  dalawlem3  37013  dalawlem5  37015  dalawlem7  37017  dalawlem8  37018  dalawlem11  37021  dalawlem12  37022  lhpexle3lem  37151  4atexlemc  37209  trlnidat  37313  arglem1N  37330  cdlemd9  37346  cdleme0moN  37365  cdleme11c  37401  cdleme11h  37406  cdleme11  37410  cdleme16c  37420  cdleme16f  37423  cdlemeda  37438  cdleme20l2  37461  cdlemefs32sn1aw  37554  cdleme43fsv1snlem  37560  cdleme41sn3a  37573  cdleme32fva  37577  cdleme32b  37582  cdleme32c  37583  cdleme32e  37585  cdleme40m  37607  cdleme40n  37608  cdleme42e  37619  cdleme48d  37675  cdlemf2  37702  cdlemf  37703  cdlemg2fv2  37740  cdlemg7fvbwN  37747  cdlemg7fvN  37764  cdlemg9a  37772  cdlemg9b  37773  cdlemg10a  37780  cdlemg12b  37784  cdlemg17b  37802  cdlemg31d  37840  cdlemg33b0  37841  cdlemg33a  37846  ltrnco  37859  ltrncom  37878  cdlemh  37957  cdlemk3  37973  cdlemk12  37990  cdlemk12u  38012  cdlemkfid1N  38061  cdlemk51  38093  cdlemk54  38098  cdlemk43N  38103  cdlemk35u  38104  cdlemk55u1  38105  cdlemk39u1  38107  cdlemk19u1  38109  dia2dimlem10  38213  dvhgrp  38247  dvh0g  38251  cdlemm10N  38258  diblsmopel  38311  cdlemn4  38338  cdlemn6  38342  cdlemn7  38343  dihordlem7  38354  dihord1  38358  dihord2pre  38365  dihvalcqat  38379  dihopelvalcpre  38388  dihord5apre  38402  dihord  38404  dih1  38426  dihglbcpreN  38440  dihjatc1  38451  dihmeetlem13N  38459  dihmeetALTN  38467  dihjatcclem1  38558  baerlem3lem1  38847  pellfundex  39489  rmxypairf1o  39514  rmxycomplete  39520  rmxyneg  39523  rmxyadd  39524  rmxy1  39525  rmxy0  39526  jm2.22  39598  proot1mul  39805  deg1mhm  39813  stoweidlem7  42299  stoweidlem36  42328