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  6080  caovcand  6083  caovordid  6087  caovordd  6089  caovdid  6096  caovdird  6099  swoer  6617  swoord1  6618  swoord2  6619  fimax2gtrilemstep  6958  iunfidisj  7007  ssfii  7035  suplub2ti  7062  prarloclem3  7559  fzosubel3  10266  seq3split  10562  seqsplitg  10563  seq3caopr  10569  seqcaoprg  10570  zsumdc  11530  fsumiun  11623  divalglemex  12066  pcgcd1  12469  strle1g  12727  mnd32g  13011  mnd12g  13012  mnd4g  13013  ismndd  13021  mndinvmod  13029  grpassd  13087  grpasscan2  13139  grpidrcan  13140  grpidlcan  13141  grpinvinv  13142  grplmulf1o  13149  grpinvssd  13152  grpinvadd  13153  grpsubrcan  13156  grpsubadd  13163  grpaddsubass  13165  grppncan  13166  grpsubsub4  13168  grppnpcan2  13169  grpnpncan  13170  grpnpncan0  13171  grpnnncan2  13172  dfgrp3mlem  13173  dfgrp3m  13174  grplactcnv  13177  imasgrp  13184  mhmmnd  13189  mulgaddcomlem  13218  mulgaddcom  13219  mulgnn0dir  13225  mulgdirlem  13226  mulgneg2  13229  mulgnnass  13230  mulgnn0ass  13231  mulgass  13232  mulgmodid  13234  nsgconj  13279  isnsg3  13280  nmzsubg  13283  ssnmz  13284  eqger  13297  eqgcpbl  13301  conjghm  13349  conjnmz  13352  conjnmzb  13353  abl32  13380  abladdsub4  13387  abladdsub  13388  ablpncan2  13389  ablsubsub  13391  rngass  13438  rnglz  13444  rngrz  13445  rngmneg1  13446  rngmneg2  13447  rngsubdi  13450  rngsubdir  13451  imasrng  13455  srgass  13470  srgmulgass  13488  srgpcomp  13489  srgpcompp  13490  srgpcomppsc  13491  ringass  13515  ringadd2  13526  ringo2times  13527  ringcom  13530  ringlz  13542  ringrz  13543  ringnegl  13550  ringnegr  13551  ringmneg1  13552  ringmneg2  13553  ringsubdi  13555  ringsubdir  13556  mulgass2  13557  imasring  13563  opprrng  13576  opprring  13578  mulgass3  13584  dvdsrtr  13600  dvdsrmul1  13601  unitgrp  13615  dvrass  13638  dvrcan1  13639  dvrcan3  13640  dvrdir  13642  rdivmuldivd  13643  rhmunitinv  13677  lringuplu  13695  subrginv  13736  unitrrg  13766  aprcotr  13784  islmod  13790  lmod0vs  13820  lmodvs0  13821  lmodvsmmulgdi  13822  lmodfopne  13825  lmodvneg1  13829  lmodvsneg  13830  lmodcom  13832  lmodsubvs  13842  lmodsubdi  13843  lmodsubdir  13844  islss3  13878  lss1d  13882  sralmod  13949  rnglidlmsgrp  13996  2idlcpblrng  14022  mulgrhm  14108  psmetsym  14508  psmettri  14509  psmetge0  14510  psmetres2  14512  xmetge0  14544  xmetsym  14547  xmettri  14551  metrtri  14556  xmetres2  14558  bldisj  14580  xblss2ps  14583  xblss2  14584  xmeter  14615  xmetxp  14686