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  6078  caovcand  6081  caovordid  6085  caovordd  6087  caovdid  6094  caovdird  6097  swoer  6615  swoord1  6616  swoord2  6617  fimax2gtrilemstep  6956  iunfidisj  7005  ssfii  7033  suplub2ti  7060  prarloclem3  7557  fzosubel3  10263  seq3split  10559  seqsplitg  10560  seq3caopr  10566  seqcaoprg  10567  zsumdc  11527  fsumiun  11620  divalglemex  12063  pcgcd1  12466  strle1g  12724  mnd32g  13008  mnd12g  13009  mnd4g  13010  ismndd  13018  mndinvmod  13026  grpassd  13084  grpasscan2  13136  grpidrcan  13137  grpidlcan  13138  grpinvinv  13139  grplmulf1o  13146  grpinvssd  13149  grpinvadd  13150  grpsubrcan  13153  grpsubadd  13160  grpaddsubass  13162  grppncan  13163  grpsubsub4  13165  grppnpcan2  13166  grpnpncan  13167  grpnpncan0  13168  grpnnncan2  13169  dfgrp3mlem  13170  dfgrp3m  13171  grplactcnv  13174  imasgrp  13181  mhmmnd  13186  mulgaddcomlem  13215  mulgaddcom  13216  mulgnn0dir  13222  mulgdirlem  13223  mulgneg2  13226  mulgnnass  13227  mulgnn0ass  13228  mulgass  13229  mulgmodid  13231  nsgconj  13276  isnsg3  13277  nmzsubg  13280  ssnmz  13281  eqger  13294  eqgcpbl  13298  conjghm  13346  conjnmz  13349  conjnmzb  13350  abl32  13377  abladdsub4  13384  abladdsub  13385  ablpncan2  13386  ablsubsub  13388  rngass  13435  rnglz  13441  rngrz  13442  rngmneg1  13443  rngmneg2  13444  rngsubdi  13447  rngsubdir  13448  imasrng  13452  srgass  13467  srgmulgass  13485  srgpcomp  13486  srgpcompp  13487  srgpcomppsc  13488  ringass  13512  ringadd2  13523  ringo2times  13524  ringcom  13527  ringlz  13539  ringrz  13540  ringnegl  13547  ringnegr  13548  ringmneg1  13549  ringmneg2  13550  ringsubdi  13552  ringsubdir  13553  mulgass2  13554  imasring  13560  opprrng  13573  opprring  13575  mulgass3  13581  dvdsrtr  13597  dvdsrmul1  13598  unitgrp  13612  dvrass  13635  dvrcan1  13636  dvrcan3  13637  dvrdir  13639  rdivmuldivd  13640  rhmunitinv  13674  lringuplu  13692  subrginv  13733  unitrrg  13763  aprcotr  13781  islmod  13787  lmod0vs  13817  lmodvs0  13818  lmodvsmmulgdi  13819  lmodfopne  13822  lmodvneg1  13826  lmodvsneg  13827  lmodcom  13829  lmodsubvs  13839  lmodsubdi  13840  lmodsubdir  13841  islss3  13875  lss1d  13879  sralmod  13946  rnglidlmsgrp  13993  2idlcpblrng  14019  mulgrhm  14097  psmetsym  14497  psmettri  14498  psmetge0  14499  psmetres2  14501  xmetge0  14533  xmetsym  14536  xmettri  14540  metrtri  14545  xmetres2  14547  bldisj  14569  xblss2ps  14572  xblss2  14573  xmeter  14604  xmetxp  14675