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  6083  caovcand  6086  caovordid  6090  caovordd  6092  caovdid  6099  caovdird  6102  swoer  6620  swoord1  6621  swoord2  6622  fimax2gtrilemstep  6961  iunfidisj  7012  ssfii  7040  suplub2ti  7067  prarloclem3  7564  fzosubel3  10272  seq3split  10580  seqsplitg  10581  seq3caopr  10587  seqcaoprg  10588  zsumdc  11549  fsumiun  11642  divalglemex  12087  pcgcd1  12497  strle1g  12784  mnd32g  13068  mnd12g  13069  mnd4g  13070  ismndd  13078  mndinvmod  13086  grpassd  13144  grpasscan2  13196  grpidrcan  13197  grpidlcan  13198  grpinvinv  13199  grplmulf1o  13206  grpinvssd  13209  grpinvadd  13210  grpsubrcan  13213  grpsubadd  13220  grpaddsubass  13222  grppncan  13223  grpsubsub4  13225  grppnpcan2  13226  grpnpncan  13227  grpnpncan0  13228  grpnnncan2  13229  dfgrp3mlem  13230  dfgrp3m  13231  grplactcnv  13234  imasgrp  13241  mhmmnd  13246  mulgaddcomlem  13275  mulgaddcom  13276  mulgnn0dir  13282  mulgdirlem  13283  mulgneg2  13286  mulgnnass  13287  mulgnn0ass  13288  mulgass  13289  mulgmodid  13291  nsgconj  13336  isnsg3  13337  nmzsubg  13340  ssnmz  13341  eqger  13354  eqgcpbl  13358  conjghm  13406  conjnmz  13409  conjnmzb  13410  abl32  13437  abladdsub4  13444  abladdsub  13445  ablpncan2  13446  ablsubsub  13448  rngass  13495  rnglz  13501  rngrz  13502  rngmneg1  13503  rngmneg2  13504  rngsubdi  13507  rngsubdir  13508  imasrng  13512  srgass  13527  srgmulgass  13545  srgpcomp  13546  srgpcompp  13547  srgpcomppsc  13548  ringass  13572  ringadd2  13583  ringo2times  13584  ringcom  13587  ringlz  13599  ringrz  13600  ringnegl  13607  ringnegr  13608  ringmneg1  13609  ringmneg2  13610  ringsubdi  13612  ringsubdir  13613  mulgass2  13614  imasring  13620  opprrng  13633  opprring  13635  mulgass3  13641  dvdsrtr  13657  dvdsrmul1  13658  unitgrp  13672  dvrass  13695  dvrcan1  13696  dvrcan3  13697  dvrdir  13699  rdivmuldivd  13700  rhmunitinv  13734  lringuplu  13752  subrginv  13793  unitrrg  13823  aprcotr  13841  islmod  13847  lmod0vs  13877  lmodvs0  13878  lmodvsmmulgdi  13879  lmodfopne  13882  lmodvneg1  13886  lmodvsneg  13887  lmodcom  13889  lmodsubvs  13899  lmodsubdi  13900  lmodsubdir  13901  islss3  13935  lss1d  13939  sralmod  14006  rnglidlmsgrp  14053  2idlcpblrng  14079  mulgrhm  14165  psmetsym  14565  psmettri  14566  psmetge0  14567  psmetres2  14569  xmetge0  14601  xmetsym  14604  xmettri  14608  metrtri  14613  xmetres2  14615  bldisj  14637  xblss2ps  14640  xblss2  14641  xmeter  14672  xmetxp  14743  dvdsppwf1o  15225  perfect1  15234  perfectlem1  15235  perfectlem2  15236