Theorem sylanbrc 417

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 )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sb2  1767  sbequ1  1768  sbidm  1851  eqeu  2907  euind  2924  reuind  2942  eldifd  3139  eqssd  3172  ssrabdv  3234  elind  3320  dcun  3533  opm  4232  issod  4317  ordsucim  4497  onintonm  4514  ordtri2or2exmidlem  4523  en2lp  4551  ordwe  4573  sosng  4697  sotri2  5023  sotri3  5024  relssdmrn  5146  funun  5257  fnsng  5260  fnprg  5268  fntpg  5269  fntp  5270  fununi  5281  imain  5295  fnco  5321  f00  5404  f1ss  5424  f1ssr  5425  f1ssres  5427  f1f1orn  5469  foimacnv  5476  foun  5477  fun11iun  5479  sefvex  5533  dff3im  5658  fmpt  5663  ffnfv  5671  fmpt2d  5675  ffvresb  5676  fprg  5696  foco2  5750  fcof1  5779  fcofo  5780  fcof1o  5785  fliftf  5795  isoini2  5815  f1oiso  5822  moriotass  5854  fnoprabg  5971  f1ocnvd  6068  suppssfv  6074  suppssov1  6075  1stcof  6159  2ndcof  6160  1stconst  6217  2ndconst  6218  fo2ndf  6223  f1o2ndf1  6224  f1od2  6231  smores2  6290  tfrlem5  6310  tfrlemibfn  6324  tfr1onlembfn  6340  tfri1dALT  6347  tfrcllembfn  6353  nntri2  6490  eroveu  6621  elixpsn  6730  dom2lem  6767  xpf1o  6839  fidifsnen  6865  finexdc  6897  unfidisj  6916  f1finf1o  6941  fidcenumlemrks  6947  sbthlemi9  6959  supeuti  6988  infeuti  7023  casef1  7084  caseinl  7085  caseinr  7086  difinfsnlem  7093  ctmlemr  7102  ctm  7103  ctssdclemn0  7104  ctssdccl  7105  ctssdc  7107  enumctlemm  7108  nnnninf  7119  nninfwlpoimlemg  7168  en2other2  7190  exmidfodomrlemim  7195  pw1nel3  7225  dftap2  7245  cc2lem  7260  cc4f  7263  addclpi  7321  mulclpi  7322  nnppipi  7337  recmulnqg  7385  enq0ref  7427  nqnq0pi  7432  genipv  7503  addclpr  7531  nqprxx  7540  prmuloc  7560  mulclpr  7566  distrlem1prl  7576  distrlem1pru  7577  ltexprlempr  7602  ltexprlemrl  7604  ltexprlemru  7606  lteupri  7611  recexprlempr  7626  cauappcvgprlemm  7639  cauappcvgprlemopl  7640  cauappcvgprlemlol  7641  cauappcvgprlemopu  7642  cauappcvgprlemupu  7643  cauappcvgprlemloc  7646  cauappcvgprlemcl  7647  cauappcvgprlemladdfu  7648  cauappcvgprlemladdfl  7649  cauappcvgprlem2  7654  caucvgprlemm  7662  caucvgprlemopl  7663  caucvgprlemlol  7664  caucvgprlemopu  7665  caucvgprlemupu  7666  caucvgprlemloc  7669  caucvgprlemcl  7670  caucvgprlemladdfu  7671  caucvgprlem2  7674  caucvgprprlemml  7688  caucvgprprlemmu  7689  caucvgprprlemopl  7691  caucvgprprlemlol  7692  caucvgprprlemopu  7693  caucvgprprlemupu  7694  caucvgprprlemloc  7697  caucvgprprlemcl  7698  caucvgprprlem2  7704  suplocexprlemex  7716  suplocsrlem  7802  elrealeu  7823  rereceu  7883  axpre-suploclemres  7895  negf1o  8333  aptap  8601  receuap  8620  divvalap  8625  cju  8912  nn0ge2m1nn  9230  nnnegz  9250  elnnz  9257  elnn0z  9260  peano2z  9283  nn0n0n1ge2  9317  msqznn  9347  eluzaddi  9548  eluzsubi  9549  uzind4  9582  supinfneg  9589  infsupneg  9590  elnn1uz2  9601  uz2mulcl  9602  divfnzn  9615  nnrp  9657  rpaddcl  9671  rpmulcl  9672  rpdivcl  9673  rpgecl  9676  ge0p1rp  9679  elrpd  9687  ge0addcl  9975  ge0mulcl  9976  ge0xaddcl  9977  icoshftf1o  9985  peano2fzr  10030  uzsubsubfz  10040  fzsplit2  10043  elfznn  10047  fzss1  10056  fzss2  10057  fzp1elp1  10068  elfz1b  10083  elfz0fzfz0  10119  fz0fzelfz0  10120  difelfznle  10128  elfzofz  10155  fzosplitsnm1  10202  ubmelm1fzo  10219  fzofzp1b  10221  fzosplitsn  10226  exbtwnz  10244  flqge0nn0  10286  flqge1nn  10287  zmodcl  10337  modqmuladdnn0  10361  modsumfzodifsn  10389  frec2uzf1od  10399  frec2uzisod  10400  frecuzrdgrrn  10401  frec2uzrdg  10402  frecuzrdgrcl  10403  frecuzrdgtcl  10405  frecuzrdgsuc  10407  frecuzrdgrclt  10408  frecuzrdgfunlem  10412  frecuzrdgtclt  10414  frecuzrdgsuctlem  10416  uzennn  10429  seq3fveq2  10462  monoord  10469  iseqf1olemqcl  10479  iseqf1olemnab  10481  iseqf1olemab  10482  iseqf1olemqf1o  10486  seq3f1olemqsumkj  10491  seq3f1olemqsumk  10492  seq3id2  10502  exp3val  10515  expcl2lemap  10525  expclzaplem  10537  expge0  10549  expge1  10550  zsqcl2  10590  bcval4  10723  bcn1  10729  bccl2  10739  hashennnuni  10750  hashunlem  10775  hashdifpr  10791  zfz1isolem1  10811  seq3coll  10813  shftfn  10824  shftf  10830  recvguniq  10995  resqrexlemdecn  11012  rersqreu  11028  nn0abscl  11085  nnabscl  11100  abs2dif  11106  climuni  11292  2clim  11300  climcn2  11308  summodclem2a  11380  fsum3  11386  fsum3cvg3  11395  fsumcl2lem  11397  fsumadd  11405  fisum0diag2  11446  fsummulc2  11447  fsumge0  11458  geolim2  11511  cvgratnnlemabsle  11526  cvgratz  11531  mertenslemi1  11534  prodmodclem3  11574  prodmodclem2a  11575  fprodeq0  11616  fprodge0  11636  eff2  11679  tanvalap  11707  zdvdsdc  11810  fzo0dvdseq  11853  oexpneg  11872  oddge22np1  11876  evennn02n  11877  evennn2n  11878  nno  11901  divalglemeunn  11916  divalglemex  11917  divalglemeuneg  11918  divalg  11919  zsupcllemstep  11936  zsupcl  11938  divgcdz  11962  bezoutlemmain  11989  bezoutlemmo  11997  bezoutlemeu  11998  bezoutlemle  11999  sqgcd  12020  uzwodc  12028  eucalgval2  12043  eucalglt  12047  lcmcllem  12057  lcmledvds  12060  lcmneg  12064  lcmgcdlem  12067  ncoprmgcdne1b  12079  prmind2  12110  prmdc  12120  sqnprm  12126  isprm5lem  12131  isprm5  12132  isprm6  12137  sqrt2irrlem  12151  pw2dvdseu  12158  sqpweven  12165  2sqpwodd  12166  sqrt2irrap  12170  qgt0numnn  12189  phicl2  12204  hashdvds  12211  crth  12214  phimullem  12215  eulerthlem1  12217  eulerthlemh  12221  eulerthlemth  12222  hashgcdlem  12228  oddprm  12249  pythagtriplem6  12260  pythagtriplem11  12264  pythagtriplem13  12266  pythagtriplem19  12272  pclem0  12276  pcpremul  12283  pceu  12285  pc2dvds  12319  difsqpwdvds  12327  pcadd  12329  pockthlem  12344  pockthg  12345  1arith  12355  oddennn  12383  evenennn  12384  ennnfoneleminc  12402  ennnfonelemf1  12409  ennnfonelemen  12412  exmidunben  12417  ctinf  12421  ctiunctlemfo  12430  nninfdclemlt  12442  nninfdclemf1  12443  mgmsscl  12710  sgrp0  12745  sgrp1  12746  hashfinmndnn  12763  ismndd  12768  mndpfo  12769  mhmf1o  12789  0mhm  12801  mhmco  12802  isgrpd2e  12824  grpinvf1o  12868  grpinvnzcl  12870  dfgrp3m  12897  mhmmnd  12908  ghmgrp  12910  mulgval  12914  mulgfng  12915  subgmulg  12974  issubg4m  12979  isabld  13002  srgfcl  13056  srglmhm  13076  srgrmhm  13077  iscrngd  13121  ringsrg  13124  unitabl  13185  ringelnzr  13227  tgtopon  13348  distopon  13369  epttop  13372  resttopon  13453  resttopon2  13460  cnco  13503  lmss  13528  txtopon  13544  uptx  13556  txdis1cn  13560  hmeocnv  13589  hmeof1o2  13590  hmeores  13597  hmeoco  13598  idhmeo  13599  txhmeo  13601  txswaphmeo  13603  psmetxrge0  13614  isxmet2d  13630  metres2  13663  xmetresbl  13722  comet  13781  bdxmet  13783  bdmet  13784  tgioo  13828  mulc1cncf  13858  mulcncflem  13872  cnrehmeocntop  13875  cnopnap  13876  dedekindeu  13883  dedekindicclemicc  13892  ivthinclemlm  13894  ivthinclemum  13895  ivthinclemlopn  13896  ivthinclemlr  13897  ivthinclemuopn  13898  ivthinclemur  13899  ivthinclemloc  13901  ivthinc  13903  dvfgg  13939  dvcjbr  13954  dvcj  13955  dvfre  13956  rplogbval  14145  lgsfcl2  14189  lgsval2lem  14193  lgsmod  14209  lgsdirprm  14217  lgsne0  14221  2sqlem8  14241  2sqlem9  14242  bj-charfundcALT  14332  bj-nnord  14481  bj-inf2vnlem1  14493  pwf1oexmid  14520  nnsf  14525  nninfall  14529  nninfself  14533  exmidsbthrlem  14541  qdencn  14546