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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  divdiv32d  12017  divcan5d  12018  divcan7d  12020  divdiv1d  12023  divdiv2d  12024  seqcoll  14503  cau3lem  15408  eqsqrtd  15421  isercolllem2  15719  isercoll  15721  summolem2a  15768  divrcnv  15908  prodmolem2a  15990  prmind2  16744  divnumden  16808  pceulem  16906  pcqmul  16914  pcqdiv  16918  pcexp  16920  pcaddlem  16949  pcbc  16961  prmodvdslcmf  17108  latledi  18534  latjjdi  18548  latjjdir  18549  sylow1lem1  19669  sylow1lem5  19673  efgred2  19824  abladdsub4  19882  ablpnpcan  19890  ghmplusg  19917  frgpnabllem2  19945  isdomn4  20801  isabvd  20896  orngsqr  20950  ornglmulle  20951  orngrmulle  20952  orngmullt  20955  suborng  20960  lmodvs1  20992  lspsolvlem  21247  isprmidlc  21453  ssdifidlprm  21467  frgpcyg  21704  ip2di  21772  evlslem1  22214  mdetuni0  22759  cpmadugsumlemB  23012  elptr2  23712  blss2ps  24541  blss2  24542  blssps  24562  blss  24563  xmeter  24571  metdcnlem  24975  lebnumii  25106  minveclem2  25566  pjthlem1  25577  volfiniun  25687  dvfsumrlimge0  26170  lgsdi  27479  cofcut1d  28095  prlngeq  29188  ax5seglem3  29262  ax5seglem6  29265  axcontlem8  29302  eengtrkg  29317  vacn  31027  minvecolem2  31208  minvecolem4  31213  disjabrex  32908  disjabrexf  32909  2ndresdju  32975  fnpreimac  32996  cmn4d  33333  gsummulsubdishift1  33369  slmdvs1  33521  slmd0vs  33525  rlocaddval  33570  domnprodn0  33579  q1pdir  33874  madjusmdetlem1  34198  cgrcomand  36464  cgrcomr  36470  cgrcomland  36472  cgrcomrand  36473  cgrtriv  36475  cgrid2  36476  ofscom  36480  cgrextend  36481  segconeq  36483  btwntriv2  36485  btwnexch3and  36494  btwnouttr2  36495  btwnouttr  36497  btwnexch  36498  btwnexchand  36499  btwndiff  36500  ifscgr  36517  cgrsub  36518  cgrxfr  36528  lineext  36549  endofsegid  36558  btwnconn1lem2  36561  btwnconn1lem3  36562  btwnconn1lem4  36563  btwnconn1lem5  36564  btwnconn1lem7  36566  btwnconn1lem8  36567  btwnconn1lem10  36569  btwnconn1lem11  36570  btwnconn1lem13  36572  btwnconn1lem14  36573  btwnconn3  36576  midofsegid  36577  segcon2  36578  brsegle2  36582  seglecgr12im  36583  seglecgr12  36584  seglerflx  36585  seglemin  36586  segletr  36587  btwnsegle  36590  colinbtwnle  36591  btwnoutside  36598  broutsideof3  36599  outsideoftr  36602  outsideofeq  36603  outsidele  36605  lineunray  36620  lineelsb2  36621  lfladdcl  39826  lshpkrlem4  39868  latmmdiN  39989  latmmdir  39990  hlatj4  40129  4atlem4b  40355  4atlem11  40364  4atlem12  40367  dalem2  40416  dalem-cly  40426  dalem10  40428  dalem23  40451  dalem38  40465  dalem44  40471  dalem55  40482  cdlema1N  40546  paddclN  40597  pmapjoin  40607  dalawlem3  40628  dalawlem5  40630  dalawlem7  40632  dalawlem8  40633  dalawlem11  40636  dalawlem12  40637  lhpexle3lem  40766  4atexlemc  40824  trlnidat  40928  arglem1N  40945  cdlemd9  40961  cdleme0moN  40980  cdleme11c  41016  cdleme11h  41021  cdleme11  41025  cdleme16c  41035  cdleme16f  41038  cdlemeda  41053  cdleme20l2  41076  cdlemefs32sn1aw  41169  cdleme43fsv1snlem  41175  cdleme41sn3a  41188  cdleme32fva  41192  cdleme32b  41197  cdleme32c  41198  cdleme32e  41200  cdleme40m  41222  cdleme40n  41223  cdleme42e  41234  cdleme48d  41290  cdlemf2  41317  cdlemf  41318  cdlemg2fv2  41355  cdlemg7fvbwN  41362  cdlemg7fvN  41379  cdlemg9a  41387  cdlemg9b  41388  cdlemg10a  41395  cdlemg12b  41399  cdlemg17b  41417  cdlemg31d  41455  cdlemg33b0  41456  cdlemg33a  41461  ltrnco  41474  ltrncom  41493  cdlemh  41572  cdlemk3  41588  cdlemk12  41605  cdlemk12u  41627  cdlemkfid1N  41676  cdlemk51  41708  cdlemk54  41713  cdlemk43N  41718  cdlemk35u  41719  cdlemk55u1  41720  cdlemk39u1  41722  cdlemk19u1  41724  dia2dimlem10  41828  dvhgrp  41862  dvh0g  41866  cdlemm10N  41873  diblsmopel  41926  cdlemn4  41953  cdlemn6  41957  cdlemn7  41958  dihordlem7  41969  dihord1  41973  dihord2pre  41980  dihvalcqat  41994  dihopelvalcpre  42003  dihord5apre  42017  dihord  42019  dih1  42041  dihglbcpreN  42055  dihjatc1  42066  dihmeetlem13N  42074  dihmeetALTN  42082  dihjatcclem1  42173  baerlem3lem1  42462  domnexpgn0cl  43274  pellfundex  43596  rmxypairf1o  43621  rmxycomplete  43627  rmxyneg  43630  rmxyadd  43631  rmxy1  43632  rmxy0  43633  jm2.22  43705  proot1mul  43904  deg1mhm  43910  stoweidlem7  46704  stoweidlem36  46733