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 1460  eqtr3t 1491  psssstr 2148  reuss2 2271  reupick 2275  opabss 2663  poirr 2840  reuuni1 2877  fr2nr 2920  fr3nr 2921  wefrc 2938  fnfco 3633  fvopab2 3782  fnressn 3828  iinon 3901  tfrlem2 3903  oeordi 4204  oeordsuc 4211  oelim2 4212  omsmolem 4246  erref 4265  mapdom2 4480  mapunen 4488  ssnn 4520  fiint 4540  iunfi 4549  supmo 4556  inf3lem5 4597  r1pwcl 4667  aceq5lem4 4718  uniimadomf 4791  addclpi 5000  addnidpi 5008  recexsr 5196  xrlttrt 5534  addgt0 5580  divdivdivt 5749  infmrcl 6024  xrub 6035  uzind3 6163  uzind3OLD 6165  qbtwnxr 6225  uzind4 6390  infmssuzcl 6406  fsequb 6463  expcllem 6515  expge1t 6532  expword2it 6544  leabst 6807  faclbnd4lem3 6895  faclbnd4 6897  fsumcom 6974  clmnns 7030  clmi2rp 7034  climaddlem1 7058  climmullem6 7069  isummulc1ALT 7156  isummulc1a 7157  ruclem26 7486  blssioo 7865  lmcvgnns 7895  grpidinvlem3 8000  abl23 8055  ablmuldiv 8059  abldivdiv 8060  abldiv23 8062  nvadd12 8194  nvscom 8202  nvsubsub23 8234  ipassr 8450  minveclem30 8518  hsn0elch 9059  nmopunt 9877  branmfnt 9976  hmopidmch 10017  mdslj1 10183  mdslj2 10184  atss 10210  chcv1t 10219  dmdbr5at 10284  ltsubpostb 10507  ltaddpos2tb 10508

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