Theorem syl132anc 1416

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

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl132anc.7	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)

Assertion

Ref	Expression
syl132anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl132anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6		syl33anc.6	. . 3 ⊢ (𝜑 → 𝜁)
7	5, 6	jca 521	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁))
8		syl132anc.7	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)
9	1, 2, 3, 4, 7, 8	syl131anc 1411	1 ⊢ (𝜑 → 𝜎)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  drsdirfi  18505  eengtrkg  29591  eengtrkge  29592  mgcmnt1  33620  mgcmnt2  33621  mgcmntco  33622  dfmgc2lem  33623  gsumtp  33692  linds2eq  34003  evl1deg1  34175  evl1deg3  34177  qqhval2lem  34680  qqhghm  34687  qqhrhm  34688  btwncomim  36955  btwnswapid  36959  btwnintr  36961  btwnexch3  36962  btwnxfr  36998  linecgrand  37024  btwnconn1lem13  37041  seglecgr12im  37052  segletr  37056  linethru  37095  lshpkrlem5  40362  omlmod1i2N  40508  omlspjN  40509  atcmp  40559  atexchcvrN  40688  atbtwn  40694  1cvratlt  40722  2atjlej  40727  hlatexch3N  40728  hlatexch4  40729  atcvrlln2  40767  atcvrlln  40768  llncmp  40770  llncvrlpln  40806  lplncmp  40810  lplnexllnN  40812  2llnjaN  40814  4atlem11  40857  lplncvrlvol  40864  lvolcmp  40865  dalem1  40907  dalem2  40909  dalem24  40945  dalem25  40946  dalem42  40962  lncvrat  41030  2llnma3r  41036  lhp2lt  41249  4atexlemswapqr  41311  4atexlemtlw  41315  4atexlemntlpq  41316  4atexlemc  41317  4atexlemnclw  41318  4atexlemcnd  41320  4atex2  41325  cdlemd1  41446  cdlemd7  41452  cdleme0e  41465  cdleme7c  41493  cdleme7d  41494  cdleme7e  41495  cdleme7ga  41496  cdleme7  41497  cdleme16aN  41507  cdleme11c  41509  cdleme11e  41511  cdleme11l  41517  cdleme11  41518  cdleme14  41521  cdleme15a  41522  cdleme16b  41527  cdleme16c  41528  cdleme16d  41529  cdleme16e  41530  cdleme16f  41531  cdleme18b  41540  cdleme19d  41554  cdleme20d  41560  cdleme20f  41562  cdleme20h  41564  cdleme20l1  41568  cdleme20l2  41569  cdleme20l  41570  cdleme21a  41573  cdleme21b  41574  cdleme21c  41575  cdleme21ct  41577  cdleme22f2  41595  cdleme22g  41596  cdlemefr32sn2aw  41652  cdleme43fsv1snlem  41668  cdleme32b  41690  cdleme35a  41696  cdleme35f  41702  cdleme36m  41709  cdleme37m  41710  cdleme42k  41732  cdleme43bN  41738  cdleme17d2  41743  cdlemeg46req  41777  cdlemeg46gfv  41778  cdlemeg46gfre  41780  cdleme50trn2a  41798  cdleme50trn2  41799  cdlemg8b  41876  cdlemg10a  41888  cdlemg12d  41894  cdlemg13a  41899  cdlemg15  41904  cdlemg16z  41907  cdlemg18b  41927  cdlemg18c  41928  cdlemg18  41930  cdlemg27b  41944  cdlemg33  41959  cdlemg42  41977  trljco  41988  cdlemj3  42071  tendoid0  42073  cdlemk3  42081  cdlemk22  42141  cdlemk36  42161  cdlemkfid3N  42173  cdlemk47  42197  cdlemk48  42198  cdlemk49  42199  cdlemk50  42200  cdlemk51  42201  cdlemk52  42202  cdlemk53a  42203  cdlemk53b  42204  cdlemk53  42205  cdlemk54  42206  cdlemk55  42209  cdlemk35u  42212  cdlemk39u1  42215  cdleml3N  42226  m1modnep2mod  48631  ssccatid  50389