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 5804  recrecltt 5850  supxrun 6032  gtndivt 6140  ser1add2 6275  ser1add 6276  expord2t 6535  recjt 6753  absrelet 6804  absimlet 6805  facwordit 6881  climmullem1 7056  climmullem3 7058  climcmpc1 7075  climcau 7092  isum1p 7141  geoisumr 7178  cvgratlem5 7189  efcltlem1 7246  erelem3 7263  efaddlem5 7284  efaddlem17 7296  ef1tllem 7323  effsumle 7338  eflegeolem1 7353  efcn 7363  acdc2lem2 7431  acdc5lem2 7434  metxplem3 7768  blss 7793  lmle 7895  nmobndi 8370  ubthlem3 8462  htthlem10 8559  normpyct 8934  bcs2t 8970  mayete3 9590  unopnormt 9757  unoplint 9760  hmoplint 9782  nmophm 9876  branmfnt 9951  pjsspos 10011  golem1 10108  mdslmd4 10168

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