Theorem syl31anc 1253

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 )
syl31anc.5	|- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )

Assertion

Ref	Expression
syl31anc	|- ( ph -> et )

Proof of Theorem syl31anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	3jca 1180	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
5		sylXanc.4	. 2 |- ( ph -> ta )
6		syl31anc.5	. 2 |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )
7	4, 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:  syl32anc  1258  stoic4b  1453  enq0tr  7577  ltmul12a  8963  lt2msq1  8988  ledivp1  9006  lemul1ad  9042  lemul2ad  9043  lediv2ad  9871  xaddge0  10030  difelfznle  10287  expubnd  10773  nn0leexp2  10887  expcanlem  10892  expcand  10894  swrds1  11154  ccatswrd  11156  pfxfv  11170  xrmaxaddlem  11656  mertenslemi1  11931  eftlub  12086  dvdsadd  12232  3dvds  12260  divalgmod  12323  bitsfzolem  12350  bitsfzo  12351  bitsmod  12352  bitsinv1lem  12357  gcdzeq  12428  rplpwr  12433  sqgcd  12435  bezoutr  12438  rpmulgcd2  12502  rpdvds  12506  isprm5  12549  divgcdodd  12550  oddpwdclemxy  12576  divnumden  12603  crth  12631  phimullem  12632  coprimeprodsq2  12666  pythagtriplem19  12690  pclemub  12695  pcpre1  12700  pcidlem  12731  pockthlem  12764  prmunb  12770  kerf1ghm  13695  elrhmunit  14024  rrgnz  14115  znunit  14506  xblss2ps  14961  xblss2  14962  metcnpi3  15074  limcimolemlt  15221  limccnp2cntop  15234  dvmulxxbr  15259  dvcoapbr  15264  ltexp2d  15499  mpodvdsmulf1o  15547  lgsquad2lem2  15644  2lgsoddprmlem1  15667  2sqlem8a  15684  2sqlem8  15685