Theorem syl13anc 1276

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 1204	. 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 1005

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 1007

This theorem is referenced by:  syl23anc  1281  syl33anc  1289  caovassd  6222  caovcand  6225  caovordid  6229  caovordd  6231  caovdid  6238  caovdird  6241  swoer  6808  swoord1  6809  swoord2  6810  fimax2gtrilemstep  7171  iunfidisj  7226  ssfii  7274  suplub2ti  7305  prarloclem3  7828  fzosubel3  10563  seq3split  10874  seqsplitg  10875  seq3caopr  10881  seqcaoprg  10882  zsumdc  12095  fsumiun  12188  divalglemex  12633  pcgcd1  13051  strle1g  13403  mnd32g  13688  mnd12g  13689  mnd4g  13690  ismndd  13698  mndinvmod  13706  imasmnd  13708  grpassd  13767  grpasscan2  13819  grpidrcan  13820  grpidlcan  13821  grpinvinv  13822  grplmulf1o  13829  grpinvssd  13832  grpinvadd  13833  grpsubrcan  13836  grpsubadd  13843  grpaddsubass  13845  grppncan  13846  grpsubsub4  13848  grppnpcan2  13849  grpnpncan  13850  grpnpncan0  13851  grpnnncan2  13852  dfgrp3mlem  13853  dfgrp3m  13854  grplactcnv  13857  imasgrp  13864  mhmmnd  13869  mulgaddcomlem  13898  mulgaddcom  13899  mulgnn0dir  13905  mulgdirlem  13906  mulgneg2  13909  mulgnnass  13910  mulgnn0ass  13911  mulgass  13912  mulgmodid  13914  nsgconj  13959  isnsg3  13960  nmzsubg  13963  ssnmz  13964  eqger  13977  eqgcpbl  13981  conjghm  14029  conjnmz  14032  conjnmzb  14033  abl32  14060  abladdsub4  14067  abladdsub  14068  ablpncan2  14069  ablsubsub  14071  prdssgrpd  14133  prdsmndd  14136  rngass  14178  rnglz  14184  rngrz  14185  rngmneg1  14186  rngmneg2  14187  rngsubdi  14190  rngsubdir  14191  imasrng  14195  srgass  14214  srgmulgass  14232  srgpcomp  14233  srgpcompp  14234  srgpcomppsc  14235  ringass  14259  ringadd2  14270  ringo2times  14271  ringcom  14274  ringlz  14286  ringrz  14287  ringnegl  14294  ringnegr  14295  ringmneg1  14296  ringmneg2  14297  ringsubdi  14299  ringsubdir  14300  mulgass2  14301  imasring  14307  opprrng  14320  opprring  14322  mulgass3  14329  dvdsrtr  14346  dvdsrmul1  14347  unitgrp  14361  dvrass  14384  dvrcan1  14385  dvrcan3  14386  dvrdir  14388  rdivmuldivd  14389  rhmunitinv  14423  lringuplu  14441  subrginv  14483  unitrrg  14514  aprcotr  14535  islmod  14565  lmod0vs  14595  lmodvs0  14596  lmodvsmmulgdi  14597  lmodfopne  14600  lmodvneg1  14604  lmodvsneg  14605  lmodcom  14607  lmodsubvs  14617  lmodsubdi  14618  lmodsubdir  14619  islss3  14653  lss1d  14657  sralmod  14724  rnglidlmsgrp  14771  2idlcpblrng  14797  mulgrhm  14883  psmetsym  15320  psmettri  15321  psmetge0  15322  psmetres2  15324  xmetge0  15356  xmetsym  15359  xmettri  15363  metrtri  15368  xmetres2  15370  bldisj  15392  xblss2ps  15395  xblss2  15396  xmeter  15427  xmetxp  15498  dvdsppwf1o  15983  perfect1  15992  perfectlem1  15993  perfectlem2  15994  3dom  16888