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  1755  sbequ1  1756  sbidm  1839  eqeu  2895  euind  2912  reuind  2930  eldifd  3125  eqssd  3158  ssrabdv  3220  elind  3306  dcun  3518  opm  4211  issod  4296  ordsucim  4476  onintonm  4493  ordtri2or2exmidlem  4502  en2lp  4530  ordwe  4552  sosng  4676  sotri2  5000  sotri3  5001  relssdmrn  5123  funun  5231  fnsng  5234  fnprg  5242  fntpg  5243  fntp  5244  fununi  5255  imain  5269  fnco  5295  f00  5378  f1ss  5398  f1ssr  5399  f1ssres  5401  f1f1orn  5442  foimacnv  5449  foun  5450  fun11iun  5452  sefvex  5506  dff3im  5629  fmpt  5634  ffnfv  5642  fmpt2d  5646  ffvresb  5647  fprg  5667  foco2  5721  fcof1  5750  fcofo  5751  fcof1o  5756  fliftf  5766  isoini2  5786  f1oiso  5793  moriotass  5825  fnoprabg  5939  f1ocnvd  6039  suppssfv  6045  suppssov1  6046  1stcof  6128  2ndcof  6129  1stconst  6185  2ndconst  6186  fo2ndf  6191  f1o2ndf1  6192  f1od2  6199  smores2  6258  tfrlem5  6278  tfrlemibfn  6292  tfr1onlembfn  6308  tfri1dALT  6315  tfrcllembfn  6321  nntri2  6458  eroveu  6588  elixpsn  6697  dom2lem  6734  xpf1o  6806  fidifsnen  6832  finexdc  6864  unfidisj  6883  f1finf1o  6908  fidcenumlemrks  6914  sbthlemi9  6926  supeuti  6955  infeuti  6990  casef1  7051  caseinl  7052  caseinr  7053  difinfsnlem  7060  ctmlemr  7069  ctm  7070  ctssdclemn0  7071  ctssdccl  7072  ctssdc  7074  enumctlemm  7075  nnnninf  7086  en2other2  7148  exmidfodomrlemim  7153  pw1nel3  7183  cc2lem  7203  cc4f  7206  addclpi  7264  mulclpi  7265  nnppipi  7280  recmulnqg  7328  enq0ref  7370  nqnq0pi  7375  genipv  7446  addclpr  7474  nqprxx  7483  prmuloc  7503  mulclpr  7509  distrlem1prl  7519  distrlem1pru  7520  ltexprlempr  7545  ltexprlemrl  7547  ltexprlemru  7549  lteupri  7554  recexprlempr  7569  cauappcvgprlemm  7582  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemopu  7585  cauappcvgprlemupu  7586  cauappcvgprlemloc  7589  cauappcvgprlemcl  7590  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  cauappcvgprlem2  7597  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemopu  7608  caucvgprlemupu  7609  caucvgprlemloc  7612  caucvgprlemcl  7613  caucvgprlemladdfu  7614  caucvgprlem2  7617  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemopl  7634  caucvgprprlemlol  7635  caucvgprprlemopu  7636  caucvgprprlemupu  7637  caucvgprprlemloc  7640  caucvgprprlemcl  7641  caucvgprprlem2  7647  suplocexprlemex  7659  suplocsrlem  7745  elrealeu  7766  rereceu  7826  axpre-suploclemres  7838  negf1o  8276  receuap  8562  divvalap  8566  cju  8852  nn0ge2m1nn  9170  nnnegz  9190  elnnz  9197  elnn0z  9200  peano2z  9223  nn0n0n1ge2  9257  msqznn  9287  eluzaddi  9488  eluzsubi  9489  uzind4  9522  supinfneg  9529  infsupneg  9530  elnn1uz2  9541  uz2mulcl  9542  divfnzn  9555  nnrp  9595  rpaddcl  9609  rpmulcl  9610  rpdivcl  9611  rpgecl  9614  ge0p1rp  9617  elrpd  9625  ge0addcl  9913  ge0mulcl  9914  ge0xaddcl  9915  icoshftf1o  9923  peano2fzr  9968  uzsubsubfz  9978  fzsplit2  9981  elfznn  9985  fzss1  9994  fzss2  9995  fzp1elp1  10006  elfz1b  10021  elfz0fzfz0  10057  fz0fzelfz0  10058  difelfznle  10066  elfzofz  10093  fzosplitsnm1  10140  ubmelm1fzo  10157  fzofzp1b  10159  fzosplitsn  10164  exbtwnz  10182  flqge0nn0  10224  flqge1nn  10225  zmodcl  10275  modqmuladdnn0  10299  modsumfzodifsn  10327  frec2uzf1od  10337  frec2uzisod  10338  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdgrcl  10341  frecuzrdgtcl  10343  frecuzrdgsuc  10345  frecuzrdgrclt  10346  frecuzrdgfunlem  10350  frecuzrdgtclt  10352  frecuzrdgsuctlem  10354  uzennn  10367  seq3fveq2  10400  monoord  10407  iseqf1olemqcl  10417  iseqf1olemnab  10419  iseqf1olemab  10420  iseqf1olemqf1o  10424  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3id2  10440  exp3val  10453  expcl2lemap  10463  expclzaplem  10475  expge0  10487  expge1  10488  zsqcl2  10528  bcval4  10661  bcn1  10667  bccl2  10677  hashennnuni  10688  hashunlem  10713  hashdifpr  10729  zfz1isolem1  10749  seq3coll  10751  shftfn  10762  shftf  10768  recvguniq  10933  resqrexlemdecn  10950  rersqreu  10966  nn0abscl  11023  nnabscl  11038  abs2dif  11044  climuni  11230  2clim  11238  climcn2  11246  summodclem2a  11318  fsum3  11324  fsum3cvg3  11333  fsumcl2lem  11335  fsumadd  11343  fisum0diag2  11384  fsummulc2  11385  fsumge0  11396  geolim2  11449  cvgratnnlemabsle  11464  cvgratz  11469  mertenslemi1  11472  prodmodclem3  11512  prodmodclem2a  11513  fprodeq0  11554  fprodge0  11574  eff2  11617  tanvalap  11645  zdvdsdc  11748  fzo0dvdseq  11791  oexpneg  11810  oddge22np1  11814  evennn02n  11815  evennn2n  11816  nno  11839  divalglemeunn  11854  divalglemex  11855  divalglemeuneg  11856  divalg  11857  zsupcllemstep  11874  zsupcl  11876  divgcdz  11900  bezoutlemmain  11927  bezoutlemmo  11935  bezoutlemeu  11936  bezoutlemle  11937  sqgcd  11958  uzwodc  11966  eucalgval2  11981  eucalglt  11985  lcmcllem  11995  lcmledvds  11998  lcmneg  12002  lcmgcdlem  12005  ncoprmgcdne1b  12017  prmind2  12048  prmdc  12058  sqnprm  12064  isprm5lem  12069  isprm5  12070  isprm6  12075  sqrt2irrlem  12089  pw2dvdseu  12096  sqpweven  12103  2sqpwodd  12104  sqrt2irrap  12108  qgt0numnn  12127  phicl2  12142  hashdvds  12149  crth  12152  phimullem  12153  eulerthlem1  12155  eulerthlemh  12159  eulerthlemth  12160  hashgcdlem  12166  oddprm  12187  pythagtriplem6  12198  pythagtriplem11  12202  pythagtriplem13  12204  pythagtriplem19  12210  pclem0  12214  pcpremul  12221  pceu  12223  pc2dvds  12257  difsqpwdvds  12265  pcadd  12267  pockthlem  12282  pockthg  12283  1arith  12293  oddennn  12321  evenennn  12322  ennnfoneleminc  12340  ennnfonelemf1  12347  ennnfonelemen  12350  exmidunben  12355  ctinf  12359  ctiunctlemfo  12368  nninfdclemlt  12380  nninfdclemf1  12381  tgtopon  12666  distopon  12687  epttop  12690  resttopon  12771  resttopon2  12778  cnco  12821  lmss  12846  txtopon  12862  uptx  12874  txdis1cn  12878  hmeocnv  12907  hmeof1o2  12908  hmeores  12915  hmeoco  12916  idhmeo  12917  txhmeo  12919  txswaphmeo  12921  psmetxrge0  12932  isxmet2d  12948  metres2  12981  xmetresbl  13040  comet  13099  bdxmet  13101  bdmet  13102  tgioo  13146  mulc1cncf  13176  mulcncflem  13190  cnrehmeocntop  13193  cnopnap  13194  dedekindeu  13201  dedekindicclemicc  13210  ivthinclemlm  13212  ivthinclemum  13213  ivthinclemlopn  13214  ivthinclemlr  13215  ivthinclemuopn  13216  ivthinclemur  13217  ivthinclemloc  13219  ivthinc  13221  dvfgg  13257  dvcjbr  13272  dvcj  13273  dvfre  13274  rplogbval  13463  lgsfcl2  13507  lgsval2lem  13511  lgsmod  13527  lgsdirprm  13535  lgsne0  13539  2sqlem8  13559  2sqlem9  13560  bj-charfundcALT  13651  bj-nnord  13800  bj-inf2vnlem1  13812  pwf1oexmid  13839  nnsf  13845  nninfall  13849  nninfself  13853  exmidsbthrlem  13861  qdencn  13866