Theorem syl2anb 455

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 449	. 2 |- ((th /\ ps) -> ch)
4		syl2anb.3	. 2 |- (ta <-> ps)
5	3, 4	sylan2b 452	1 |- ((th /\ ta) -> ch)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  sylancb 473  opth2 2789  pwssun 2816  ordsucsssuc 3064  ordsucun 3072  fnun 3580  f1oun 3691  th3qlem1 4298  ener 4391  domtr 4396  undom 4418  xpdom2 4422  mapen 4471  abfii4 4538  pm54.43 4546  suc11reg 4577  kmlem9 4745  zorn 4769  mulclpi 4993  pre-axmulgt0 5262  xrltnsymt 5523  xrlttrit 5525  lt2add 5570  le2add 5571  addge0 5573  add20 5576  mulge0 5581  addgtge0t 5622  mulnzcnopr 5671  divmul24t 5739  lt2msq 5829  nn0addclt 6067  nn0ltp1let 6074  nn0subt 6108  zaddclt 6112  zmulclt 6127  zltp1let 6128  qaddclt 6207  qmulclt 6209  rpaddclt 6227  rpmulclt 6228  rpdivclt 6229  nnwo 6390  cvganz 6861  bccl2t 6909  isumnn0nn 7142  xpnnen 7441  znnen 7445  subbas 7586  tgioolem 7853  ablsn 8062  ablmul 8068  ringsn 8100  pslem 8573  efif1lem7 8651  hsn0elch 9041  projlem4 9105  5oalem6 9521  hmopidmch 9990  superpos 10189  ghomsn 10293  infi1 10347  ficli 10368  oefil2 10441  filintf 10443  fgsb 10444  fgsb2 10449

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