Theorem syl2anc 472

Description: A syllogism inference combined with contraction.

Hypotheses

Ref	Expression
syl2anc.1	|- (((ph /\ ps) /\ (ch /\ th)) -> ta)
syl2anc.2	|- (et -> ph)
syl2anc.3	|- (et -> ps)
syl2anc.4	|- (et -> ch)
syl2anc.5	|- (et -> th)

Assertion

Ref	Expression
syl2anc	|- (et -> ta)

Proof of Theorem syl2anc

Step	Hyp	Ref	Expression
1		syl2anc.1	. 2 |- (((ph /\ ps) /\ (ch /\ th)) -> ta)
2		syl2anc.2	. . 3 |- (et -> ph)
3		syl2anc.3	. . 3 |- (et -> ps)
4	2, 3	jca 288	. 2 |- (et -> (ph /\ ps))
5		syl2anc.4	. . 3 |- (et -> ch)
6		syl2anc.5	. . 3 |- (et -> th)
7	5, 6	jca 288	. 2 |- (et -> (ch /\ th))
8	1, 4, 7	sylanc 471	1 |- (et -> ta)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  lemulge11t 5814  recrecltt 5860  supxrun 6042  gtndivt 6150  ser1add2 6288  ser1add 6289  expord2t 6549  recjt 6768  absrelet 6819  absimlet 6820  facwordit 6896  climmullem1 7073  climmullem3 7075  climcmpc1 7092  climcau 7109  isum1p 7158  geoisumr 7195  cvgratlem5 7206  efcltlem1 7263  erelem3 7280  efaddlem5 7301  efaddlem17 7313  ef1tllem 7340  effsumle 7355  eflegeolem1 7370  efcn 7380  acdc2lem2 7448  acdc5lem2 7451  metxplem3 7790  blss 7815  lmle 7922  nmobndi 8398  ubthlem3 8490  htthlem10 8587  normpyct 8968  bcs2t 9004  mayete3 9630  unopnormt 9798  unoplint 9801  hmoplint 9823  nmophm 9917  branmfnt 9994  pjsspos 10056  golem1 10154  mdslmd4 10216

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain