Theorem syl132anc 1344

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

Hypotheses

Ref	Expression
syl12anc.1	|- ( ph -> ps )
syl12anc.2	|- ( ph -> ch )
syl12anc.3	|- ( ph -> th )
syl22anc.4	|- ( ph -> ta )
syl23anc.5	|- ( ph -> et )
syl33anc.6	|- ( ph -> ze )
syl132anc.7	|- ( ( ps /\ ( ch /\ th /\ ta ) /\ ( et /\ ze ) ) -> si )

Assertion

Ref	Expression
syl132anc	|- ( ph -> si )

Proof of Theorem syl132anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 |- ( ph -> ps )
2		syl12anc.2	. 2 |- ( ph -> ch )
3		syl12anc.3	. 2 |- ( ph -> th )
4		syl22anc.4	. 2 |- ( ph -> ta )
5		syl23anc.5	. . 3 |- ( ph -> et )
6		syl33anc.6	. . 3 |- ( ph -> ze )
7	5, 6	jca 554	. 2 |- ( ph -> ( et /\ ze ) )
8		syl132anc.7	. 2 |- ( ( ps /\ ( ch /\ th /\ ta ) /\ ( et /\ ze ) ) -> si )
9	1, 2, 3, 4, 7, 8	syl131anc 1339	1 |- ( ph -> si )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  drsdirfi  16938  eengtrkg  25865  eengtrkge  25866  qqhval2lem  30025  qqhghm  30032  qqhrhm  30033  btwncomim  32120  btwnswapid  32124  btwnintr  32126  btwnexch3  32127  btwnxfr  32163  linecgrand  32189  btwnconn1lem13  32206  seglecgr12im  32217  segletr  32221  linethru  32260  lshpkrlem5  34401  omlmod1i2N  34547  omlspjN  34548  atcmp  34598  atexchcvrN  34726  atbtwn  34732  1cvratlt  34760  2atjlej  34765  hlatexch3N  34766  hlatexch4  34767  atcvrlln2  34805  atcvrlln  34806  llncmp  34808  llncvrlpln  34844  lplncmp  34848  lplnexllnN  34850  2llnjaN  34852  4atlem11  34895  lplncvrlvol  34902  lvolcmp  34903  dalem1  34945  dalem2  34947  dalem24  34983  dalem25  34984  dalem42  35000  lncvrat  35068  2llnma3r  35074  lhp2lt  35287  4atexlemswapqr  35349  4atexlemtlw  35353  4atexlemntlpq  35354  4atexlemc  35355  4atexlemnclw  35356  4atexlemcnd  35358  4atex2  35363  cdlemd1  35485  cdlemd7  35491  cdleme0e  35504  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme16aN  35546  cdleme11c  35548  cdleme11e  35550  cdleme11l  35556  cdleme11  35557  cdleme14  35560  cdleme15a  35561  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme16e  35569  cdleme16f  35570  cdleme18b  35579  cdleme19d  35594  cdleme20d  35600  cdleme20f  35602  cdleme20h  35604  cdleme20l1  35608  cdleme20l2  35609  cdleme20l  35610  cdleme21a  35613  cdleme21b  35614  cdleme21c  35615  cdleme21ct  35617  cdleme22f2  35635  cdleme22g  35636  cdlemefr32sn2aw  35692  cdleme43fsv1snlem  35708  cdleme32b  35730  cdleme35a  35736  cdleme35f  35742  cdleme36m  35749  cdleme37m  35750  cdleme42k  35772  cdleme43bN  35778  cdleme17d2  35783  cdlemeg46req  35817  cdlemeg46gfv  35818  cdlemeg46gfre  35820  cdleme50trn2a  35838  cdleme50trn2  35839  cdlemg8b  35916  cdlemg10a  35928  cdlemg12d  35934  cdlemg13a  35939  cdlemg15  35944  cdlemg16z  35947  cdlemg18b  35967  cdlemg18c  35968  cdlemg18  35970  cdlemg27b  35984  cdlemg33  35999  cdlemg42  36017  trljco  36028  cdlemj3  36111  tendoid0  36113  cdlemk3  36121  cdlemk22  36181  cdlemk36  36201  cdlemkfid3N  36213  cdlemk47  36237  cdlemk48  36238  cdlemk49  36239  cdlemk50  36240  cdlemk51  36241  cdlemk52  36242  cdlemk53a  36243  cdlemk53b  36244  cdlemk53  36245  cdlemk54  36246  cdlemk55  36249  cdlemk35u  36252  cdlemk39u1  36255  cdleml3N  36266