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  11943  divcan5d  11944  divcan7d  11946  divdiv1d  11949  divdiv2d  11950  seqcoll  14389  cau3lem  15280  eqsqrtd  15293  isercolllem2  15591  isercoll  15593  summolem2a  15640  divrcnv  15777  prodmolem2a  15859  prmind2  16614  divnumden  16677  pceulem  16775  pcqmul  16783  pcqdiv  16787  pcexp  16789  pcaddlem  16818  pcbc  16830  prmodvdslcmf  16977  latledi  18401  latjjdi  18415  latjjdir  18416  sylow1lem1  19495  sylow1lem5  19499  efgred2  19650  abladdsub4  19708  ablpnpcan  19716  ghmplusg  19743  frgpnabllem2  19771  isdomn4  20619  isabvd  20715  orngsqr  20769  ornglmulle  20770  orngrmulle  20771  orngmullt  20774  suborng  20779  lmodvs1  20811  lspsolvlem  21067  frgpcyg  21498  ip2di  21566  evlslem1  22005  mdetuni0  22524  cpmadugsumlemB  22777  elptr2  23477  blss2ps  24307  blss2  24308  blssps  24328  blss  24329  xmeter  24337  metdcnlem  24741  lebnumii  24881  minveclem2  25342  pjthlem1  25353  volfiniun  25464  dvfsumrlimge0  25953  lgsdi  27261  cofcut1d  27852  ax5seglem3  28894  ax5seglem6  28897  axcontlem8  28934  eengtrkg  28949  vacn  30656  minvecolem2  30837  minvecolem4  30842  disjabrex  32544  disjabrexf  32545  2ndresdju  32606  fnpreimac  32628  cmn4d  32999  slmdvs1  33172  slmd0vs  33176  rlocaddval  33218  domnprodn0  33225  isprmidlc  33394  ssdifidlprm  33405  q1pdir  33544  madjusmdetlem1  33793  cgrcomand  35964  cgrcomr  35970  cgrcomland  35972  cgrcomrand  35973  cgrtriv  35975  cgrid2  35976  ofscom  35980  cgrextend  35981  segconeq  35983  btwntriv2  35985  btwnexch3and  35994  btwnouttr2  35995  btwnouttr  35997  btwnexch  35998  btwnexchand  35999  btwndiff  36000  ifscgr  36017  cgrsub  36018  cgrxfr  36028  lineext  36049  endofsegid  36058  btwnconn1lem2  36061  btwnconn1lem3  36062  btwnconn1lem4  36063  btwnconn1lem5  36064  btwnconn1lem7  36066  btwnconn1lem8  36067  btwnconn1lem10  36069  btwnconn1lem11  36070  btwnconn1lem13  36072  btwnconn1lem14  36073  btwnconn3  36076  midofsegid  36077  segcon2  36078  brsegle2  36082  seglecgr12im  36083  seglecgr12  36084  seglerflx  36085  seglemin  36086  segletr  36087  btwnsegle  36090  colinbtwnle  36091  btwnoutside  36098  broutsideof3  36099  outsideoftr  36102  outsideofeq  36103  outsidele  36105  lineunray  36120  lineelsb2  36121  lfladdcl  39049  lshpkrlem4  39091  latmmdiN  39212  latmmdir  39213  hlatj4  39352  4atlem4b  39579  4atlem11  39588  4atlem12  39591  dalem2  39640  dalem-cly  39650  dalem10  39652  dalem23  39675  dalem38  39689  dalem44  39695  dalem55  39706  cdlema1N  39770  paddclN  39821  pmapjoin  39831  dalawlem3  39852  dalawlem5  39854  dalawlem7  39856  dalawlem8  39857  dalawlem11  39860  dalawlem12  39861  lhpexle3lem  39990  4atexlemc  40048  trlnidat  40152  arglem1N  40169  cdlemd9  40185  cdleme0moN  40204  cdleme11c  40240  cdleme11h  40245  cdleme11  40249  cdleme16c  40259  cdleme16f  40262  cdlemeda  40277  cdleme20l2  40300  cdlemefs32sn1aw  40393  cdleme43fsv1snlem  40399  cdleme41sn3a  40412  cdleme32fva  40416  cdleme32b  40421  cdleme32c  40422  cdleme32e  40424  cdleme40m  40446  cdleme40n  40447  cdleme42e  40458  cdleme48d  40514  cdlemf2  40541  cdlemf  40542  cdlemg2fv2  40579  cdlemg7fvbwN  40586  cdlemg7fvN  40603  cdlemg9a  40611  cdlemg9b  40612  cdlemg10a  40619  cdlemg12b  40623  cdlemg17b  40641  cdlemg31d  40679  cdlemg33b0  40680  cdlemg33a  40685  ltrnco  40698  ltrncom  40717  cdlemh  40796  cdlemk3  40812  cdlemk12  40829  cdlemk12u  40851  cdlemkfid1N  40900  cdlemk51  40932  cdlemk54  40937  cdlemk43N  40942  cdlemk35u  40943  cdlemk55u1  40944  cdlemk39u1  40946  cdlemk19u1  40948  dia2dimlem10  41052  dvhgrp  41086  dvh0g  41090  cdlemm10N  41097  diblsmopel  41150  cdlemn4  41177  cdlemn6  41181  cdlemn7  41182  dihordlem7  41193  dihord1  41197  dihord2pre  41204  dihvalcqat  41218  dihopelvalcpre  41227  dihord5apre  41241  dihord  41243  dih1  41265  dihglbcpreN  41279  dihjatc1  41290  dihmeetlem13N  41298  dihmeetALTN  41306  dihjatcclem1  41397  baerlem3lem1  41686  domnexpgn0cl  42496  pellfundex  42859  rmxypairf1o  42884  rmxycomplete  42890  rmxyneg  42893  rmxyadd  42894  rmxy1  42895  rmxy0  42896  jm2.22  42968  proot1mul  43167  deg1mhm  43173  stoweidlem7  45989  stoweidlem36  46018