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  7342  prarloclem3  7865  fzosubel3  10625  seq3split  10940  seqsplitg  10941  seq3caopr  10947  seqcaoprg  10948  zsumdc  12170  fsumiun  12263  divalglemex  12708  pcgcd1  13130  strle1g  13513  mnd32g  13793  mnd12g  13794  mnd4g  13795  ismndd  13803  mndinvmod  13811  imasmnd  13813  grpassd  13870  grpasscan2  13922  grpidrcan  13923  grpidlcan  13924  grpinvinv  13925  grplmulf1o  13932  grpinvssd  13935  grpinvadd  13936  grpsubrcan  13939  grpsubadd  13946  grpaddsubass  13948  grppncan  13949  grpsubsub4  13951  grppnpcan2  13952  grpnpncan  13953  grpnpncan0  13954  grpnnncan2  13955  dfgrp3mlem  13956  dfgrp3m  13957  grplactcnv  13960  imasgrp  13967  mhmmnd  13972  mulgaddcomlem  14001  mulgaddcom  14002  mulgnn0dir  14008  mulgdirlem  14009  mulgneg2  14012  mulgnnass  14013  mulgnn0ass  14014  mulgass  14015  mulgmodid  14017  nsgconj  14062  isnsg3  14063  nmzsubg  14066  ssnmz  14067  eqger  14080  eqgcpbl  14084  conjghm  14132  conjnmz  14135  conjnmzb  14136  cntzsgrpcl  14161  cntzsubm  14164  cntzsubg  14165  abl32  14194  abladdsub4  14202  abladdsub  14203  ablpncan2  14204  ablsubsub  14206  prdssgrpd  14275  prdsmndd  14278  rngass  14322  rnglz  14328  rngrz  14329  rngmneg1  14330  rngmneg2  14331  rngsubdi  14334  rngsubdir  14335  imasrng  14339  srgass  14359  srgmulgass  14377  srgpcomp  14378  srgpcompp  14379  srgpcomppsc  14380  ringass  14404  ringadd2  14416  ringo2times  14417  ringcom  14420  ringlz  14432  ringrz  14433  ringnegl  14440  ringnegr  14441  ringmneg1  14442  ringmneg2  14443  ringsubdi  14445  ringsubdir  14446  mulgass2  14447  imasring  14453  opprrng  14466  opprring  14468  mulgass3  14475  dvdsrtr  14492  dvdsrmul1  14493  unitgrp  14507  dvrass  14530  dvrcan1  14531  dvrcan3  14532  dvrdir  14534  rdivmuldivd  14535  rhmunitinv  14569  lringuplu  14587  subrginv  14629  unitrrg  14660  aprcotr  14681  islmod  14711  lmod0vs  14742  lmodvs0  14743  lmodvsmmulgdi  14744  lmodfopne  14747  lmodvneg1  14751  lmodvsneg  14752  lmodcom  14754  lmodsubvs  14764  lmodsubdi  14765  lmodsubdir  14766  islss3  14800  lss1d  14804  sralmod  14871  rnglidlmsgrp  14918  2idlcpblrng  14944  mulgrhm  15028  assa2ass  15093  assa2ass2  15094  asclghm  15109  asclmul1  15113  asclmul2  15114  ascldimul  15115  assamulgscmlem2  15126  asclmulg  15128  psmetsym  15521  psmettri  15522  psmetge0  15523  psmetres2  15525  xmetge0  15557  xmetsym  15560  xmettri  15564  metrtri  15569  xmetres2  15571  bldisj  15593  xblss2ps  15596  xblss2  15597  xmeter  15628  xmetxp  15699  dvdsppwf1o  16244  perfect1  16259  perfectlem1  16260  perfectlem2  16261  3dom  17184