Theorem syl132anc 1386

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 511	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁))
8		syl132anc.7	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)
9	1, 2, 3, 4, 7, 8	syl131anc 1381	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  drsdirfi  17938  eengtrkg  27257  eengtrkge  27258  mgcmnt1  31172  mgcmnt2  31173  mgcmntco  31174  dfmgc2lem  31175  linds2eq  31477  qqhval2lem  31831  qqhghm  31838  qqhrhm  31839  btwncomim  34242  btwnswapid  34246  btwnintr  34248  btwnexch3  34249  btwnxfr  34285  linecgrand  34311  btwnconn1lem13  34328  seglecgr12im  34339  segletr  34343  linethru  34382  lshpkrlem5  37055  omlmod1i2N  37201  omlspjN  37202  atcmp  37252  atexchcvrN  37381  atbtwn  37387  1cvratlt  37415  2atjlej  37420  hlatexch3N  37421  hlatexch4  37422  atcvrlln2  37460  atcvrlln  37461  llncmp  37463  llncvrlpln  37499  lplncmp  37503  lplnexllnN  37505  2llnjaN  37507  4atlem11  37550  lplncvrlvol  37557  lvolcmp  37558  dalem1  37600  dalem2  37602  dalem24  37638  dalem25  37639  dalem42  37655  lncvrat  37723  2llnma3r  37729  lhp2lt  37942  4atexlemswapqr  38004  4atexlemtlw  38008  4atexlemntlpq  38009  4atexlemc  38010  4atexlemnclw  38011  4atexlemcnd  38013  4atex2  38018  cdlemd1  38139  cdlemd7  38145  cdleme0e  38158  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme16aN  38200  cdleme11c  38202  cdleme11e  38204  cdleme11l  38210  cdleme11  38211  cdleme14  38214  cdleme15a  38215  cdleme16b  38220  cdleme16c  38221  cdleme16d  38222  cdleme16e  38223  cdleme16f  38224  cdleme18b  38233  cdleme19d  38247  cdleme20d  38253  cdleme20f  38255  cdleme20h  38257  cdleme20l1  38261  cdleme20l2  38262  cdleme20l  38263  cdleme21a  38266  cdleme21b  38267  cdleme21c  38268  cdleme21ct  38270  cdleme22f2  38288  cdleme22g  38289  cdlemefr32sn2aw  38345  cdleme43fsv1snlem  38361  cdleme32b  38383  cdleme35a  38389  cdleme35f  38395  cdleme36m  38402  cdleme37m  38403  cdleme42k  38425  cdleme43bN  38431  cdleme17d2  38436  cdlemeg46req  38470  cdlemeg46gfv  38471  cdlemeg46gfre  38473  cdleme50trn2a  38491  cdleme50trn2  38492  cdlemg8b  38569  cdlemg10a  38581  cdlemg12d  38587  cdlemg13a  38592  cdlemg15  38597  cdlemg16z  38600  cdlemg18b  38620  cdlemg18c  38621  cdlemg18  38623  cdlemg27b  38637  cdlemg33  38652  cdlemg42  38670  trljco  38681  cdlemj3  38764  tendoid0  38766  cdlemk3  38774  cdlemk22  38834  cdlemk36  38854  cdlemkfid3N  38866  cdlemk47  38890  cdlemk48  38891  cdlemk49  38892  cdlemk50  38893  cdlemk51  38894  cdlemk52  38895  cdlemk53a  38896  cdlemk53b  38897  cdlemk53  38898  cdlemk54  38899  cdlemk55  38902  cdlemk35u  38905  cdlemk39u1  38908  cdleml3N  38919