Theorem sylan2b 501

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	biimpi 168	. 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:  syl2anb 504  bm1.1 1870  eqtr3 1907  psssstr 2716  reuss2 2870  reupick 2874  reximdva0 2886  opabss 3397  opabssOLD 3398  poirr 3597  fr2nr 3635  wefrc 3652  reuuni1OLD 3809  fr3nr 3859  onzsl 3928  xpcan 4348  fnfco 4581  fvopab2 4754  fnressn 4812  dfoprab3s 5055  1stconst 5070  2ndconst 5071  iinon 5115  tfrlem2 5120  oeordi 5262  oeordsuc 5269  oelim2 5270  omsmolem 5313  erref 5333  ac6sfi 5509  mapdom2 5588  mapunen 5596  finsucdom 5620  ssnnfi 5629  fiint 5650  iunfi 5659  supmo 5666  hartog 5693  inf3lem5 5723  r1pwcl 5798  aceq5lem4 5900  uniimadomf 5973  nnacda 6088  addclpi 6172  addnidpi 6180  recexsr 6368  xrlttr 6728  addgt0iOLD 6776  infmrcl 7278  xrub 7289  uzind3 7419  uzind3OLD 7421  qbtwnxr 7460  uzind4 7619  infmssuzcl 7636  fsequb 7702  expcllem 7818  expne0i 7830  expge1 7835  expword2i 7850  leabs 8115  faclbnd4lem3 8202  faclbnd4 8204  fsumcom 8288  clmnnsi 8344  clmi2rpi 8348  climaddlem1 8374  climmullem6 8385  isummulc1iALT 8474  isummulc1ai 8475  explecnv 8495  ruclem26 8804  blssioo 9191  lmcvgnns 9221  grpidinvlem3 9330  abl23 9412  ablmuldiv 9415  abldivdiv 9416  abldiv23 9418  nvadd12 9574  nvscom 9582  nvsubsub23 9614  vacnlem1 9667  ipassr 9847  minveclem30 9919  indexfi 10174  elsubsp 10248  subcld 10254  fintopcomp 10333  hsn0elch 10753  nmopun 11576  branmfn 11675  branmfnOLD 11676  hmopidmchi 11723  mdslj1i 11891  mdslj2i 11892  atss 11918  chcv1 11927  dmdbr5ati 11994  bnj521 12522  bnj926 12832  bnj1120 12930  bnj1165 12957  bnj1277 13034  bnj1389 13104  bnj518 13260  bnj578 13291  bnj605 13292  bnj594 13300  bnj934 13334  bnj953 13343  bnj1174 13442  eluznn0 13661  gcdcllem1 13718  eucalgf 13751  eucalginv 13752  eucalglt 13753  axfelem14 14044  resid2 14425  toplat 14638  inttop3 14864  sallnei 14873  ltsubpostb 15005  ltaddpos2tb 15006  hartogOLD 15384  ntruni 15412  clsint2 15414  subsubtop 15423  subcls 15424  subntr 15425  cnsubsp 15426  cnsubsp2 15427  compsublem 15430  compsub 15431  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  connsub 15443  neibastop1 15518  topjoin 15527  fnejoin1 15530  fnejoin2 15531  uffixfr 15575  filcon 15580  morex 15662  eqfnun 15705  ac6gf 15749  indexfiOLD 15755  zornn0 15764  divexp 15779  fzfi2 15787  fzn0 15789  sdclem1 15809  sdc 15811  subspabs 15840  mettrifi 15847  cnimass 15888  cnres2 15890  cnss 15892  txsubsp 15912  totbndss 15937  blbnd 15943  totbndbnd 15944  ismtybndlem 15952  heiborlem23 15977  rrnmet 16016  rrndstprj1 16017  phtpycolem4 16054  phtpycolem5 16055  phtpyco 16056  pcocn 16076  pcoloopf 16079  pcohtpylem3 16082  pcohtpy 16083  pi1gp 16095  isdivrng2 16111  unichnidl 16179  isfldidl 16216  posgelem 16795  latlem12 16873  clatlat 16893  lubun 16899  lubunNEW 16900  grpidinvlem3NEW 17111  elpadd0 17270

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