Theorem syl13anc 1251

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 1179	. 2 |- ( ph -> ( ch /\ th /\ ta ) )
6		syl13anc.5	. 2 |- ( ( ps /\ ( ch /\ th /\ ta ) ) -> et )
7	1, 5, 6	syl2anc 411	1 |- ( ph -> et )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  syl23anc  1256  syl33anc  1264  caovassd  6105  caovcand  6108  caovordid  6112  caovordd  6114  caovdid  6121  caovdird  6124  swoer  6647  swoord1  6648  swoord2  6649  fimax2gtrilemstep  6996  iunfidisj  7047  ssfii  7075  suplub2ti  7102  prarloclem3  7609  fzosubel3  10323  seq3split  10631  seqsplitg  10632  seq3caopr  10638  seqcaoprg  10639  zsumdc  11666  fsumiun  11759  divalglemex  12204  pcgcd1  12622  strle1g  12909  prdssgrpd  13218  mnd32g  13230  mnd12g  13231  mnd4g  13232  ismndd  13240  mndinvmod  13248  prdsmndd  13251  imasmnd  13256  grpassd  13315  grpasscan2  13367  grpidrcan  13368  grpidlcan  13369  grpinvinv  13370  grplmulf1o  13377  grpinvssd  13380  grpinvadd  13381  grpsubrcan  13384  grpsubadd  13391  grpaddsubass  13393  grppncan  13394  grpsubsub4  13396  grppnpcan2  13397  grpnpncan  13398  grpnpncan0  13399  grpnnncan2  13400  dfgrp3mlem  13401  dfgrp3m  13402  grplactcnv  13405  imasgrp  13418  mhmmnd  13423  mulgaddcomlem  13452  mulgaddcom  13453  mulgnn0dir  13459  mulgdirlem  13460  mulgneg2  13463  mulgnnass  13464  mulgnn0ass  13465  mulgass  13466  mulgmodid  13468  nsgconj  13513  isnsg3  13514  nmzsubg  13517  ssnmz  13518  eqger  13531  eqgcpbl  13535  conjghm  13583  conjnmz  13586  conjnmzb  13587  abl32  13614  abladdsub4  13621  abladdsub  13622  ablpncan2  13623  ablsubsub  13625  rngass  13672  rnglz  13678  rngrz  13679  rngmneg1  13680  rngmneg2  13681  rngsubdi  13684  rngsubdir  13685  imasrng  13689  srgass  13704  srgmulgass  13722  srgpcomp  13723  srgpcompp  13724  srgpcomppsc  13725  ringass  13749  ringadd2  13760  ringo2times  13761  ringcom  13764  ringlz  13776  ringrz  13777  ringnegl  13784  ringnegr  13785  ringmneg1  13786  ringmneg2  13787  ringsubdi  13789  ringsubdir  13790  mulgass2  13791  imasring  13797  opprrng  13810  opprring  13812  mulgass3  13818  dvdsrtr  13834  dvdsrmul1  13835  unitgrp  13849  dvrass  13872  dvrcan1  13873  dvrcan3  13874  dvrdir  13876  rdivmuldivd  13877  rhmunitinv  13911  lringuplu  13929  subrginv  13970  unitrrg  14000  aprcotr  14018  islmod  14024  lmod0vs  14054  lmodvs0  14055  lmodvsmmulgdi  14056  lmodfopne  14059  lmodvneg1  14063  lmodvsneg  14064  lmodcom  14066  lmodsubvs  14076  lmodsubdi  14077  lmodsubdir  14078  islss3  14112  lss1d  14116  sralmod  14183  rnglidlmsgrp  14230  2idlcpblrng  14256  mulgrhm  14342  psmetsym  14772  psmettri  14773  psmetge0  14774  psmetres2  14776  xmetge0  14808  xmetsym  14811  xmettri  14815  metrtri  14820  xmetres2  14822  bldisj  14844  xblss2ps  14847  xblss2  14848  xmeter  14879  xmetxp  14950  dvdsppwf1o  15432  perfect1  15441  perfectlem1  15442  perfectlem2  15443