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 2800  pwssun 2827  ordsucsssuc 3074  ordsucun 3082  fnun 3594  f1oun 3706  th3qlem1 4314  ener 4410  domtr 4415  undom 4438  xpdom2 4442  mapen 4491  abfii4OLD 4564  pm54.43 4572  suc11reg 4605  kmlem9 4773  zorn 4797  mulclpi 5021  pre-axmulgt0 5290  xrltnsymt 5550  xrlttrit 5552  lt2add 5596  le2add 5597  addge0 5599  add20 5602  mulge0 5607  addgtge0t 5649  mulnzcnopr 5702  divmul24t 5783  lt2msq 5881  nn0addclt 6120  nn0ltp1let 6127  nn0subt 6161  zaddclt 6165  zmulclt 6180  zltp1let 6181  qaddclt 6269  qmulclt 6271  rpaddclt 6290  rpmulclt 6291  rpdivclt 6292  nnwo 6458  cvganz 6924  bccl2t 6971  isumnn0nn 7207  xpnnen 7499  subbasOLD 7644  tgioolem 7914  ablsn 8125  ablmul 8131  ringsn 8163  pslem 8647  efif1lem7 8736  hsn0elch 9120  projlem4 9189  5oalem6 9604  hmopidmch 10079  superpos 10281  ghomsn 10388  infi1 10447  infi1OLD 10448  ficli 10472  ficliOLD 10473  oefil2 10567  filintf 10569  fgsb 10570  fgsbOLD 10571  fgsb2 10580  rcfpfillem4 10591  rcfpfillem4OLD 10592

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