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  6057  caovcand  6060  caovordid  6064  caovordd  6066  caovdid  6073  caovdird  6076  swoer  6588  swoord1  6589  swoord2  6590  fimax2gtrilemstep  6929  iunfidisj  6976  ssfii  7004  suplub2ti  7031  prarloclem3  7527  fzosubel3  10228  seq3split  10512  seq3caopr  10516  zsumdc  11427  fsumiun  11520  divalglemex  11962  pcgcd1  12363  strle1g  12621  mnd32g  12903  mnd12g  12904  mnd4g  12905  ismndd  12913  mndinvmod  12921  grpassd  12972  grpasscan2  13023  grpidrcan  13024  grpidlcan  13025  grpinvinv  13026  grplmulf1o  13033  grpinvssd  13036  grpinvadd  13037  grpsubrcan  13040  grpsubadd  13047  grpaddsubass  13049  grppncan  13050  grpsubsub4  13052  grppnpcan2  13053  grpnpncan  13054  grpnpncan0  13055  grpnnncan2  13056  dfgrp3mlem  13057  dfgrp3m  13058  grplactcnv  13061  imasgrp  13068  mhmmnd  13073  mulgaddcomlem  13102  mulgaddcom  13103  mulgnn0dir  13109  mulgdirlem  13110  mulgneg2  13113  mulgnnass  13114  mulgnn0ass  13115  mulgass  13116  mulgmodid  13118  nsgconj  13162  isnsg3  13163  nmzsubg  13166  ssnmz  13167  eqger  13180  eqgcpbl  13184  conjghm  13232  conjnmz  13235  conjnmzb  13236  abl32  13263  abladdsub4  13270  abladdsub  13271  ablpncan2  13272  ablsubsub  13274  rngass  13310  rnglz  13316  rngrz  13317  rngmneg1  13318  rngmneg2  13319  rngsubdi  13322  rngsubdir  13323  imasrng  13327  srgass  13342  srgmulgass  13360  srgpcomp  13361  srgpcompp  13362  srgpcomppsc  13363  ringass  13387  ringadd2  13398  ringo2times  13399  ringcom  13402  ringlz  13414  ringrz  13415  ringnegl  13420  ringnegr  13421  ringmneg1  13422  ringmneg2  13423  ringsubdi  13425  ringsubdir  13426  mulgass2  13427  imasring  13431  opprrng  13444  opprring  13446  mulgass3  13452  dvdsrtr  13468  dvdsrmul1  13469  unitgrp  13483  dvrass  13506  dvrcan1  13507  dvrcan3  13508  dvrdir  13510  rdivmuldivd  13511  rhmunitinv  13545  lringuplu  13560  subrginv  13601  aprcotr  13618  islmod  13624  lmod0vs  13654  lmodvs0  13655  lmodvsmmulgdi  13656  lmodfopne  13659  lmodvneg1  13663  lmodvsneg  13664  lmodcom  13666  lmodsubvs  13676  lmodsubdi  13677  lmodsubdir  13678  islss3  13712  lss1d  13716  sralmod  13783  rnglidlmsgrp  13830  2idlcpblrng  13855  mulgrhm  13924  psmetsym  14306  psmettri  14307  psmetge0  14308  psmetres2  14310  xmetge0  14342  xmetsym  14345  xmettri  14349  metrtri  14354  xmetres2  14356  bldisj  14378  xblss2ps  14381  xblss2  14382  xmeter  14413  xmetxp  14484