Theorem syl2anb 457

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

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221

This theorem is referenced by:  sylancb 476  opth2 2876  pwssun 2905  ordsucsssuc 3179  ordsucun 3180  fnun 3700  f1oun 3815  th3qlem1 4455  ener 4551  domtr 4556  undom 4579  xpdom2 4583  mapen 4638  abfii4 4707  pm54.43 4715  suc11reg 4750  kmlem9 4919  zorn 4943  mulclpi 5175  pre-axmulgt0 5444  xrltnsym 5704  xrlttri 5706  lt2addi 5750  le2addi 5751  addge0i 5753  add20i 5756  mulge0i 5761  addgtge0 5803  mulnzcnopr 5854  lt2msqi 6026  rpaddcl 6206  rpmulcl 6207  rpdivcl 6208  nn0addcl 6288  nn0ltp1le 6295  nn0sub 6329  zaddcl 6333  zmulcl 6348  zltp1le 6349  qaddcl 6408  qmulcl 6410  nnwo 6585  cvganz 7127  bccl2 7174  isumnn0nn 7411  xpnnen 7711  subbas 7856  tgioolem 8125  ablsn 8366  ablmul 8372  ringsn 8405  pslem 8909  efif1lem7 9008  hsn0elch 9396  projlem4 9465  5oalem6 9882  hmopidmchi 10359  superpos 10562  ghomsn 10673  infi1 10735  ficli 10756  inttr 10787  inposet 10868  oefil2 11079  filintf 11081  fgsb 11082  fgsb2 11086  rcfpfillem4 11092  supfil 11645  morex 11804  heiborlem18 12028

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 145  df-an 223

Copyright terms: Public domain