Theorem syl13anc 1252

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 1180	. 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 981

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 983

This theorem is referenced by:  syl23anc  1257  syl33anc  1265  caovassd  6129  caovcand  6132  caovordid  6136  caovordd  6138  caovdid  6145  caovdird  6148  swoer  6671  swoord1  6672  swoord2  6673  fimax2gtrilemstep  7023  iunfidisj  7074  ssfii  7102  suplub2ti  7129  prarloclem3  7645  fzosubel3  10362  seq3split  10670  seqsplitg  10671  seq3caopr  10677  seqcaoprg  10678  zsumdc  11810  fsumiun  11903  divalglemex  12348  pcgcd1  12766  strle1g  13053  prdssgrpd  13362  mnd32g  13374  mnd12g  13375  mnd4g  13376  ismndd  13384  mndinvmod  13392  prdsmndd  13395  imasmnd  13400  grpassd  13459  grpasscan2  13511  grpidrcan  13512  grpidlcan  13513  grpinvinv  13514  grplmulf1o  13521  grpinvssd  13524  grpinvadd  13525  grpsubrcan  13528  grpsubadd  13535  grpaddsubass  13537  grppncan  13538  grpsubsub4  13540  grppnpcan2  13541  grpnpncan  13542  grpnpncan0  13543  grpnnncan2  13544  dfgrp3mlem  13545  dfgrp3m  13546  grplactcnv  13549  imasgrp  13562  mhmmnd  13567  mulgaddcomlem  13596  mulgaddcom  13597  mulgnn0dir  13603  mulgdirlem  13604  mulgneg2  13607  mulgnnass  13608  mulgnn0ass  13609  mulgass  13610  mulgmodid  13612  nsgconj  13657  isnsg3  13658  nmzsubg  13661  ssnmz  13662  eqger  13675  eqgcpbl  13679  conjghm  13727  conjnmz  13730  conjnmzb  13731  abl32  13758  abladdsub4  13765  abladdsub  13766  ablpncan2  13767  ablsubsub  13769  rngass  13816  rnglz  13822  rngrz  13823  rngmneg1  13824  rngmneg2  13825  rngsubdi  13828  rngsubdir  13829  imasrng  13833  srgass  13848  srgmulgass  13866  srgpcomp  13867  srgpcompp  13868  srgpcomppsc  13869  ringass  13893  ringadd2  13904  ringo2times  13905  ringcom  13908  ringlz  13920  ringrz  13921  ringnegl  13928  ringnegr  13929  ringmneg1  13930  ringmneg2  13931  ringsubdi  13933  ringsubdir  13934  mulgass2  13935  imasring  13941  opprrng  13954  opprring  13956  mulgass3  13962  dvdsrtr  13978  dvdsrmul1  13979  unitgrp  13993  dvrass  14016  dvrcan1  14017  dvrcan3  14018  dvrdir  14020  rdivmuldivd  14021  rhmunitinv  14055  lringuplu  14073  subrginv  14114  unitrrg  14144  aprcotr  14162  islmod  14168  lmod0vs  14198  lmodvs0  14199  lmodvsmmulgdi  14200  lmodfopne  14203  lmodvneg1  14207  lmodvsneg  14208  lmodcom  14210  lmodsubvs  14220  lmodsubdi  14221  lmodsubdir  14222  islss3  14256  lss1d  14260  sralmod  14327  rnglidlmsgrp  14374  2idlcpblrng  14400  mulgrhm  14486  psmetsym  14916  psmettri  14917  psmetge0  14918  psmetres2  14920  xmetge0  14952  xmetsym  14955  xmettri  14959  metrtri  14964  xmetres2  14966  bldisj  14988  xblss2ps  14991  xblss2  14992  xmeter  15023  xmetxp  15094  dvdsppwf1o  15576  perfect1  15585  perfectlem1  15586  perfectlem2  15587