Theorem sylan2b 454

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 453	1 |- ((ph /\ th) -> ch)

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

This theorem is referenced by:  syl2anb 457  bm1.1 1465  eqtr3t 1497  psssstr 2155  reuss2 2278  reupick 2282  opabss 2673  poirr 2851  reuuni1 2888  fr2nr 2931  fr3nr 2932  wefrc 2949  fnfco 3648  fvopab2 3797  fnressn 3843  iinon 3916  tfrlem2 3918  oeordi 4220  oeordsuc 4227  oelim2 4228  omsmolem 4262  erref 4281  mapdom2 4500  mapunen 4508  finsucdom 4532  ssnnfi 4545  ssnnfiOLD 4546  fiint 4572  fiintOLD 4573  supmo 4585  inf3lem5 4626  r1pwcl 4697  aceq5lem4 4748  uniimadomf 4821  addclpi 5032  addnidpi 5040  recexsr 5228  xrlttrt 5565  addgt0 5610  divdivdivt 5787  infmrcl 6071  xrub 6082  uzind3 6209  uzind3OLD 6211  qbtwnxr 6280  uzind4 6451  infmssuzcl 6467  fsequb 6524  expcllem 6576  expge1t 6594  expword2it 6606  leabst 6864  faclbnd4lem3 6950  faclbnd4 6952  fsumcom 7028  clmnns 7084  clmi2rp 7088  climaddlem1 7114  climmullem6 7125  isummulc1ALT 7213  isummulc1a 7214  ruclem26 7536  blssioo 7910  lmcvgnns 7940  grpidinvlem3 8047  abl23 8100  ablmuldiv 8103  abldivdiv 8104  abldiv23 8106  nvadd12 8238  nvscom 8246  nvsubsub23 8278  ipassr 8502  minveclem30 8570  hsn0elch 9115  nmopunt 9934  branmfnt 10033  hmopidmch 10074  mdslj1 10241  mdslj2 10242  atss 10268  chcv1t 10277  dmdbr5at 10344  ltsubpostb 10598  ltaddpos2tb 10599

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