Theorem sylanbrc 421

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

Hypotheses

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

Assertion

Ref	Expression
sylanbrc	|- ( ph -> th )

Proof of Theorem sylanbrc

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  dcand  945  ecase2d  1392  sb2  1820  sbequ1  1821  sbidm  1904  eqeu  2996  euind  3013  reuind  3031  eldifd  3230  eqssd  3265  ssrabdv  3327  elind  3414  dcun  3637  opm  4374  issod  4464  ordsucim  4647  onintonm  4664  ordtri2or2exmidlem  4673  en2lp  4701  ordwe  4723  sosng  4848  sotri2  5185  sotri3  5186  relssdmrn  5308  funun  5422  fnsng  5428  fnprg  5436  fntpg  5437  fntp  5438  fununi  5449  imain  5463  fnco  5491  f00  5584  f1ss  5604  f1ssr  5605  f1ssres  5607  f1f1orn  5650  foimacnv  5657  foun  5658  fun11iun  5660  sefvex  5716  dff3im  5853  fmpt  5858  ffnfv  5866  fmpt2d  5870  ffvresb  5871  fprg  5898  foco2  5959  fcof1  5989  fcofo  5990  fcof1o  5995  fliftf  6005  isoini2  6025  f1oiso  6032  moriotass  6069  fnoprabg  6189  f1ocnvd  6292  f1o3d  6298  suppssov1  6299  1stcof  6397  2ndcof  6398  1stconst  6457  2ndconst  6458  fo2ndf  6463  f1o2ndf1  6464  f1od2  6471  suppssfvg  6503  smores2  6565  tfrlem5  6585  tfrlemibfn  6599  tfr1onlembfn  6615  tfri1dALT  6622  tfrcllembfn  6628  nntri2  6767  eroveu  6900  elixpsn  7017  dom2lem  7058  xpf1o  7144  fidifsnen  7172  finexdc  7207  elssdc  7209  unfidisj  7229  f1finf1o  7264  fidcenumlemrks  7270  sbthlemi9  7282  supeuti  7334  infeuti  7369  casef1  7430  caseinl  7431  caseinr  7432  difinfsnlem  7439  ctmlemr  7448  ctm  7449  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  enumctlemm  7454  nnnninf  7466  nninfwlpoimlemg  7515  en2other2  7548  exmidfodomrlemim  7553  pw1if  7584  pw1nel3  7590  dftap2  7617  cc2lem  7632  cc4f  7635  addclpi  7694  mulclpi  7695  nnppipi  7710  recmulnqg  7758  enq0ref  7800  nqnq0pi  7805  genipv  7876  addclpr  7904  nqprxx  7913  prmuloc  7933  mulclpr  7939  distrlem1prl  7949  distrlem1pru  7950  ltexprlempr  7975  ltexprlemrl  7977  ltexprlemru  7979  lteupri  7984  recexprlempr  7999  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemloc  8019  cauappcvgprlemcl  8020  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlem2  8027  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlem2  8047  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemupu  8067  caucvgprprlemloc  8070  caucvgprprlemcl  8071  caucvgprprlem2  8077  suplocexprlemex  8089  suplocsrlem  8175  elrealeu  8196  rereceu  8256  axpre-suploclemres  8268  negf1o  8709  aptap  8978  receuap  8999  divvalap  9004  cju  9291  nn0ge2m1nn  9627  nnnegz  9647  elnnz  9654  elnn0z  9657  peano2z  9680  nn0n0n1ge2  9715  msqznn  9746  eluzaddi  9949  eluzsubi  9950  uzind4  9988  supinfneg  9995  infsupneg  9996  elnn1uz2  10007  uz2mulcl  10008  divfnzn  10021  nnrp  10064  rpaddcl  10078  rpmulcl  10079  rpdivcl  10080  rpgecl  10083  ge0p1rp  10086  elrpd  10094  ge0addcl  10383  ge0mulcl  10384  ge0xaddcl  10385  icoshftf1o  10393  peano2fzr  10441  uzsubsubfz  10452  fzsplit2  10455  fzsplit3  10458  elfznn  10460  fzss1  10469  fzss2  10470  fzp1elp1  10482  elfz1b  10497  elfz0fzfz0  10533  fz0fzelfz0  10534  difelfznle  10542  elfzofz  10570  nn0p1elfzo  10594  fzosplitsnm1  10627  ubmelm1fzo  10644  fzofzp1b  10646  fzosplitsn  10651  zsupcllemstep  10662  zsupcl  10664  infssfzcldc  10669  infssfzledc  10670  exbtwnz  10685  flqge0nn0  10728  flqge1nn  10729  zmodcl  10781  modqmuladdnn0  10805  modsumfzodifsn  10833  frec2uzf1od  10843  frec2uzisod  10844  frecuzrdgrrn  10845  frec2uzrdg  10846  frecuzrdgrcl  10847  frecuzrdgtcl  10849  frecuzrdgsuc  10851  frecuzrdgrclt  10852  frecuzrdgfunlem  10856  frecuzrdgtclt  10858  frecuzrdgsuctlem  10860  uzennn  10873  seq3fveq2  10912  seqfveq2g  10914  monoord  10922  iseqf1olemqcl  10936  iseqf1olemnab  10938  iseqf1olemab  10939  iseqf1olemqf1o  10943  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seq3id2  10963  exp3val  10978  expcl2lemap  10988  expclzaplem  11000  expge0  11012  expge1  11013  zsqcl2  11054  bcval4  11190  bcn1  11196  bccl2  11206  hashennnuni  11218  hashunlem  11244  hashdifpr  11261  zfz1isolem1  11292  seq3coll  11294  iswrdiz  11311  ccatsymb  11370  ccatrn  11377  ccat2s1fvwd  11415  swrds1  11440  swrdccat2  11443  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12lem3  11504  pfxccatin12  11505  pfxccat3  11506  pfxccat3a  11510  shftfn  11589  shftf  11595  recvguniq  11761  resqrexlemdecn  11778  rersqreu  11794  nn0abscl  11851  nnabscl  11866  abs2dif  11872  nn0maxcl  11991  climuni  12059  2clim  12067  climcn2  12075  summodclem2a  12148  fsum3  12154  fsum3cvg3  12163  fsumcl2lem  12165  fsumadd  12173  fisum0diag2  12214  fsummulc2  12215  fsumge0  12226  geolim2  12279  cvgratnnlemabsle  12294  cvgratz  12299  mertenslemi1  12302  prodmodclem3  12342  prodmodclem2a  12343  fprodeq0  12384  fprodge0  12404  eff2  12447  tanvalap  12475  zdvdsdc  12579  fzo0dvdseq  12624  oexpneg  12644  oddge22np1  12648  evennn02n  12649  evennn2n  12650  nno  12673  divalglemeunn  12688  divalglemex  12689  divalglemeuneg  12690  divalg  12691  bitsfzolem  12721  bitsinv1lem  12728  divgcdz  12748  bezoutlemmain  12775  bezoutlemmo  12783  bezoutlemeu  12784  bezoutlemle  12785  sqgcd  12806  uzwodc  12814  nninfctlemfo  12817  eucalgval2  12831  eucalglt  12835  lcmneg  12852  lcmgcdlem  12855  ncoprmgcdne1b  12867  prmind2  12898  prmdc  12908  sqnprm  12914  isprm5lem  12919  isprm5  12920  isprm6  12925  sqrt2irrlem  12939  pw2dvdseu  12946  sqpweven  12953  2sqpwodd  12954  sqrt2irrap  12958  qgt0numnn  12977  phicl2  12992  crth  13002  phimullem  13003  eulerthlem1  13005  eulerthlemh  13009  eulerthlemth  13010  hashgcdlem  13016  oddprm  13038  pythagtriplem6  13049  pythagtriplem11  13053  pythagtriplem13  13055  pythagtriplem19  13061  pclem0  13065  pcpremul  13072  pceu  13074  pc2dvds  13109  difsqpwdvds  13117  pcadd  13119  pockthlem  13135  pockthg  13136  1arith  13146  4sqlemffi  13175  4sqlem11  13180  4sqlem12  13181  4sqlem13m  13182  4sqlem14  13183  4sqlem17  13186  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemrc  13274  ballotfilemth  13281  oddennn  13283  evenennn  13284  ennnfoneleminc  13302  ennnfonelemf1  13309  ennnfonelemen  13312  exmidunben  13317  ctinf  13321  ctiunctlemfo  13330  nninfdclemlt  13342  nninfdclemf1  13343  ptex  13618  imasaddfnlemg  13635  imasaddflemg  13637  mgmsscl  13681  sgrp0  13725  sgrp1  13726  hashfinmndnn  13745  ismndd  13750  mndpfo  13751  mhmf1o  13777  0mhm  13793  resmhm  13794  resmhm2  13795  resmhm2b  13796  mhmco  13797  gsumvallem2  13800  isgrpd2e  13825  grpinvf1o  13875  grpinvnzcl  13877  dfgrp3m  13904  mhmmnd  13919  ghmgrp  13921  mulgval  13925  mulgfng  13927  subgmulg  13991  issubg4m  13996  isnsg3  14010  nmzsubg  14013  ssnmz  14014  0nsg  14017  nsgid  14018  ghmnsgima  14071  ghmnsgpreima  14072  ghmf1  14076  kerf1ghm  14077  ghmf1o  14078  conjnmzb  14083  isabld  14102  cmnsubm  14112  ghmcmn  14131  ghmabl  14132  invghm  14133  gsumvalfi  14152  srgfcl  14277  srglmhm  14297  srgrmhm  14298  iscrngd  14347  ringsrg  14352  unitabl  14424  rhmf1o  14475  rhmco  14481  ringelnzr  14494  subrngringnsg  14513  subrgcrng  14533  subrgnzr  14550  resrhm  14556  unitrrg  14576  aprnzr  14599  aprlring  14600  drngnzr  14619  lssneln0  14711  rnglidlmsgrp  14834  quscrng  14870  expghmap  14942  mulgghm2  14943  znf1o  14986  znidom  14992  znidomb  14993  isassad  15011  psrbaglesuppg  15057  psrbagcon  15062  tgtopon  15167  distopon  15188  epttop  15191  resttopon  15272  resttopon2  15279  cnco  15322  lmss  15347  txtopon  15363  uptx  15375  txdis1cn  15379  hmeocnv  15408  hmeof1o2  15409  hmeores  15416  hmeoco  15417  idhmeo  15418  txhmeo  15420  txswaphmeo  15422  psmetxrge0  15433  isxmet2d  15449  metres2  15482  xmetresbl  15541  comet  15600  bdxmet  15602  bdmet  15603  tgioo  15655  mulc1cncf  15690  mulcncflem  15708  cnrehmeocntop  15711  cnopnap  15712  dedekindeu  15724  dedekindicclemicc  15733  ivthinclemlm  15735  ivthinclemum  15736  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemloc  15742  ivthinc  15744  ivthreinc  15746  dvfgg  15789  dvcjbr  15809  dvcj  15810  dvfre  15811  elplyr  15841  plyreres  15865  rplogbval  16047  sgmnncl  16102  mpodvdsmulf1o  16104  mersenne  16111  perfectlem2  16114  lgsfcl2  16125  lgsval2lem  16129  lgsmod  16145  lgsdirprm  16153  lgsne0  16157  gausslemma2dlem0h  16175  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  gausslemma2dlem4  16183  lgseisenlem1  16189  lgseisenlem2  16190  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem2  16201  2sqlem8  16242  2sqlem9  16243  structiedg0val  16281  ausgrumgrien  16411  usgredgreu  16457  uspgredg2vtxeu  16459  uspgredg2v  16462  usgredg2v  16465  usgr1e  16482  subuhgr  16513  subupgr  16514  subumgr  16515  subusgr  16516  vdegp1aid  16555  trlres  16631  clwwlkbp  16636  clwwlkccatlem  16641  s2elclwwlknon2  16677  clwwlknonex2lem2  16679  clwwlknonex2e  16681  bj-charfundcALT  16835  bj-nnord  16984  bj-inf2vnlem1  16996  pwf1oexmid  17029  nnsf  17048  nninfall  17052  nninfself  17056  exmidsbthrlem  17067  qdencn  17072  alsd  17131  ralsd  17132  alseud  17167  ralseud  17168