Theorem syl132anc 1415

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 1410	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  18397  eengtrkg  29429  eengtrkge  29430  mgcmnt1  33419  mgcmnt2  33420  mgcmntco  33421  dfmgc2lem  33422  gsumtp  33491  linds2eq  33801  evl1deg1  33973  evl1deg3  33975  qqhval2lem  34478  qqhghm  34485  qqhrhm  34486  btwncomim  36580  btwnswapid  36584  btwnintr  36586  btwnexch3  36587  btwnxfr  36623  linecgrand  36649  btwnconn1lem13  36666  seglecgr12im  36677  segletr  36681  linethru  36720  lshpkrlem5  39974  omlmod1i2N  40120  omlspjN  40121  atcmp  40171  atexchcvrN  40300  atbtwn  40306  1cvratlt  40334  2atjlej  40339  hlatexch3N  40340  hlatexch4  40341  atcvrlln2  40379  atcvrlln  40380  llncmp  40382  llncvrlpln  40418  lplncmp  40422  lplnexllnN  40424  2llnjaN  40426  4atlem11  40469  lplncvrlvol  40476  lvolcmp  40477  dalem1  40519  dalem2  40521  dalem24  40557  dalem25  40558  dalem42  40574  lncvrat  40642  2llnma3r  40648  lhp2lt  40861  4atexlemswapqr  40923  4atexlemtlw  40927  4atexlemntlpq  40928  4atexlemc  40929  4atexlemnclw  40930  4atexlemcnd  40932  4atex2  40937  cdlemd1  41058  cdlemd7  41064  cdleme0e  41077  cdleme7c  41105  cdleme7d  41106  cdleme7e  41107  cdleme7ga  41108  cdleme7  41109  cdleme16aN  41119  cdleme11c  41121  cdleme11e  41123  cdleme11l  41129  cdleme11  41130  cdleme14  41133  cdleme15a  41134  cdleme16b  41139  cdleme16c  41140  cdleme16d  41141  cdleme16e  41142  cdleme16f  41143  cdleme18b  41152  cdleme19d  41166  cdleme20d  41172  cdleme20f  41174  cdleme20h  41176  cdleme20l1  41180  cdleme20l2  41181  cdleme20l  41182  cdleme21a  41185  cdleme21b  41186  cdleme21c  41187  cdleme21ct  41189  cdleme22f2  41207  cdleme22g  41208  cdlemefr32sn2aw  41264  cdleme43fsv1snlem  41280  cdleme32b  41302  cdleme35a  41308  cdleme35f  41314  cdleme36m  41321  cdleme37m  41322  cdleme42k  41344  cdleme43bN  41350  cdleme17d2  41355  cdlemeg46req  41389  cdlemeg46gfv  41390  cdlemeg46gfre  41392  cdleme50trn2a  41410  cdleme50trn2  41411  cdlemg8b  41488  cdlemg10a  41500  cdlemg12d  41506  cdlemg13a  41511  cdlemg15  41516  cdlemg16z  41519  cdlemg18b  41539  cdlemg18c  41540  cdlemg18  41542  cdlemg27b  41556  cdlemg33  41571  cdlemg42  41589  trljco  41600  cdlemj3  41683  tendoid0  41685  cdlemk3  41693  cdlemk22  41753  cdlemk36  41773  cdlemkfid3N  41785  cdlemk47  41809  cdlemk48  41810  cdlemk49  41811  cdlemk50  41812  cdlemk51  41813  cdlemk52  41814  cdlemk53a  41815  cdlemk53b  41816  cdlemk53  41817  cdlemk54  41818  cdlemk55  41821  cdlemk35u  41824  cdlemk39u1  41827  cdleml3N  41838  m1modnep2mod  48233  ssccatid  49985