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 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  divdiv32d  11929  divcan5d  11930  divcan7d  11932  divdiv1d  11935  divdiv2d  11936  seqcoll  14373  cau3lem  15264  eqsqrtd  15277  isercolllem2  15575  isercoll  15577  summolem2a  15624  divrcnv  15761  prodmolem2a  15843  prmind2  16598  divnumden  16661  pceulem  16759  pcqmul  16767  pcqdiv  16771  pcexp  16773  pcaddlem  16802  pcbc  16814  prmodvdslcmf  16961  latledi  18385  latjjdi  18399  latjjdir  18400  sylow1lem1  19512  sylow1lem5  19516  efgred2  19667  abladdsub4  19725  ablpnpcan  19733  ghmplusg  19760  frgpnabllem2  19788  isdomn4  20633  isabvd  20729  orngsqr  20783  ornglmulle  20784  orngrmulle  20785  orngmullt  20788  suborng  20793  lmodvs1  20825  lspsolvlem  21081  frgpcyg  21512  ip2di  21580  evlslem1  22018  mdetuni0  22537  cpmadugsumlemB  22790  elptr2  23490  blss2ps  24319  blss2  24320  blssps  24340  blss  24341  xmeter  24349  metdcnlem  24753  lebnumii  24893  minveclem2  25354  pjthlem1  25365  volfiniun  25476  dvfsumrlimge0  25965  lgsdi  27273  cofcut1d  27866  ax5seglem3  28911  ax5seglem6  28914  axcontlem8  28951  eengtrkg  28966  vacn  30676  minvecolem2  30857  minvecolem4  30862  disjabrex  32564  disjabrexf  32565  2ndresdju  32633  fnpreimac  32655  cmn4d  33020  slmdvs1  33196  slmd0vs  33200  rlocaddval  33242  domnprodn0  33249  isprmidlc  33419  ssdifidlprm  33430  q1pdir  33570  madjusmdetlem1  33861  cgrcomand  36056  cgrcomr  36062  cgrcomland  36064  cgrcomrand  36065  cgrtriv  36067  cgrid2  36068  ofscom  36072  cgrextend  36073  segconeq  36075  btwntriv2  36077  btwnexch3and  36086  btwnouttr2  36087  btwnouttr  36089  btwnexch  36090  btwnexchand  36091  btwndiff  36092  ifscgr  36109  cgrsub  36110  cgrxfr  36120  lineext  36141  endofsegid  36150  btwnconn1lem2  36153  btwnconn1lem3  36154  btwnconn1lem4  36155  btwnconn1lem5  36156  btwnconn1lem7  36158  btwnconn1lem8  36159  btwnconn1lem10  36161  btwnconn1lem11  36162  btwnconn1lem13  36164  btwnconn1lem14  36165  btwnconn3  36168  midofsegid  36169  segcon2  36170  brsegle2  36174  seglecgr12im  36175  seglecgr12  36176  seglerflx  36177  seglemin  36178  segletr  36179  btwnsegle  36182  colinbtwnle  36183  btwnoutside  36190  broutsideof3  36191  outsideoftr  36194  outsideofeq  36195  outsidele  36197  lineunray  36212  lineelsb2  36213  lfladdcl  39190  lshpkrlem4  39232  latmmdiN  39353  latmmdir  39354  hlatj4  39493  4atlem4b  39719  4atlem11  39728  4atlem12  39731  dalem2  39780  dalem-cly  39790  dalem10  39792  dalem23  39815  dalem38  39829  dalem44  39835  dalem55  39846  cdlema1N  39910  paddclN  39961  pmapjoin  39971  dalawlem3  39992  dalawlem5  39994  dalawlem7  39996  dalawlem8  39997  dalawlem11  40000  dalawlem12  40001  lhpexle3lem  40130  4atexlemc  40188  trlnidat  40292  arglem1N  40309  cdlemd9  40325  cdleme0moN  40344  cdleme11c  40380  cdleme11h  40385  cdleme11  40389  cdleme16c  40399  cdleme16f  40402  cdlemeda  40417  cdleme20l2  40440  cdlemefs32sn1aw  40533  cdleme43fsv1snlem  40539  cdleme41sn3a  40552  cdleme32fva  40556  cdleme32b  40561  cdleme32c  40562  cdleme32e  40564  cdleme40m  40586  cdleme40n  40587  cdleme42e  40598  cdleme48d  40654  cdlemf2  40681  cdlemf  40682  cdlemg2fv2  40719  cdlemg7fvbwN  40726  cdlemg7fvN  40743  cdlemg9a  40751  cdlemg9b  40752  cdlemg10a  40759  cdlemg12b  40763  cdlemg17b  40781  cdlemg31d  40819  cdlemg33b0  40820  cdlemg33a  40825  ltrnco  40838  ltrncom  40857  cdlemh  40936  cdlemk3  40952  cdlemk12  40969  cdlemk12u  40991  cdlemkfid1N  41040  cdlemk51  41072  cdlemk54  41077  cdlemk43N  41082  cdlemk35u  41083  cdlemk55u1  41084  cdlemk39u1  41086  cdlemk19u1  41088  dia2dimlem10  41192  dvhgrp  41226  dvh0g  41230  cdlemm10N  41237  diblsmopel  41290  cdlemn4  41317  cdlemn6  41321  cdlemn7  41322  dihordlem7  41333  dihord1  41337  dihord2pre  41344  dihvalcqat  41358  dihopelvalcpre  41367  dihord5apre  41381  dihord  41383  dih1  41405  dihglbcpreN  41419  dihjatc1  41430  dihmeetlem13N  41438  dihmeetALTN  41446  dihjatcclem1  41537  baerlem3lem1  41826  domnexpgn0cl  42641  pellfundex  43003  rmxypairf1o  43028  rmxycomplete  43034  rmxyneg  43037  rmxyadd  43038  rmxy1  43039  rmxy0  43040  jm2.22  43112  proot1mul  43311  deg1mhm  43317  stoweidlem7  46129  stoweidlem36  46158