Theorem syl122anc 1378

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  divdiv32d  11785  divcan5d  11786  divcan7d  11788  divdiv1d  11791  divdiv2d  11792  seqcoll  14187  cau3lem  15075  eqsqrtd  15088  isercolllem2  15386  isercoll  15388  summolem2a  15436  divrcnv  15573  prodmolem2a  15653  prmind2  16399  divnumden  16461  pceulem  16555  pcqmul  16563  pcqdiv  16567  pcexp  16569  pcaddlem  16598  pcbc  16610  prmodvdslcmf  16757  latledi  18204  latjjdi  18218  latjjdir  18219  sylow1lem1  19212  sylow1lem5  19216  efgred2  19368  abladdsub4  19424  ablpnpcan  19430  ghmplusg  19456  frgpnabllem2  19484  isabvd  20089  lmodvs1  20160  lspsolvlem  20413  frgpcyg  20790  ip2di  20855  evlslem1  21301  mdetuni0  21779  cpmadugsumlemB  22032  elptr2  22734  blss2ps  23565  blss2  23566  blssps  23586  blss  23587  xmeter  23595  metdcnlem  24008  lebnumii  24138  minveclem2  24599  pjthlem1  24610  volfiniun  24720  dvfsumrlimge0  25203  lgsdi  26491  ax5seglem3  27308  ax5seglem6  27311  axcontlem8  27348  eengtrkg  27363  vacn  29065  minvecolem2  29246  minvecolem4  29251  disjabrex  30930  disjabrexf  30931  2ndresdju  30995  fnpreimac  31017  slmdvs1  31482  slmd0vs  31486  orngsqr  31512  ornglmulle  31513  orngrmulle  31514  orngmullt  31517  suborng  31523  isprmidlc  31632  madjusmdetlem1  31786  cgrcomand  34302  cgrcomr  34308  cgrcomland  34310  cgrcomrand  34311  cgrtriv  34313  cgrid2  34314  ofscom  34318  cgrextend  34319  segconeq  34321  btwntriv2  34323  btwnexch3and  34332  btwnouttr2  34333  btwnouttr  34335  btwnexch  34336  btwnexchand  34337  btwndiff  34338  ifscgr  34355  cgrsub  34356  cgrxfr  34366  lineext  34387  endofsegid  34396  btwnconn1lem2  34399  btwnconn1lem3  34400  btwnconn1lem4  34401  btwnconn1lem5  34402  btwnconn1lem7  34404  btwnconn1lem8  34405  btwnconn1lem10  34407  btwnconn1lem11  34408  btwnconn1lem13  34410  btwnconn1lem14  34411  btwnconn3  34414  midofsegid  34415  segcon2  34416  brsegle2  34420  seglecgr12im  34421  seglecgr12  34422  seglerflx  34423  seglemin  34424  segletr  34425  btwnsegle  34428  colinbtwnle  34429  btwnoutside  34436  broutsideof3  34437  outsideoftr  34440  outsideofeq  34441  outsidele  34443  lineunray  34458  lineelsb2  34459  lfladdcl  37092  lshpkrlem4  37134  latmmdiN  37255  latmmdir  37256  hlatj4  37395  4atlem4b  37621  4atlem11  37630  4atlem12  37633  dalem2  37682  dalem-cly  37692  dalem10  37694  dalem23  37717  dalem38  37731  dalem44  37737  dalem55  37748  cdlema1N  37812  paddclN  37863  pmapjoin  37873  dalawlem3  37894  dalawlem5  37896  dalawlem7  37898  dalawlem8  37899  dalawlem11  37902  dalawlem12  37903  lhpexle3lem  38032  4atexlemc  38090  trlnidat  38194  arglem1N  38211  cdlemd9  38227  cdleme0moN  38246  cdleme11c  38282  cdleme11h  38287  cdleme11  38291  cdleme16c  38301  cdleme16f  38304  cdlemeda  38319  cdleme20l2  38342  cdlemefs32sn1aw  38435  cdleme43fsv1snlem  38441  cdleme41sn3a  38454  cdleme32fva  38458  cdleme32b  38463  cdleme32c  38464  cdleme32e  38466  cdleme40m  38488  cdleme40n  38489  cdleme42e  38500  cdleme48d  38556  cdlemf2  38583  cdlemf  38584  cdlemg2fv2  38621  cdlemg7fvbwN  38628  cdlemg7fvN  38645  cdlemg9a  38653  cdlemg9b  38654  cdlemg10a  38661  cdlemg12b  38665  cdlemg17b  38683  cdlemg31d  38721  cdlemg33b0  38722  cdlemg33a  38727  ltrnco  38740  ltrncom  38759  cdlemh  38838  cdlemk3  38854  cdlemk12  38871  cdlemk12u  38893  cdlemkfid1N  38942  cdlemk51  38974  cdlemk54  38979  cdlemk43N  38984  cdlemk35u  38985  cdlemk55u1  38986  cdlemk39u1  38988  cdlemk19u1  38990  dia2dimlem10  39094  dvhgrp  39128  dvh0g  39132  cdlemm10N  39139  diblsmopel  39192  cdlemn4  39219  cdlemn6  39223  cdlemn7  39224  dihordlem7  39235  dihord1  39239  dihord2pre  39246  dihvalcqat  39260  dihopelvalcpre  39269  dihord5apre  39283  dihord  39285  dih1  39307  dihglbcpreN  39321  dihjatc1  39332  dihmeetlem13N  39340  dihmeetALTN  39348  dihjatcclem1  39439  baerlem3lem1  39728  isdomn4  40179  pellfundex  40715  rmxypairf1o  40740  rmxycomplete  40746  rmxyneg  40749  rmxyadd  40750  rmxy1  40751  rmxy0  40752  jm2.22  40824  proot1mul  41031  deg1mhm  41039  stoweidlem7  43555  stoweidlem36  43584