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 1087

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 1089

This theorem is referenced by:  divdiv32d  12068  divcan5d  12069  divcan7d  12071  divdiv1d  12074  divdiv2d  12075  seqcoll  14503  cau3lem  15393  eqsqrtd  15406  isercolllem2  15702  isercoll  15704  summolem2a  15751  divrcnv  15888  prodmolem2a  15970  prmind2  16722  divnumden  16785  pceulem  16883  pcqmul  16891  pcqdiv  16895  pcexp  16897  pcaddlem  16926  pcbc  16938  prmodvdslcmf  17085  latledi  18522  latjjdi  18536  latjjdir  18537  sylow1lem1  19616  sylow1lem5  19620  efgred2  19771  abladdsub4  19829  ablpnpcan  19837  ghmplusg  19864  frgpnabllem2  19892  isdomn4  20716  isabvd  20813  lmodvs1  20888  lspsolvlem  21144  frgpcyg  21592  ip2di  21659  evlslem1  22106  mdetuni0  22627  cpmadugsumlemB  22880  elptr2  23582  blss2ps  24413  blss2  24414  blssps  24434  blss  24435  xmeter  24443  metdcnlem  24858  lebnumii  24998  minveclem2  25460  pjthlem1  25471  volfiniun  25582  dvfsumrlimge0  26071  lgsdi  27378  cofcut1d  27955  ax5seglem3  28946  ax5seglem6  28949  axcontlem8  28986  eengtrkg  29001  vacn  30713  minvecolem2  30894  minvecolem4  30899  disjabrex  32595  disjabrexf  32596  2ndresdju  32659  fnpreimac  32681  cmn4d  33037  slmdvs1  33226  slmd0vs  33230  rlocaddval  33272  domnprodn0  33279  orngsqr  33334  ornglmulle  33335  orngrmulle  33336  orngmullt  33339  suborng  33345  isprmidlc  33475  ssdifidlprm  33486  q1pdir  33623  madjusmdetlem1  33826  cgrcomand  35992  cgrcomr  35998  cgrcomland  36000  cgrcomrand  36001  cgrtriv  36003  cgrid2  36004  ofscom  36008  cgrextend  36009  segconeq  36011  btwntriv2  36013  btwnexch3and  36022  btwnouttr2  36023  btwnouttr  36025  btwnexch  36026  btwnexchand  36027  btwndiff  36028  ifscgr  36045  cgrsub  36046  cgrxfr  36056  lineext  36077  endofsegid  36086  btwnconn1lem2  36089  btwnconn1lem3  36090  btwnconn1lem4  36091  btwnconn1lem5  36092  btwnconn1lem7  36094  btwnconn1lem8  36095  btwnconn1lem10  36097  btwnconn1lem11  36098  btwnconn1lem13  36100  btwnconn1lem14  36101  btwnconn3  36104  midofsegid  36105  segcon2  36106  brsegle2  36110  seglecgr12im  36111  seglecgr12  36112  seglerflx  36113  seglemin  36114  segletr  36115  btwnsegle  36118  colinbtwnle  36119  btwnoutside  36126  broutsideof3  36127  outsideoftr  36130  outsideofeq  36131  outsidele  36133  lineunray  36148  lineelsb2  36149  lfladdcl  39072  lshpkrlem4  39114  latmmdiN  39235  latmmdir  39236  hlatj4  39375  4atlem4b  39602  4atlem11  39611  4atlem12  39614  dalem2  39663  dalem-cly  39673  dalem10  39675  dalem23  39698  dalem38  39712  dalem44  39718  dalem55  39729  cdlema1N  39793  paddclN  39844  pmapjoin  39854  dalawlem3  39875  dalawlem5  39877  dalawlem7  39879  dalawlem8  39880  dalawlem11  39883  dalawlem12  39884  lhpexle3lem  40013  4atexlemc  40071  trlnidat  40175  arglem1N  40192  cdlemd9  40208  cdleme0moN  40227  cdleme11c  40263  cdleme11h  40268  cdleme11  40272  cdleme16c  40282  cdleme16f  40285  cdlemeda  40300  cdleme20l2  40323  cdlemefs32sn1aw  40416  cdleme43fsv1snlem  40422  cdleme41sn3a  40435  cdleme32fva  40439  cdleme32b  40444  cdleme32c  40445  cdleme32e  40447  cdleme40m  40469  cdleme40n  40470  cdleme42e  40481  cdleme48d  40537  cdlemf2  40564  cdlemf  40565  cdlemg2fv2  40602  cdlemg7fvbwN  40609  cdlemg7fvN  40626  cdlemg9a  40634  cdlemg9b  40635  cdlemg10a  40642  cdlemg12b  40646  cdlemg17b  40664  cdlemg31d  40702  cdlemg33b0  40703  cdlemg33a  40708  ltrnco  40721  ltrncom  40740  cdlemh  40819  cdlemk3  40835  cdlemk12  40852  cdlemk12u  40874  cdlemkfid1N  40923  cdlemk51  40955  cdlemk54  40960  cdlemk43N  40965  cdlemk35u  40966  cdlemk55u1  40967  cdlemk39u1  40969  cdlemk19u1  40971  dia2dimlem10  41075  dvhgrp  41109  dvh0g  41113  cdlemm10N  41120  diblsmopel  41173  cdlemn4  41200  cdlemn6  41204  cdlemn7  41205  dihordlem7  41216  dihord1  41220  dihord2pre  41227  dihvalcqat  41241  dihopelvalcpre  41250  dihord5apre  41264  dihord  41266  dih1  41288  dihglbcpreN  41302  dihjatc1  41313  dihmeetlem13N  41321  dihmeetALTN  41329  dihjatcclem1  41420  baerlem3lem1  41709  domnexpgn0cl  42533  pellfundex  42897  rmxypairf1o  42923  rmxycomplete  42929  rmxyneg  42932  rmxyadd  42933  rmxy1  42934  rmxy0  42935  jm2.22  43007  proot1mul  43206  deg1mhm  43212  stoweidlem7  46022  stoweidlem36  46051