Theorem syl122anc 1327

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl122anc.6	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)

Assertion

Ref	Expression
syl122anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl122anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl22anc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	4, 5	jca 553	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl122anc.6	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)
8	1, 2, 3, 6, 7	syl121anc 1323	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  divdiv32d  10705  divcan5d  10706  divcan7d  10708  divdiv1d  10711  divdiv2d  10712  seqcoll  13105  cau3lem  13942  eqsqrtd  13955  isercolllem2  14244  isercoll  14246  summolem2a  14293  divrcnv  14423  prodmolem2a  14503  prmind2  15236  divnumden  15294  pceulem  15388  pcqmul  15396  pcqdiv  15400  pcexp  15402  pcaddlem  15430  pcbc  15442  prmodvdslcmf  15589  latledi  16912  latjjdi  16926  latjjdir  16927  sylow1lem1  17836  sylow1lem5  17840  efgred2  17989  abladdsub4  18042  ablpnpcan  18048  ghmplusg  18072  frgpnabllem2  18100  isabvd  18643  lmodvs1  18714  lspsolvlem  18963  evlslem1  19336  frgpcyg  19741  ip2di  19805  mdetuni0  20246  cpmadugsumlemB  20498  elptr2  21187  blss2ps  22018  blss2  22019  blssps  22039  blss  22040  xmeter  22048  metdcnlem  22447  lebnumii  22573  minveclem2  23005  pjthlem1  23016  volfiniun  23122  dvfsumrlimge0  23597  lgsdi  24859  ax5seglem3  25611  ax5seglem6  25614  axcontlem8  25651  eengtrkg  25665  vacn  26933  minvecolem2  27115  minvecolem4  27120  disjabrex  28777  disjabrexf  28778  slmdvs1  29104  slmd0vs  29108  orngsqr  29135  ornglmulle  29136  orngrmulle  29137  orngmullt  29140  suborng  29146  madjusmdetlem1  29221  cgrcomand  31268  cgrcomr  31274  cgrcomland  31276  cgrcomrand  31277  cgrtriv  31279  cgrid2  31280  ofscom  31284  cgrextend  31285  segconeq  31287  btwntriv2  31289  btwnexch3and  31298  btwnouttr2  31299  btwnouttr  31301  btwnexch  31302  btwnexchand  31303  btwndiff  31304  ifscgr  31321  cgrsub  31322  cgrxfr  31332  lineext  31353  endofsegid  31362  btwnconn1lem2  31365  btwnconn1lem3  31366  btwnconn1lem4  31367  btwnconn1lem5  31368  btwnconn1lem7  31370  btwnconn1lem8  31371  btwnconn1lem10  31373  btwnconn1lem11  31374  btwnconn1lem13  31376  btwnconn1lem14  31377  btwnconn3  31380  midofsegid  31381  segcon2  31382  brsegle2  31386  seglecgr12im  31387  seglecgr12  31388  seglerflx  31389  seglemin  31390  segletr  31391  btwnsegle  31394  colinbtwnle  31395  btwnoutside  31402  broutsideof3  31403  outsideoftr  31406  outsideofeq  31407  outsidele  31409  lineunray  31424  lineelsb2  31425  lfladdcl  33376  lshpkrlem4  33418  latmmdiN  33539  latmmdir  33540  hlatj4  33678  4atlem4b  33904  4atlem11  33913  4atlem12  33916  dalem2  33965  dalem-cly  33975  dalem10  33977  dalem23  34000  dalem38  34014  dalem44  34020  dalem55  34031  cdlema1N  34095  paddclN  34146  pmapjoin  34156  dalawlem3  34177  dalawlem5  34179  dalawlem7  34181  dalawlem8  34182  dalawlem11  34185  dalawlem12  34186  lhpexle3lem  34315  4atexlemc  34373  trlnidat  34478  arglem1N  34495  cdlemd9  34511  cdleme0moN  34530  cdleme11c  34566  cdleme11h  34571  cdleme11  34575  cdleme16c  34585  cdleme16f  34588  cdlemeda  34603  cdleme20l2  34627  cdlemefs32sn1aw  34720  cdleme43fsv1snlem  34726  cdleme41sn3a  34739  cdleme32fva  34743  cdleme32b  34748  cdleme32c  34749  cdleme32e  34751  cdleme40m  34773  cdleme40n  34774  cdleme42e  34785  cdleme48d  34841  cdlemf2  34868  cdlemf  34869  cdlemg2fv2  34906  cdlemg7fvbwN  34913  cdlemg7fvN  34930  cdlemg9a  34938  cdlemg9b  34939  cdlemg10a  34946  cdlemg12b  34950  cdlemg17b  34968  cdlemg31d  35006  cdlemg33b0  35007  cdlemg33a  35012  ltrnco  35025  ltrncom  35044  cdlemh  35123  cdlemk3  35139  cdlemk12  35156  cdlemk12u  35178  cdlemkfid1N  35227  cdlemk51  35259  cdlemk54  35264  cdlemk43N  35269  cdlemk35u  35270  cdlemk55u1  35271  cdlemk39u1  35273  cdlemk19u1  35275  dia2dimlem10  35380  dvhgrp  35414  dvh0g  35418  cdlemm10N  35425  diblsmopel  35478  cdlemn4  35505  cdlemn6  35509  cdlemn7  35510  dihordlem7  35521  dihord1  35525  dihord2pre  35532  dihvalcqat  35546  dihopelvalcpre  35555  dihord5apre  35569  dihord  35571  dih1  35593  dihglbcpreN  35607  dihjatc1  35618  dihmeetlem13N  35626  dihmeetALTN  35634  dihjatcclem1  35725  baerlem3lem1  36014  pellfundex  36468  rmxypairf1o  36494  rmxycomplete  36500  rmxyneg  36503  rmxyadd  36504  rmxy1  36505  rmxy0  36506  jm2.22  36580  proot1mul  36796  deg1mhm  36804  stoweidlem7  38900  stoweidlem36  38929