Theorem sylan2br 502

Description: A syllogism inference.

Hypotheses

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

Assertion

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

Proof of Theorem sylan2br

Step	Hyp	Ref	Expression
1		sylan.1	. 2 |- ((ph /\ ps) -> ch)
2		sylan2br.2	. . 3 |- (ps <-> th)
3	2	biimpri 169	. 2 |- (th -> ps)
4	1, 3	sylan2 500	1 |- ((ph /\ th) -> ch)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240

This theorem is referenced by:  syl2anbr 505  pm2.61neOLD 2088  tfindsg2 3945  nn0suc 3976  imainss 4331  xpexr2 4353  imadif 4493  fnop 4516  ssimaex 4729  tfrlem2 5120  tz7.48-2 5166  xpfi 5632  rankxplim3 5825  aceq5 5902  ac6lem 5916  zorn2lem7 5956  suppsr 6374  supsrlem6 6382  supre 6412  xrltnsym 6725  xrsupsslem 7285  xrinfmsslem 7286  uzind3 7419  uzind3OLD 7421  bcval4 8213  clm3i 8339  climconst2 8355  cvgratlem3ALT 8511  cvgratlem3 8514  ef0lem 8572  elcls 8980  neiint 8995  neips 9003  cnconst 9057  bopcnlem2 9260  vacnlem5 9671  sqcn 9674  minveclem31 9920  fbunfip 10282  hausfillim 10303  cncomp 10331  hiidge0 10597  normgt0OLD 10626  hommval 11145  hfmmval 11148  nmcoplbi 11595  nmophmi 11598  nmbdfnlbi 11615  nmcfnlbi 11624  mdslmd1i 11901  mdslmd3i 11904  sumdmdlem2 11991  bnj955 12851  nn0seqcvgd 13659  gcdcllem3 13720  gcd0id 13729  mulgcdlem2 13757  wfr3g 13956  tfr3ALT 13979  fordisxex 14291  fiiu 14344  preodom2 14567  preoran2 14571  opnbnd 15409  opnnei 15417  pofun 15772  tlmconst 15907  totbndss 15937  heiborlem11 15965  heiborlem13 15967  heiborlem23 15977  heiborlem32 15986  bfplem8 16005  rrntotbnd 16022  abl4pnp 16037  phtpycolem5 16055  pi1val 16094  pi1gp 16095  iscringd 16147  crngm4 16151  igenval 16209  smores2 16447  smoge 16454  grpclNEW 17106  ringclNEW 17144  pmodlem2 17308  polval 17318

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 164  df-an 242

Copyright terms: Public domain