Theorem sylanbrc 414

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 304	. 2 |- ( ph -> ( ps /\ ch ) )
4		sylanbrc.3	. 2 |- ( th <-> ( ps /\ ch ) )
5	3, 4	sylibr 133	1 |- ( ph -> th )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sb2  1741  sbequ1  1742  sbidm  1824  eqeu  2858  euind  2875  reuind  2893  eldifd  3086  eqssd  3119  ssrabdv  3181  elind  3266  dcun  3478  opm  4164  issod  4249  ordsucim  4424  onintonm  4441  ordtri2or2exmidlem  4449  en2lp  4477  ordwe  4498  sosng  4620  sotri2  4944  sotri3  4945  relssdmrn  5067  funun  5175  fnsng  5178  fnprg  5186  fntpg  5187  fntp  5188  fununi  5199  imain  5213  fnco  5239  f00  5322  f1ss  5342  f1ssr  5343  f1ssres  5345  f1f1orn  5386  foimacnv  5393  foun  5394  fun11iun  5396  sefvex  5450  dff3im  5573  fmpt  5578  ffnfv  5586  fmpt2d  5590  ffvresb  5591  fprg  5611  foco2  5663  fcof1  5692  fcofo  5693  fcof1o  5698  fliftf  5708  isoini2  5728  f1oiso  5735  moriotass  5766  fnoprabg  5880  f1ocnvd  5980  suppssfv  5986  suppssov1  5987  1stcof  6069  2ndcof  6070  1stconst  6126  2ndconst  6127  fo2ndf  6132  f1o2ndf1  6133  f1od2  6140  smores2  6199  tfrlem5  6219  tfrlemibfn  6233  tfr1onlembfn  6249  tfri1dALT  6256  tfrcllembfn  6262  nntri2  6398  eroveu  6528  elixpsn  6637  dom2lem  6674  xpf1o  6746  fidifsnen  6772  finexdc  6804  unfidisj  6818  f1finf1o  6843  fidcenumlemrks  6849  sbthlemi9  6861  supeuti  6889  infeuti  6924  casef1  6983  caseinl  6984  caseinr  6985  difinfsnlem  6992  ctmlemr  7001  ctm  7002  ctssdclemn0  7003  ctssdccl  7004  ctssdc  7006  enumctlemm  7007  nnnninf  7031  en2other2  7069  exmidfodomrlemim  7074  cc2lem  7098  cc4f  7101  addclpi  7159  mulclpi  7160  nnppipi  7175  recmulnqg  7223  enq0ref  7265  nqnq0pi  7270  genipv  7341  addclpr  7369  nqprxx  7378  prmuloc  7398  mulclpr  7404  distrlem1prl  7414  distrlem1pru  7415  ltexprlempr  7440  ltexprlemrl  7442  ltexprlemru  7444  lteupri  7449  recexprlempr  7464  cauappcvgprlemm  7477  cauappcvgprlemopl  7478  cauappcvgprlemlol  7479  cauappcvgprlemopu  7480  cauappcvgprlemupu  7481  cauappcvgprlemloc  7484  cauappcvgprlemcl  7485  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  cauappcvgprlem2  7492  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemopu  7503  caucvgprlemupu  7504  caucvgprlemloc  7507  caucvgprlemcl  7508  caucvgprlemladdfu  7509  caucvgprlem2  7512  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemopl  7529  caucvgprprlemlol  7530  caucvgprprlemopu  7531  caucvgprprlemupu  7532  caucvgprprlemloc  7535  caucvgprprlemcl  7536  caucvgprprlem2  7542  suplocexprlemex  7554  suplocsrlem  7640  elrealeu  7661  rereceu  7721  axpre-suploclemres  7733  negf1o  8168  receuap  8454  divvalap  8458  cju  8743  nn0ge2m1nn  9061  nnnegz  9081  elnnz  9088  elnn0z  9091  peano2z  9114  nn0n0n1ge2  9145  msqznn  9175  eluzaddi  9376  eluzsubi  9377  uzind4  9410  supinfneg  9417  infsupneg  9418  elnn1uz2  9428  uz2mulcl  9429  divfnzn  9440  nnrp  9480  rpaddcl  9494  rpmulcl  9495  rpdivcl  9496  rpgecl  9499  ge0p1rp  9502  elrpd  9510  ge0addcl  9794  ge0mulcl  9795  ge0xaddcl  9796  icoshftf1o  9804  peano2fzr  9848  uzsubsubfz  9858  fzsplit2  9861  elfznn  9865  fzss1  9874  fzss2  9875  fzp1elp1  9886  elfz1b  9901  elfz0fzfz0  9934  fz0fzelfz0  9935  difelfznle  9943  elfzofz  9970  fzosplitsnm1  10017  ubmelm1fzo  10034  fzofzp1b  10036  fzosplitsn  10041  exbtwnz  10059  flqge0nn0  10097  flqge1nn  10098  zmodcl  10148  modqmuladdnn0  10172  modsumfzodifsn  10200  frec2uzf1od  10210  frec2uzisod  10211  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgtcl  10216  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgfunlem  10223  frecuzrdgtclt  10225  frecuzrdgsuctlem  10227  uzennn  10240  seq3fveq2  10273  monoord  10280  iseqf1olemqcl  10290  iseqf1olemnab  10292  iseqf1olemab  10293  iseqf1olemqf1o  10297  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3id2  10313  exp3val  10326  expcl2lemap  10336  expclzaplem  10348  expge0  10360  expge1  10361  zsqcl2  10401  bcval4  10530  bcn1  10536  bccl2  10546  hashennnuni  10557  hashunlem  10582  hashdifpr  10598  zfz1isolem1  10615  seq3coll  10617  shftfn  10628  shftf  10634  recvguniq  10799  resqrexlemdecn  10816  rersqreu  10832  nn0abscl  10889  nnabscl  10904  abs2dif  10910  climuni  11094  2clim  11102  climcn2  11110  summodclem2a  11182  fsum3  11188  fsum3cvg3  11197  fsumcl2lem  11199  fsumadd  11207  fisum0diag2  11248  fsummulc2  11249  fsumge0  11260  geolim2  11313  cvgratnnlemabsle  11328  cvgratz  11333  mertenslemi1  11336  prodmodclem3  11376  prodmodclem2a  11377  eff2  11423  tanvalap  11451  zdvdsdc  11550  fzo0dvdseq  11591  oexpneg  11610  oddge22np1  11614  evennn02n  11615  evennn2n  11616  nno  11639  divalglemeunn  11654  divalglemex  11655  divalglemeuneg  11656  divalg  11657  zsupcllemstep  11674  zsupcl  11676  divgcdz  11696  bezoutlemmain  11722  bezoutlemmo  11730  bezoutlemeu  11731  bezoutlemle  11732  sqgcd  11753  eucalgval2  11770  eucalglt  11774  lcmcllem  11784  lcmledvds  11787  lcmneg  11791  lcmgcdlem  11794  ncoprmgcdne1b  11806  prmind2  11837  sqnprm  11852  isprm6  11861  sqrt2irrlem  11875  pw2dvdseu  11882  sqpweven  11889  2sqpwodd  11890  sqrt2irrap  11894  qgt0numnn  11913  phicl2  11926  hashdvds  11933  crth  11936  phimullem  11937  hashgcdlem  11939  oddennn  11941  evenennn  11942  ennnfoneleminc  11960  ennnfonelemf1  11967  ennnfonelemen  11970  exmidunben  11975  ctinf  11979  ctiunctlemfo  11988  tgtopon  12274  distopon  12295  epttop  12298  resttopon  12379  resttopon2  12386  cnco  12429  lmss  12454  txtopon  12470  uptx  12482  txdis1cn  12486  hmeocnv  12515  hmeof1o2  12516  hmeores  12523  hmeoco  12524  idhmeo  12525  txhmeo  12527  txswaphmeo  12529  psmetxrge0  12540  isxmet2d  12556  metres2  12589  xmetresbl  12648  comet  12707  bdxmet  12709  bdmet  12710  tgioo  12754  mulc1cncf  12784  mulcncflem  12798  cnrehmeocntop  12801  cnopnap  12802  dedekindeu  12809  dedekindicclemicc  12818  ivthinclemlm  12820  ivthinclemum  12821  ivthinclemlopn  12822  ivthinclemlr  12823  ivthinclemuopn  12824  ivthinclemur  12825  ivthinclemloc  12827  ivthinc  12829  dvfgg  12865  dvcjbr  12880  dvcj  12881  dvfre  12882  rplogbval  13070  bj-nnord  13327  bj-inf2vnlem1  13339  pwf1oexmid  13367  nnsf  13374  nninfall  13379  nninfself  13384  exmidsbthrlem  13392  qdencn  13397