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 2795  pwssun 2822  ordsucsssuc 3069  ordsucun 3077  fnun 3586  f1oun 3697  th3qlem1 4304  ener 4397  domtr 4402  undom 4424  xpdom2 4428  mapen 4477  abfii4 4544  pm54.43 4552  suc11reg 4585  kmlem9 4753  zorn 4777  mulclpi 5001  pre-axmulgt0 5270  xrltnsymt 5531  xrlttrit 5533  lt2add 5578  le2add 5579  addge0 5581  add20 5584  mulge0 5589  addgtge0t 5630  mulnzcnopr 5679  divmul24t 5747  lt2msq 5837  nn0addclt 6075  nn0ltp1let 6082  nn0subt 6116  zaddclt 6120  zmulclt 6135  zltp1let 6136  qaddclt 6215  qmulclt 6217  rpaddclt 6235  rpmulclt 6236  rpdivclt 6237  nnwo 6398  cvganz 6869  bccl2t 6917  isumnn0nn 7150  xpnnen 7449  znnen 7453  subbas 7594  tgioolem 7866  ablsn 8077  ablmul 8083  ringsn 8115  pslem 8590  efif1lem7 8670  hsn0elch 9059  projlem4 9128  5oalem6 9544  hmopidmch 10017  superpos 10218  ghomsn 10322  infi1 10383  ficli 10404  oefil2 10477  filintf 10479  fgsb 10480  fgsb2 10485

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