Theorem syl122anc 1382

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 1378	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  11947  divcan5d  11948  divcan7d  11950  divdiv1d  11953  divdiv2d  11954  seqcoll  14417  cau3lem  15308  eqsqrtd  15321  isercolllem2  15619  isercoll  15621  summolem2a  15668  divrcnv  15808  prodmolem2a  15890  prmind2  16645  divnumden  16709  pceulem  16807  pcqmul  16815  pcqdiv  16819  pcexp  16821  pcaddlem  16850  pcbc  16862  prmodvdslcmf  17009  latledi  18434  latjjdi  18448  latjjdir  18449  sylow1lem1  19564  sylow1lem5  19568  efgred2  19719  abladdsub4  19777  ablpnpcan  19785  ghmplusg  19812  frgpnabllem2  19840  isdomn4  20684  isabvd  20780  orngsqr  20834  ornglmulle  20835  orngrmulle  20836  orngmullt  20839  suborng  20844  lmodvs1  20876  lspsolvlem  21132  frgpcyg  21563  ip2di  21631  evlslem1  22070  mdetuni0  22596  cpmadugsumlemB  22849  elptr2  23549  blss2ps  24378  blss2  24379  blssps  24399  blss  24400  xmeter  24408  metdcnlem  24812  lebnumii  24943  minveclem2  25403  pjthlem1  25414  volfiniun  25524  dvfsumrlimge0  26007  lgsdi  27311  cofcut1d  27927  ax5seglem3  29014  ax5seglem6  29017  axcontlem8  29054  eengtrkg  29069  vacn  30780  minvecolem2  30961  minvecolem4  30966  disjabrex  32667  disjabrexf  32668  2ndresdju  32737  fnpreimac  32758  cmn4d  33107  gsummulsubdishift1  33144  slmdvs1  33296  slmd0vs  33300  rlocaddval  33344  domnprodn0  33351  isprmidlc  33522  ssdifidlprm  33533  q1pdir  33678  madjusmdetlem1  33987  cgrcomand  36189  cgrcomr  36195  cgrcomland  36197  cgrcomrand  36198  cgrtriv  36200  cgrid2  36201  ofscom  36205  cgrextend  36206  segconeq  36208  btwntriv2  36210  btwnexch3and  36219  btwnouttr2  36220  btwnouttr  36222  btwnexch  36223  btwnexchand  36224  btwndiff  36225  ifscgr  36242  cgrsub  36243  cgrxfr  36253  lineext  36274  endofsegid  36283  btwnconn1lem2  36286  btwnconn1lem3  36287  btwnconn1lem4  36288  btwnconn1lem5  36289  btwnconn1lem7  36291  btwnconn1lem8  36292  btwnconn1lem10  36294  btwnconn1lem11  36295  btwnconn1lem13  36297  btwnconn1lem14  36298  btwnconn3  36301  midofsegid  36302  segcon2  36303  brsegle2  36307  seglecgr12im  36308  seglecgr12  36309  seglerflx  36310  seglemin  36311  segletr  36312  btwnsegle  36315  colinbtwnle  36316  btwnoutside  36323  broutsideof3  36324  outsideoftr  36327  outsideofeq  36328  outsidele  36330  lineunray  36345  lineelsb2  36346  lfladdcl  39531  lshpkrlem4  39573  latmmdiN  39694  latmmdir  39695  hlatj4  39834  4atlem4b  40060  4atlem11  40069  4atlem12  40072  dalem2  40121  dalem-cly  40131  dalem10  40133  dalem23  40156  dalem38  40170  dalem44  40176  dalem55  40187  cdlema1N  40251  paddclN  40302  pmapjoin  40312  dalawlem3  40333  dalawlem5  40335  dalawlem7  40337  dalawlem8  40338  dalawlem11  40341  dalawlem12  40342  lhpexle3lem  40471  4atexlemc  40529  trlnidat  40633  arglem1N  40650  cdlemd9  40666  cdleme0moN  40685  cdleme11c  40721  cdleme11h  40726  cdleme11  40730  cdleme16c  40740  cdleme16f  40743  cdlemeda  40758  cdleme20l2  40781  cdlemefs32sn1aw  40874  cdleme43fsv1snlem  40880  cdleme41sn3a  40893  cdleme32fva  40897  cdleme32b  40902  cdleme32c  40903  cdleme32e  40905  cdleme40m  40927  cdleme40n  40928  cdleme42e  40939  cdleme48d  40995  cdlemf2  41022  cdlemf  41023  cdlemg2fv2  41060  cdlemg7fvbwN  41067  cdlemg7fvN  41084  cdlemg9a  41092  cdlemg9b  41093  cdlemg10a  41100  cdlemg12b  41104  cdlemg17b  41122  cdlemg31d  41160  cdlemg33b0  41161  cdlemg33a  41166  ltrnco  41179  ltrncom  41198  cdlemh  41277  cdlemk3  41293  cdlemk12  41310  cdlemk12u  41332  cdlemkfid1N  41381  cdlemk51  41413  cdlemk54  41418  cdlemk43N  41423  cdlemk35u  41424  cdlemk55u1  41425  cdlemk39u1  41427  cdlemk19u1  41429  dia2dimlem10  41533  dvhgrp  41567  dvh0g  41571  cdlemm10N  41578  diblsmopel  41631  cdlemn4  41658  cdlemn6  41662  cdlemn7  41663  dihordlem7  41674  dihord1  41678  dihord2pre  41685  dihvalcqat  41699  dihopelvalcpre  41708  dihord5apre  41722  dihord  41724  dih1  41746  dihglbcpreN  41760  dihjatc1  41771  dihmeetlem13N  41779  dihmeetALTN  41787  dihjatcclem1  41878  baerlem3lem1  42167  domnexpgn0cl  42982  pellfundex  43332  rmxypairf1o  43357  rmxycomplete  43363  rmxyneg  43366  rmxyadd  43367  rmxy1  43368  rmxy0  43369  jm2.22  43441  proot1mul  43640  deg1mhm  43646  stoweidlem7  46453  stoweidlem36  46482