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  8710  aptap  8980  receuap  9001  divvalap  9006  cju  9293  nn0ge2m1nn  9631  nnnegz  9651  elnnz  9658  elnn0z  9661  peano2z  9684  nn0n0n1ge2  9719  msqznn  9750  eluzaddi  9958  eluzsubi  9959  uzind4  9997  supinfneg  10004  infsupneg  10005  elnn1uz2  10016  uz2mulcl  10017  divfnzn  10030  nnrp  10074  rpaddcl  10088  rpmulcl  10089  rpdivcl  10090  rpgecl  10093  ge0p1rp  10096  elrpd  10104  ge0addcl  10393  ge0mulcl  10394  ge0xaddcl  10395  icoshftf1o  10403  peano2fzr  10451  uzsubsubfz  10462  fzsplit2  10465  fzsplit3  10468  elfznn  10470  fzss1  10479  fzss2  10480  fzp1elp1  10492  elfz1b  10507  elfz0fzfz0  10543  fz0fzelfz0  10544  difelfznle  10552  elfzofz  10580  nn0p1elfzo  10604  fzosplitsnm1  10637  ubmelm1fzo  10654  fzofzp1b  10656  fzosplitsn  10661  zsupcllemstep  10672  zsupcl  10674  infssfzcldc  10679  infssfzledc  10680  exbtwnz  10695  flqge0nn0  10741  flqge1nn  10742  zmodcl  10794  modqmuladdnn0  10818  modsumfzodifsn  10846  frec2uzf1od  10856  frec2uzisod  10857  frecuzrdgrrn  10858  frec2uzrdg  10859  frecuzrdgrcl  10860  frecuzrdgtcl  10862  frecuzrdgsuc  10864  frecuzrdgrclt  10865  frecuzrdgfunlem  10869  frecuzrdgtclt  10871  frecuzrdgsuctlem  10873  uzennn  10886  seq3fveq2  10925  seqfveq2g  10927  monoord  10935  iseqf1olemqcl  10949  iseqf1olemnab  10951  iseqf1olemab  10952  iseqf1olemqf1o  10956  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3id2  10976  exp3val  10991  expcl2lemap  11001  expclzaplem  11013  expge0  11025  expge1  11026  zsqcl2  11067  bcval4  11204  bcn1  11210  bccl2  11220  hashennnuni  11232  hashunlem  11258  hashdifpr  11275  zfz1isolem1  11306  seq3coll  11308  iswrdiz  11325  ccatsymb  11384  ccatrn  11391  ccat2s1fvwd  11429  swrds1  11454  swrdccat2  11457  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12lem3  11518  pfxccatin12  11519  pfxccat3  11520  pfxccat3a  11524  shftfn  11603  shftf  11609  recvguniq  11775  resqrexlemdecn  11792  rersqreu  11808  nn0abscl  11866  nnabscl  11881  abs2dif  11887  nn0maxcl  12006  climuni  12075  2clim  12083  climcn2  12091  summodclem2a  12164  fsum3  12170  fsum3cvg3  12179  fsumcl2lem  12181  fsumadd  12189  fisum0diag2  12230  fsummulc2  12231  fsumge0  12242  geolim2  12295  cvgratnnlemabsle  12310  cvgratz  12315  mertenslemi1  12318  prodmodclem3  12358  prodmodclem2a  12359  fprodeq0  12400  fprodge0  12420  eff2  12463  tanvalap  12491  zdvdsdc  12595  fzo0dvdseq  12640  oexpneg  12660  oddge22np1  12664  evennn02n  12665  evennn2n  12666  nno  12689  divalglemeunn  12704  divalglemex  12705  divalglemeuneg  12706  divalg  12707  bitsfzolem  12737  bitsinv1lem  12744  divgcdz  12764  bezoutlemmain  12791  bezoutlemmo  12799  bezoutlemeu  12800  bezoutlemle  12801  sqgcd  12822  uzwodc  12830  nninfctlemfo  12833  eucalgval2  12847  eucalglt  12851  lcmneg  12868  lcmgcdlem  12871  ncoprmgcdne1b  12883  prmind2  12914  prmdc  12924  sqnprm  12931  isprm5lem  12936  isprm5  12937  isprm6  12942  sqrt2irrlem  12956  pwbdvdseu  12963  sqpweven  12971  2sqpwodd  12972  sqrt2irrap  12976  qgt0numnn  12995  nn0sqdcq  13004  phicl2  13012  crth  13022  phimullem  13023  eulerthlem1  13025  eulerthlemh  13029  eulerthlemth  13030  hashgcdlem  13036  oddprm  13058  pythagtriplem6  13069  pythagtriplem11  13073  pythagtriplem13  13075  pythagtriplem19  13081  pclem0  13085  pcpremul  13092  pceu  13094  pc2dvds  13129  difsqpwdvds  13137  pcadd  13139  pockthlem  13155  pockthg  13156  1arith  13166  4sqlemffi  13195  4sqlem11  13200  4sqlem12  13201  4sqlem13m  13202  4sqlem14  13203  4sqlem17  13206  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemrc  13323  ballotfilemth  13330  oddennn  13332  evenennn  13333  ennnfoneleminc  13351  ennnfonelemf1  13358  ennnfonelemen  13361  exmidunben  13366  ctinf  13370  ctiunctlemfo  13379  nninfdclemlt  13391  nninfdclemf1  13392  ptex  13667  imasaddfnlemg  13684  imasaddflemg  13686  mgmsscl  13730  sgrp0  13774  sgrp1  13775  hashfinmndnn  13794  ismndd  13799  mndpfo  13800  mhmf1o  13826  0mhm  13842  resmhm  13843  resmhm2  13844  resmhm2b  13845  mhmco  13846  gsumvallem2  13849  isgrpd2e  13874  grpinvf1o  13924  grpinvnzcl  13926  dfgrp3m  13953  mhmmnd  13968  ghmgrp  13970  mulgval  13974  mulgfng  13976  subgmulg  14040  issubg4m  14045  isnsg3  14059  nmzsubg  14062  ssnmz  14063  0nsg  14066  nsgid  14067  ghmnsgima  14120  ghmnsgpreima  14121  ghmf1  14125  kerf1ghm  14126  ghmf1o  14127  conjnmzb  14132  isabld  14151  cmnsubm  14161  ghmcmn  14180  ghmabl  14181  invghm  14182  gsumvalfi  14201  srgfcl  14326  srglmhm  14346  srgrmhm  14347  iscrngd  14396  ringsrg  14401  unitabl  14473  rhmf1o  14524  rhmco  14530  ringelnzr  14543  subrngringnsg  14562  subrgcrng  14582  subrgnzr  14599  resrhm  14605  unitrrg  14625  aprnzr  14648  aprlring  14649  drngnzr  14668  lssneln0  14760  rnglidlmsgrp  14883  quscrng  14919  expghmap  14991  mulgghm2  14992  znf1o  15035  znidom  15041  znidomb  15042  isassad  15060  psrbaglesuppg  15106  psrbagcon  15111  tgtopon  15216  distopon  15237  epttop  15240  resttopon  15321  resttopon2  15328  cnco  15371  lmss  15396  txtopon  15412  uptx  15424  txdis1cn  15428  hmeocnv  15457  hmeof1o2  15458  hmeores  15465  hmeoco  15466  idhmeo  15467  txhmeo  15469  txswaphmeo  15471  psmetxrge0  15482  isxmet2d  15498  metres2  15531  xmetresbl  15590  comet  15649  bdxmet  15651  bdmet  15652  tgioo  15704  mulc1cncf  15739  mulcncflem  15757  cnrehmeocntop  15760  cnopnap  15761  dedekindeu  15773  dedekindicclemicc  15782  ivthinclemlm  15784  ivthinclemum  15785  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemloc  15791  ivthinc  15793  ivthreinc  15795  dvfgg  15838  dvcjbr  15858  dvcj  15859  dvfre  15860  elplyr  15890  plyreres  15914  rplogbval  16100  ppiqsval  16156  ppiqsval2  16157  ppiqfi  16158  sgmnncl  16169  ppidif  16175  ppiqnncl  16181  mpodvdsmulf1o  16185  mersenne  16195  perfectlem2  16198  bcmono  16202  bposlem1  16209  bposlem3  16211  bposlem4  16212  bposlem5  16213  lgsfcl2  16223  lgsval2lem  16227  lgsmod  16243  lgsdirprm  16251  lgsne0  16255  gausslemma2dlem0h  16273  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  gausslemma2dlem4  16281  lgseisenlem1  16287  lgseisenlem2  16288  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem2  16299  2sqlem8  16340  2sqlem9  16341  structiedg0val  16379  ausgrumgrien  16509  usgredgreu  16555  uspgredg2vtxeu  16557  uspgredg2v  16560  usgredg2v  16563  usgr1e  16580  subuhgr  16611  subupgr  16612  subumgr  16613  subusgr  16614  vdegp1aid  16653  trlres  16729  clwwlkbp  16734  clwwlkccatlem  16739  s2elclwwlknon2  16775  clwwlknonex2lem2  16777  clwwlknonex2e  16779  bj-charfundcALT  16933  bj-nnord  17082  bj-inf2vnlem1  17094  pwf1oexmid  17127  nnsf  17146  nninfall  17150  nninfself  17154  exmidsbthrlem  17165  qdencn  17170  alsd  17229  ralsd  17230  alseud  17265  ralseud  17266