Theorem syl2anb 350

Description: A double syllogism inference.

Hypotheses

Ref	Expression
sylan.1	|- ((ph /\ ps) -> ch)
syl2anb.2	|- (th <-> ph)
syl2anb.3	|- (ta <-> ps)

Assertion

Ref	Expression
syl2anb	|- ((th /\ ta ) -> ch)

Proof of Theorem syl2anb

Step	Hyp	Ref	Expression
1		sylan.1	. . 3 |- ((ph /\ ps) -> ch)
2		syl2anb.2	. . 3 |- (th <-> ph)
3	1, 2	sylanb 344	. 2 |- ((th /\ ps) -> ch)
4		syl2anb.3	. 2 |- (ta <-> ps)
5	3, 4	sylan2b 347	1 |- ((th /\ ta ) -> ch)

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  sylancb 362  opth2 1909  pwssun 1917  ordsucsssuc 2325  ordsucun 2333  fnun 2730  f1oun 2815  th3qlem1 3250  ener 3313  domtr 3320  undom 3342  xpdom2 3345  mapen 3386  suc11reg 3456  kmlem8 3587  zorn2 3612  fodomb 3615  mulclpi 3815  axmulgt0 4086  lt2add 4321  le2add 4322  addge0 4324  add20 4329  mulge0 4335  lt2sq 4414  nn0addclt 4551  nn0ltp1let 4556  nn0subt 4587  zaddclt 4590  zmulclt 4596  zltp1let 4597  qaddclt 4642  qmulclt 4644  xpnnen 4927  znnen 4930  hsn0elch 5155  projlem4 5196  5oalem6 5549

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org