Theorem sylan2b 452

Description: A syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
sylan2b	|- ((ph /\ th) -> ch)

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan.1	. 2 |- ((ph /\ ps) -> ch)
2		sylan2b.2	. . 3 |- (th <-> ps)
3	2	biimp 151	. 2 |- (th -> ps)
4	1, 3	sylan2 451	1 |- ((ph /\ th) -> ch)

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

This theorem is referenced by:  syl2anb 455  bm1.1 1462  eqtr3t 1494  psssstr 2152  reuss2 2275  reupick 2279  opabss 2668  poirr 2845  reuuni1 2882  fr2nr 2925  fr3nr 2926  wefrc 2943  fnfco 3642  fvopab2 3791  fnressn 3837  iinon 3910  tfrlem2 3912  oeordi 4214  oeordsuc 4221  oelim2 4222  omsmolem 4256  erref 4275  mapdom2 4494  mapunen 4502  ssnnfi 4535  ssnnfiOLD 4536  fiint 4559  fiintOLD 4560  iunfiOLD 4569  supmo 4576  inf3lem5 4617  r1pwcl 4687  aceq5lem4 4738  uniimadomf 4811  addclpi 5020  addnidpi 5028  recexsr 5216  xrlttrt 5553  addgt0 5598  divdivdivt 5785  infmrcl 6069  xrub 6080  uzind3 6207  uzind3OLD 6209  qbtwnxr 6279  uzind4 6450  infmssuzcl 6466  fsequb 6523  expcllem 6575  expge1t 6593  expword2it 6605  leabst 6864  faclbnd4lem3 6950  faclbnd4 6952  fsumcom 7028  clmnns 7084  clmi2rp 7088  climaddlem1 7114  climmullem6 7125  isummulc1ALT 7213  isummulc1a 7214  ruclem26 7535  blssioo 7913  lmcvgnns 7943  grpidinvlem3 8050  abl23 8104  ablmuldiv 8107  abldivdiv 8108  abldiv23 8110  nvadd12 8242  nvscom 8250  nvsubsub23 8282  ipassr 8506  minveclem30 8574  hsn0elch 9120  nmopunt 9939  branmfnt 10038  hmopidmch 10079  mdslj1 10246  mdslj2 10247  atss 10273  chcv1t 10282  dmdbr5at 10349  ltsubpostb 10627  ltaddpos2tb 10628

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