Theorem syl13anc 1280

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

Hypotheses

Ref	Expression
sylXanc.1	|- ( ph -> ps )
sylXanc.2	|- ( ph -> ch )
sylXanc.3	|- ( ph -> th )
sylXanc.4	|- ( ph -> ta )
syl13anc.5	|- ( ( ps /\ ( ch /\ th /\ ta ) ) -> et )

Assertion

Ref	Expression
syl13anc	|- ( ph -> et )

Proof of Theorem syl13anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4		sylXanc.4	. . 3 |- ( ph -> ta )
5	2, 3, 4	3jca 1208	. 2 |- ( ph -> ( ch /\ th /\ ta ) )
6		syl13anc.5	. 2 |- ( ( ps /\ ( ch /\ th /\ ta ) ) -> et )
7	1, 5, 6	syl2anc 415	1 |- ( ph -> et )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl23anc  1285  syl33anc  1293  caovassd  6249  caovcand  6252  caovordid  6256  caovordd  6258  caovdid  6265  caovdird  6268  swoer  6835  swoord1  6836  swoord2  6837  fimax2gtrilemstep  7205  iunfidisj  7260  ssfii  7308  suplub2ti  7341  prarloclem3  7864  fzosubel3  10614  seq3split  10925  seqsplitg  10926  seq3caopr  10932  seqcaoprg  10933  zsumdc  12151  fsumiun  12244  divalglemex  12689  pcgcd1  13107  strle1g  13460  mnd32g  13740  mnd12g  13741  mnd4g  13742  ismndd  13750  mndinvmod  13758  imasmnd  13760  grpassd  13817  grpasscan2  13869  grpidrcan  13870  grpidlcan  13871  grpinvinv  13872  grplmulf1o  13879  grpinvssd  13882  grpinvadd  13883  grpsubrcan  13886  grpsubadd  13893  grpaddsubass  13895  grppncan  13896  grpsubsub4  13898  grppnpcan2  13899  grpnpncan  13900  grpnpncan0  13901  grpnnncan2  13902  dfgrp3mlem  13903  dfgrp3m  13904  grplactcnv  13907  imasgrp  13914  mhmmnd  13919  mulgaddcomlem  13948  mulgaddcom  13949  mulgnn0dir  13955  mulgdirlem  13956  mulgneg2  13959  mulgnnass  13960  mulgnn0ass  13961  mulgass  13962  mulgmodid  13964  nsgconj  14009  isnsg3  14010  nmzsubg  14013  ssnmz  14014  eqger  14027  eqgcpbl  14031  conjghm  14079  conjnmz  14082  conjnmzb  14083  abl32  14110  abladdsub4  14118  abladdsub  14119  ablpncan2  14120  ablsubsub  14122  prdssgrpd  14191  prdsmndd  14194  rngass  14238  rnglz  14244  rngrz  14245  rngmneg1  14246  rngmneg2  14247  rngsubdi  14250  rngsubdir  14251  imasrng  14255  srgass  14275  srgmulgass  14293  srgpcomp  14294  srgpcompp  14295  srgpcomppsc  14296  ringass  14320  ringadd2  14332  ringo2times  14333  ringcom  14336  ringlz  14348  ringrz  14349  ringnegl  14356  ringnegr  14357  ringmneg1  14358  ringmneg2  14359  ringsubdi  14361  ringsubdir  14362  mulgass2  14363  imasring  14369  opprrng  14382  opprring  14384  mulgass3  14391  dvdsrtr  14408  dvdsrmul1  14409  unitgrp  14423  dvrass  14446  dvrcan1  14447  dvrcan3  14448  dvrdir  14450  rdivmuldivd  14451  rhmunitinv  14485  lringuplu  14503  subrginv  14545  unitrrg  14576  aprcotr  14597  islmod  14627  lmod0vs  14658  lmodvs0  14659  lmodvsmmulgdi  14660  lmodfopne  14663  lmodvneg1  14667  lmodvsneg  14668  lmodcom  14670  lmodsubvs  14680  lmodsubdi  14681  lmodsubdir  14682  islss3  14716  lss1d  14720  sralmod  14787  rnglidlmsgrp  14834  2idlcpblrng  14860  mulgrhm  14944  assa2ass  15009  assa2ass2  15010  asclghm  15025  asclmul1  15029  asclmul2  15030  ascldimul  15031  assamulgscmlem2  15042  asclmulg  15044  psmetsym  15430  psmettri  15431  psmetge0  15432  psmetres2  15434  xmetge0  15466  xmetsym  15469  xmettri  15473  metrtri  15478  xmetres2  15480  bldisj  15502  xblss2ps  15505  xblss2  15506  xmeter  15537  xmetxp  15608  dvdsppwf1o  16103  perfect1  16112  perfectlem1  16113  perfectlem2  16114  3dom  17018