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  10624  seq3split  10938  seqsplitg  10939  seq3caopr  10945  seqcaoprg  10946  zsumdc  12167  fsumiun  12260  divalglemex  12705  pcgcd1  13127  strle1g  13509  mnd32g  13789  mnd12g  13790  mnd4g  13791  ismndd  13799  mndinvmod  13807  imasmnd  13809  grpassd  13866  grpasscan2  13918  grpidrcan  13919  grpidlcan  13920  grpinvinv  13921  grplmulf1o  13928  grpinvssd  13931  grpinvadd  13932  grpsubrcan  13935  grpsubadd  13942  grpaddsubass  13944  grppncan  13945  grpsubsub4  13947  grppnpcan2  13948  grpnpncan  13949  grpnpncan0  13950  grpnnncan2  13951  dfgrp3mlem  13952  dfgrp3m  13953  grplactcnv  13956  imasgrp  13963  mhmmnd  13968  mulgaddcomlem  13997  mulgaddcom  13998  mulgnn0dir  14004  mulgdirlem  14005  mulgneg2  14008  mulgnnass  14009  mulgnn0ass  14010  mulgass  14011  mulgmodid  14013  nsgconj  14058  isnsg3  14059  nmzsubg  14062  ssnmz  14063  eqger  14076  eqgcpbl  14080  conjghm  14128  conjnmz  14131  conjnmzb  14132  abl32  14159  abladdsub4  14167  abladdsub  14168  ablpncan2  14169  ablsubsub  14171  prdssgrpd  14240  prdsmndd  14243  rngass  14287  rnglz  14293  rngrz  14294  rngmneg1  14295  rngmneg2  14296  rngsubdi  14299  rngsubdir  14300  imasrng  14304  srgass  14324  srgmulgass  14342  srgpcomp  14343  srgpcompp  14344  srgpcomppsc  14345  ringass  14369  ringadd2  14381  ringo2times  14382  ringcom  14385  ringlz  14397  ringrz  14398  ringnegl  14405  ringnegr  14406  ringmneg1  14407  ringmneg2  14408  ringsubdi  14410  ringsubdir  14411  mulgass2  14412  imasring  14418  opprrng  14431  opprring  14433  mulgass3  14440  dvdsrtr  14457  dvdsrmul1  14458  unitgrp  14472  dvrass  14495  dvrcan1  14496  dvrcan3  14497  dvrdir  14499  rdivmuldivd  14500  rhmunitinv  14534  lringuplu  14552  subrginv  14594  unitrrg  14625  aprcotr  14646  islmod  14676  lmod0vs  14707  lmodvs0  14708  lmodvsmmulgdi  14709  lmodfopne  14712  lmodvneg1  14716  lmodvsneg  14717  lmodcom  14719  lmodsubvs  14729  lmodsubdi  14730  lmodsubdir  14731  islss3  14765  lss1d  14769  sralmod  14836  rnglidlmsgrp  14883  2idlcpblrng  14909  mulgrhm  14993  assa2ass  15058  assa2ass2  15059  asclghm  15074  asclmul1  15078  asclmul2  15079  ascldimul  15080  assamulgscmlem2  15091  asclmulg  15093  psmetsym  15479  psmettri  15480  psmetge0  15481  psmetres2  15483  xmetge0  15515  xmetsym  15518  xmettri  15522  metrtri  15527  xmetres2  15529  bldisj  15551  xblss2ps  15554  xblss2  15555  xmeter  15586  xmetxp  15657  dvdsppwf1o  16184  perfect1  16196  perfectlem1  16197  perfectlem2  16198  3dom  17116