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  6106  caovcand  6109  caovordid  6113  caovordd  6115  caovdid  6122  caovdird  6125  swoer  6648  swoord1  6649  swoord2  6650  fimax2gtrilemstep  6997  iunfidisj  7048  ssfii  7076  suplub2ti  7103  prarloclem3  7610  fzosubel3  10325  seq3split  10633  seqsplitg  10634  seq3caopr  10640  seqcaoprg  10641  zsumdc  11695  fsumiun  11788  divalglemex  12233  pcgcd1  12651  strle1g  12938  prdssgrpd  13247  mnd32g  13259  mnd12g  13260  mnd4g  13261  ismndd  13269  mndinvmod  13277  prdsmndd  13280  imasmnd  13285  grpassd  13344  grpasscan2  13396  grpidrcan  13397  grpidlcan  13398  grpinvinv  13399  grplmulf1o  13406  grpinvssd  13409  grpinvadd  13410  grpsubrcan  13413  grpsubadd  13420  grpaddsubass  13422  grppncan  13423  grpsubsub4  13425  grppnpcan2  13426  grpnpncan  13427  grpnpncan0  13428  grpnnncan2  13429  dfgrp3mlem  13430  dfgrp3m  13431  grplactcnv  13434  imasgrp  13447  mhmmnd  13452  mulgaddcomlem  13481  mulgaddcom  13482  mulgnn0dir  13488  mulgdirlem  13489  mulgneg2  13492  mulgnnass  13493  mulgnn0ass  13494  mulgass  13495  mulgmodid  13497  nsgconj  13542  isnsg3  13543  nmzsubg  13546  ssnmz  13547  eqger  13560  eqgcpbl  13564  conjghm  13612  conjnmz  13615  conjnmzb  13616  abl32  13643  abladdsub4  13650  abladdsub  13651  ablpncan2  13652  ablsubsub  13654  rngass  13701  rnglz  13707  rngrz  13708  rngmneg1  13709  rngmneg2  13710  rngsubdi  13713  rngsubdir  13714  imasrng  13718  srgass  13733  srgmulgass  13751  srgpcomp  13752  srgpcompp  13753  srgpcomppsc  13754  ringass  13778  ringadd2  13789  ringo2times  13790  ringcom  13793  ringlz  13805  ringrz  13806  ringnegl  13813  ringnegr  13814  ringmneg1  13815  ringmneg2  13816  ringsubdi  13818  ringsubdir  13819  mulgass2  13820  imasring  13826  opprrng  13839  opprring  13841  mulgass3  13847  dvdsrtr  13863  dvdsrmul1  13864  unitgrp  13878  dvrass  13901  dvrcan1  13902  dvrcan3  13903  dvrdir  13905  rdivmuldivd  13906  rhmunitinv  13940  lringuplu  13958  subrginv  13999  unitrrg  14029  aprcotr  14047  islmod  14053  lmod0vs  14083  lmodvs0  14084  lmodvsmmulgdi  14085  lmodfopne  14088  lmodvneg1  14092  lmodvsneg  14093  lmodcom  14095  lmodsubvs  14105  lmodsubdi  14106  lmodsubdir  14107  islss3  14141  lss1d  14145  sralmod  14212  rnglidlmsgrp  14259  2idlcpblrng  14285  mulgrhm  14371  psmetsym  14801  psmettri  14802  psmetge0  14803  psmetres2  14805  xmetge0  14837  xmetsym  14840  xmettri  14844  metrtri  14849  xmetres2  14851  bldisj  14873  xblss2ps  14876  xblss2  14877  xmeter  14908  xmetxp  14979  dvdsppwf1o  15461  perfect1  15470  perfectlem1  15471  perfectlem2  15472