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  7335  infeuti  7370  casef1  7431  caseinl  7432  caseinr  7433  difinfsnlem  7440  ctmlemr  7449  ctm  7450  ctssdclemn0  7451  ctssdccl  7452  ctssdc  7454  enumctlemm  7455  nnnninf  7467  nninfwlpoimlemg  7516  en2other2  7549  exmidfodomrlemim  7554  pw1if  7585  pw1nel3  7591  dftap2  7618  cc2lem  7633  cc4f  7636  addclpi  7695  mulclpi  7696  nnppipi  7711  recmulnqg  7759  enq0ref  7801  nqnq0pi  7806  genipv  7877  addclpr  7905  nqprxx  7914  prmuloc  7934  mulclpr  7940  distrlem1prl  7950  distrlem1pru  7951  ltexprlempr  7976  ltexprlemrl  7978  ltexprlemru  7980  lteupri  7985  recexprlempr  8000  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemloc  8020  cauappcvgprlemcl  8021  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlem2  8028  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlem2  8048  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemupu  8068  caucvgprprlemloc  8071  caucvgprprlemcl  8072  caucvgprprlem2  8078  suplocexprlemex  8090  suplocsrlem  8176  elrealeu  8197  rereceu  8257  axpre-suploclemres  8269  negf1o  8711  aptap  8981  receuap  9002  divvalap  9007  cju  9294  nn0ge2m1nn  9632  nnnegz  9652  elnnz  9659  elnn0z  9662  peano2z  9685  nn0n0n1ge2  9720  msqznn  9751  eluzaddi  9959  eluzsubi  9960  uzind4  9998  supinfneg  10005  infsupneg  10006  elnn1uz2  10017  uz2mulcl  10018  divfnzn  10031  nnrp  10075  rpaddcl  10089  rpmulcl  10090  rpdivcl  10091  rpgecl  10094  ge0p1rp  10097  elrpd  10105  ge0addcl  10394  ge0mulcl  10395  ge0xaddcl  10396  icoshftf1o  10404  peano2fzr  10452  uzsubsubfz  10463  fzsplit2  10466  fzsplit3  10469  elfznn  10471  fzss1  10480  fzss2  10481  fzp1elp1  10493  elfz1b  10508  elfz0fzfz0  10544  fz0fzelfz0  10545  difelfznle  10553  elfzofz  10581  nn0p1elfzo  10605  fzosplitsnm1  10638  ubmelm1fzo  10655  fzofzp1b  10657  fzosplitsn  10662  zsupcllemstep  10673  zsupcl  10675  infssfzcldc  10680  infssfzledc  10681  exbtwnz  10696  flqge0nn0  10743  flqge1nn  10744  zmodcl  10796  modqmuladdnn0  10820  modsumfzodifsn  10848  frec2uzf1od  10858  frec2uzisod  10859  frecuzrdgrrn  10860  frec2uzrdg  10861  frecuzrdgrcl  10862  frecuzrdgtcl  10864  frecuzrdgsuc  10866  frecuzrdgrclt  10867  frecuzrdgfunlem  10871  frecuzrdgtclt  10873  frecuzrdgsuctlem  10875  uzennn  10888  seq3fveq2  10927  seqfveq2g  10929  monoord  10937  iseqf1olemqcl  10951  iseqf1olemnab  10953  iseqf1olemab  10954  iseqf1olemqf1o  10958  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3id2  10978  exp3val  10993  expcl2lemap  11003  expclzaplem  11015  expge0  11027  expge1  11028  zsqcl2  11069  bcval4  11206  bcn1  11212  bccl2  11222  hashennnuni  11234  hashunlem  11260  hashdifpr  11277  zfz1isolem1  11308  seq3coll  11310  iswrdiz  11327  ccatsymb  11386  ccatrn  11393  ccat2s1fvwd  11431  swrds1  11456  swrdccat2  11459  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12lem3  11520  pfxccatin12  11521  pfxccat3  11522  pfxccat3a  11526  shftfn  11605  shftf  11611  recvguniq  11777  resqrexlemdecn  11794  rersqreu  11810  nn0abscl  11868  nnabscl  11883  abs2dif  11889  nn0maxcl  12008  fiidxsupcl  12012  climuni  12078  2clim  12086  climcn2  12094  summodclem2a  12167  fsum3  12173  fsum3cvg3  12182  fsumcl2lem  12184  fsumadd  12192  fisum0diag2  12233  fsummulc2  12234  fsumge0  12245  geolim2  12298  cvgratnnlemabsle  12313  cvgratz  12318  mertenslemi1  12321  prodmodclem3  12361  prodmodclem2a  12362  fprodeq0  12403  fprodge0  12423  eff2  12466  tanvalap  12494  zdvdsdc  12598  fzo0dvdseq  12643  oexpneg  12663  oddge22np1  12667  evennn02n  12668  evennn2n  12669  nno  12692  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  divalg  12710  bitsfzolem  12740  bitsinv1lem  12747  divgcdz  12767  bezoutlemmain  12794  bezoutlemmo  12802  bezoutlemeu  12803  bezoutlemle  12804  sqgcd  12825  uzwodc  12833  nninfctlemfo  12836  eucalgval2  12850  eucalglt  12854  lcmneg  12871  lcmgcdlem  12874  ncoprmgcdne1b  12886  prmind2  12917  prmdc  12927  sqnprm  12934  isprm5lem  12939  isprm5  12940  isprm6  12945  sqrt2irrlem  12959  pwbdvdseu  12966  sqpweven  12974  2sqpwodd  12975  sqrt2irrap  12979  qgt0numnn  12998  nn0sqdcq  13007  phicl2  13015  crth  13025  phimullem  13026  eulerthlem1  13028  eulerthlemh  13032  eulerthlemth  13033  hashgcdlem  13039  oddprm  13061  pythagtriplem6  13072  pythagtriplem11  13076  pythagtriplem13  13078  pythagtriplem19  13084  pclem0  13088  pcpremul  13095  pceu  13097  pc2dvds  13132  difsqpwdvds  13140  pcadd  13142  pockthlem  13158  pockthg  13159  1arith  13169  4sqlemffi  13198  4sqlem11  13203  4sqlem12  13204  4sqlem13m  13205  4sqlem14  13206  4sqlem17  13209  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemrc  13326  ballotfilemth  13333  oddennn  13335  evenennn  13336  ennnfoneleminc  13354  ennnfonelemf1  13361  ennnfonelemen  13364  exmidunben  13369  ctinf  13373  ctiunctlemfo  13382  nninfdclemlt  13394  nninfdclemf1  13395  ptex  13671  imasaddfnlemg  13688  imasaddflemg  13690  mgmsscl  13734  sgrp0  13778  sgrp1  13779  hashfinmndnn  13798  ismndd  13803  mndpfo  13804  mhmf1o  13830  0mhm  13846  resmhm  13847  resmhm2  13848  resmhm2b  13849  mhmco  13850  gsumvallem2  13853  isgrpd2e  13878  grpinvf1o  13928  grpinvnzcl  13930  dfgrp3m  13957  mhmmnd  13972  ghmgrp  13974  mulgval  13978  mulgfng  13980  subgmulg  14044  issubg4m  14049  isnsg3  14063  nmzsubg  14066  ssnmz  14067  0nsg  14070  nsgid  14071  ghmnsgima  14124  ghmnsgpreima  14125  ghmf1  14129  kerf1ghm  14130  ghmf1o  14131  conjnmzb  14136  cntrsubgnsg  14169  isabld  14186  cmnsubm  14196  ghmcmn  14215  ghmabl  14216  invghm  14217  gsumvalfi  14236  srgfcl  14361  srglmhm  14381  srgrmhm  14382  iscrngd  14431  ringsrg  14436  unitabl  14508  rhmf1o  14559  rhmco  14565  ringelnzr  14578  subrngringnsg  14597  subrgcrng  14617  subrgnzr  14634  resrhm  14640  unitrrg  14660  aprnzr  14683  aprlring  14684  drngnzr  14703  lssneln0  14795  rnglidlmsgrp  14918  quscrng  14954  expghmap  15026  mulgghm2  15027  znf1o  15070  znidom  15076  znidomb  15077  isassad  15095  psrbaglesuppg  15141  psrbagcon  15146  psrbaglefifi  15147  tgtopon  15258  distopon  15279  epttop  15282  resttopon  15363  resttopon2  15370  cnco  15413  lmss  15438  txtopon  15454  uptx  15466  txdis1cn  15470  hmeocnv  15499  hmeof1o2  15500  hmeores  15507  hmeoco  15508  idhmeo  15509  txhmeo  15511  txswaphmeo  15513  psmetxrge0  15524  isxmet2d  15540  metres2  15573  xmetresbl  15632  comet  15691  bdxmet  15693  bdmet  15694  tgioo  15746  mulc1cncf  15781  mulcncflem  15799  cnrehmeocntop  15802  cnopnap  15803  dedekindeu  15815  dedekindicclemicc  15824  ivthinclemlm  15826  ivthinclemum  15827  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemloc  15833  ivthinc  15835  ivthreinc  15837  dvfgg  15880  dvcjbr  15900  dvcj  15901  dvfre  15902  elplyr  15932  plyreres  15956  rplogbval  16142  ppiqsval  16201  ppiqsval2  16202  ppiqfi  16203  sgmnncl  16218  chtdif  16225  ppidif  16230  ppiqnncl  16239  mpodvdsmulf1o  16245  mersenne  16258  perfectlem2  16261  bcmono  16265  bposlem1  16272  bposlem3  16274  bposlem4  16275  bposlem5  16276  bposlem6  16277  bposlem9  16280  lgsfcl2  16291  lgsval2lem  16295  lgsmod  16311  lgsdirprm  16319  lgsne0  16323  gausslemma2dlem0h  16341  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  gausslemma2dlem4  16349  lgseisenlem1  16355  lgseisenlem2  16356  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem2  16367  2sqlem8  16408  2sqlem9  16409  structiedg0val  16447  ausgrumgrien  16577  usgredgreu  16623  uspgredg2vtxeu  16625  uspgredg2v  16628  usgredg2v  16631  usgr1e  16648  subuhgr  16679  subupgr  16680  subumgr  16681  subusgr  16682  vdegp1aid  16721  trlres  16797  clwwlkbp  16802  clwwlkccatlem  16807  s2elclwwlknon2  16843  clwwlknonex2lem2  16845  clwwlknonex2e  16847  bj-charfundcALT  17001  bj-nnord  17150  bj-inf2vnlem1  17162  pwf1oexmid  17195  nnsf  17214  nninfall  17218  nninfself  17222  exmidsbthrlem  17233  qdencn  17238  alsd  17298  ralsd  17299  alseud  17334  ralseud  17335