Theorem sylanbrc 527

Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

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

Assertion

Ref	Expression
sylanbrc	|- (th -> ph)

Proof of Theorem sylanbrc

Step	Hyp	Ref	Expression
1		sylanbrc.2	. . 3 |- (th -> ps)
2		sylanbrc.3	. . 3 |- (th -> ch)
3	1, 2	jca 310	. 2 |- (th -> (ps /\ ch))
4		sylanbrc.1	. 2 |- (ph <-> (ps /\ ch))
5	3, 4	sylibr 217	1 |- (th -> ph)

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

This theorem is referenced by:  impbid 574  ecase2d 824  ecase23d 1198  a4imed 1522  sb2 1541  sbequ1 1542  sbn 1601  euind 2439  reuind 2450  eqssd 2633  ssrabdv 2686  psstr 2714  wereu 3654  ordelord 3680  ordnbtwn 3761  reucl2 3814  eufromeq2 3829  eufromeq6 3833  dflim3OLD 3931  ordomOLD 3961  omssnlimOLD 3966  relssdmrn 4416  funun 4462  fununi 4481  fnco 4521  fnopabg 4546  fssOLD 4572  fcoOLD 4574  f00 4601  f1f1orn 4649  foimacnv 4657  dff3 4790  fopab2 4796  ffnfv 4801  fprOLD 4811  f1oiso 4881  fnoprabg 4941  1stcof 5040  1stconst 5070  2ndconst 5071  curry1 5075  curry2 5078  oalimcl 5242  omlimcl 5257  omsmo 5314  en2d 5459  dom2d 5463  fodomr 5547  riotacl2 5578  mapenlem2 5584  mapxpen 5589  php2 5608  php3 5609  ordiso 5683  ordtypelem6 5689  ordtypelem7 5690  hartoglem 5692  hartog 5693  onsdom 5694  ordelordaxr 5833  elomsubsd 5885  infenomsub 5889  fodom 5960  cardsdomel 6004  ondomcard 6009  cardmin 6012  addclpi 6172  mulclpi 6173  genpcl 6263  ltxrlt 6669  nnrp 7238  rpaddcl 7247  rpmulcl 7248  rpdivcl 7249  nnnegz 7347  elnnz 7354  elnnz1 7364  msqznn 7408  uzwo5OLD 7423  flval3 7479  flge0nn0 7482  flge1nn 7483  zmodcl 7511  eliooord 7556  eluzaddi 7605  eluzsubi 7606  uzind4 7619  elfznn 7666  elfznn0 7668  shftf 7764  rpsqrcl 7965  replim 8011  absrpcl 8106  nn0abscl 8131  abs2dif 8154  mulc1cncf 8541  efaddlem2 8601  eff2 8632  reeff1 8675  efcn 8688  infmap2lem2 8849  tgcl 8894  fctop 8920  cctop 8922  dnsconst 9065  opntop 9147  tgioo 9193  lmsslem 9230  xplm 9253  xpcn 9254  lmcau 9274  cmsss 9275  grplactf1o 9406  issubg 9425  ssga 9455  gapm 9462  nvex 9562  isnv 9563  va1cnlem 9684  isblo3i 9801  sspph 9856  ipblnfi 9857  ssphl 9966  htthlem11 9977  efif 10075  efielcirc 10093  effoi 10099  resslogrn 10107  clint3 10184  uptx 10226  subtopmetlem 10255  sfvlim 10296  cncomp 10331  fintopcomp 10333  opidon 10369  mndmgmid 10389  ismnd2 10392  ocsh 10789  occli 10814  projlem10 10828  projlem29 10847  pjtheui 10868  ococin 10930  5oalem1 11234  5oalem2 11235  5oalem4 11237  5oalem5 11238  3oalem2 11243  unopf1o 11477  cnvunop 11479  unoplin 11481  counop 11482  hmopadj2 11502  hmoplin 11503  bralnfn 11509  lnopmi 11562  unopbd 11577  hmops 11582  hmopm 11583  hmopco 11585  bdophmi 11599  cnlnadjlem2 11638  adjlnop 11656  hmopidmchi 11723  hmopidmpji 11724  pjclem4 11772  pj3si 11780  strlem3a 11824  h1da 11921  shatomistici 11933  bnj214 12508  bnj599OLD 12561  bnj922 12834  bnj951 12848  bnj1153 12946  bnj1379 13100  bnj1422 13118  bnj1526 13178  bnj151 13243  bnj607 13304  bnj908 13329  bnj944 13340  bnj1004 13369  bnj1177 13445  bnj1321 13498  bnj1398 13515  nnabscl 13601  lediv2aALT 13621  ghomfo 13634  ghomf1olem 13637  divalglem5 13700  gcdcllem3 13720  dfon2 13858  wfrlem10 13966  elno2 14005  axdenselem1 14019  axdenselem6 14024  nocvxmin 14029  injrec 14461  surjsec 14462  mapmapmap 14486  injsurinj 14487  npincppr 14501  repfuntw 14502  prjmapcp 14507  unprj 14511  prjmapcp2 14515  mgmlion 14697  svli2 14826  lvsovso 15038  partarelt2 15274  carinttar 15279  cartarlim 15282  eqeu 15351  fictb 15371  ordisoOLD 15374  ordtypelem6OLD 15380  ordtypelem7OLD 15381  hartoglemOLD 15383  hartogOLD 15384  onsdomOLD 15385  elomsubsdOLD 15394  infenomsubOLD 15398  opncldf1 15402  cnsubsp 15426  compsublem 15430  compsub 15431  cptclsscpt 15432  uncomp 15433  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem4 15440  cnconn 15444  reconnlem1 15446  reconnlem3 15448  reconnlem4 15449  fnessref 15503  refssfne 15504  lfinpfin 15513  comppfsc 15517  neibastop1 15518  neibastop2lem3 15521  neibastop2lem4 15522  fnemeet2 15529  fnejoin2 15531  ist1-2 15542  neifg 15559  supfil 15560  filssufillem 15570  filssufil 15571  fixufil 15576  filcon 15580  flimcls 15588  fmfnfmlem4 15597  fmfnfm 15598  fmufil 15599  filnetlem3 15642  unirep 15664  prfunOLD 15677  prfOLD 15680  foco2 15686  enf1f1o 15720  eropreu 15733  eroprf 15735  wofi 15770  sdc 15811  geomcau 15849  metdcn 15853  lincmb01cmp 15878  cnimass 15888  sstotbnd 15936  blbnd 15943  totbndbnd 15944  heiborlem10 15964  heiborlem22 15976  heiborlem23 15977  heiborlem29 15983  heiborlem33 15987  heiborlem42 15996  rrnmet 16016  rrncms 16019  iccbnd 16026  isgrpda 16033  isablda 16035  grpkerinj 16042  phtpycolem4 16054  pcocn 16076  pcoloopf 16079  pcohtpylem3 16082  isdivrng2 16111  iscringd 16147  crnghomfo 16154  smprngpr 16200  prnc 16215  isfldidl 16216  pridlc3 16221  lubun 16899  lubunNEW 16900  divrngidNEW 17166  pmodlem1 17307

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