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:  dcand  935  sb2  1790  sbequ1  1791  sbidm  1874  eqeu  2943  euind  2960  reuind  2978  eldifd  3176  eqssd  3210  ssrabdv  3272  elind  3358  dcun  3570  opm  4278  issod  4366  ordsucim  4548  onintonm  4565  ordtri2or2exmidlem  4574  en2lp  4602  ordwe  4624  sosng  4748  sotri2  5080  sotri3  5081  relssdmrn  5203  funun  5315  fnsng  5321  fnprg  5329  fntpg  5330  fntp  5331  fununi  5342  imain  5356  fnco  5384  f00  5467  f1ss  5487  f1ssr  5488  f1ssres  5490  f1f1orn  5533  foimacnv  5540  foun  5541  fun11iun  5543  sefvex  5597  dff3im  5725  fmpt  5730  ffnfv  5738  fmpt2d  5742  ffvresb  5743  fprg  5767  foco2  5822  fcof1  5852  fcofo  5853  fcof1o  5858  fliftf  5868  isoini2  5888  f1oiso  5895  moriotass  5928  fnoprabg  6046  f1ocnvd  6148  suppssfv  6154  suppssov1  6155  1stcof  6249  2ndcof  6250  1stconst  6307  2ndconst  6308  fo2ndf  6313  f1o2ndf1  6314  f1od2  6321  smores2  6380  tfrlem5  6400  tfrlemibfn  6414  tfr1onlembfn  6430  tfri1dALT  6437  tfrcllembfn  6443  nntri2  6580  eroveu  6713  elixpsn  6822  dom2lem  6863  xpf1o  6941  fidifsnen  6967  finexdc  6999  unfidisj  7019  f1finf1o  7049  fidcenumlemrks  7055  sbthlemi9  7067  supeuti  7096  infeuti  7131  casef1  7192  caseinl  7193  caseinr  7194  difinfsnlem  7201  ctmlemr  7210  ctm  7211  ctssdclemn0  7212  ctssdccl  7213  ctssdc  7215  enumctlemm  7216  nnnninf  7228  nninfwlpoimlemg  7277  en2other2  7304  exmidfodomrlemim  7309  pw1nel3  7343  dftap2  7363  cc2lem  7378  cc4f  7381  addclpi  7440  mulclpi  7441  nnppipi  7456  recmulnqg  7504  enq0ref  7546  nqnq0pi  7551  genipv  7622  addclpr  7650  nqprxx  7659  prmuloc  7679  mulclpr  7685  distrlem1prl  7695  distrlem1pru  7696  ltexprlempr  7721  ltexprlemrl  7723  ltexprlemru  7725  lteupri  7730  recexprlempr  7745  cauappcvgprlemm  7758  cauappcvgprlemopl  7759  cauappcvgprlemlol  7760  cauappcvgprlemopu  7761  cauappcvgprlemupu  7762  cauappcvgprlemloc  7765  cauappcvgprlemcl  7766  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  cauappcvgprlem2  7773  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemlol  7783  caucvgprlemopu  7784  caucvgprlemupu  7785  caucvgprlemloc  7788  caucvgprlemcl  7789  caucvgprlemladdfu  7790  caucvgprlem2  7793  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemopu  7812  caucvgprprlemupu  7813  caucvgprprlemloc  7816  caucvgprprlemcl  7817  caucvgprprlem2  7823  suplocexprlemex  7835  suplocsrlem  7921  elrealeu  7942  rereceu  8002  axpre-suploclemres  8014  negf1o  8454  aptap  8723  receuap  8742  divvalap  8747  cju  9034  nn0ge2m1nn  9355  nnnegz  9375  elnnz  9382  elnn0z  9385  peano2z  9408  nn0n0n1ge2  9443  msqznn  9473  eluzaddi  9675  eluzsubi  9676  uzind4  9709  supinfneg  9716  infsupneg  9717  elnn1uz2  9728  uz2mulcl  9729  divfnzn  9742  nnrp  9785  rpaddcl  9799  rpmulcl  9800  rpdivcl  9801  rpgecl  9804  ge0p1rp  9807  elrpd  9815  ge0addcl  10103  ge0mulcl  10104  ge0xaddcl  10105  icoshftf1o  10113  peano2fzr  10159  uzsubsubfz  10169  fzsplit2  10172  elfznn  10176  fzss1  10185  fzss2  10186  fzp1elp1  10197  elfz1b  10212  elfz0fzfz0  10248  fz0fzelfz0  10249  difelfznle  10257  elfzofz  10285  fzosplitsnm1  10338  ubmelm1fzo  10355  fzofzp1b  10357  fzosplitsn  10362  zsupcllemstep  10372  zsupcl  10374  exbtwnz  10393  flqge0nn0  10436  flqge1nn  10437  zmodcl  10489  modqmuladdnn0  10513  modsumfzodifsn  10541  frec2uzf1od  10551  frec2uzisod  10552  frecuzrdgrrn  10553  frec2uzrdg  10554  frecuzrdgrcl  10555  frecuzrdgtcl  10557  frecuzrdgsuc  10559  frecuzrdgrclt  10560  frecuzrdgfunlem  10564  frecuzrdgtclt  10566  frecuzrdgsuctlem  10568  uzennn  10581  seq3fveq2  10620  seqfveq2g  10622  monoord  10630  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemab  10647  iseqf1olemqf1o  10651  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seq3id2  10671  exp3val  10686  expcl2lemap  10696  expclzaplem  10708  expge0  10720  expge1  10721  zsqcl2  10762  bcval4  10897  bcn1  10903  bccl2  10913  hashennnuni  10924  hashunlem  10949  hashdifpr  10965  zfz1isolem1  10985  seq3coll  10987  iswrdiz  11001  ccatsymb  11058  ccatrn  11065  swrds1  11121  swrdccat2  11124  shftfn  11135  shftf  11141  recvguniq  11306  resqrexlemdecn  11323  rersqreu  11339  nn0abscl  11396  nnabscl  11411  abs2dif  11417  nn0maxcl  11536  climuni  11604  2clim  11612  climcn2  11620  summodclem2a  11692  fsum3  11698  fsum3cvg3  11707  fsumcl2lem  11709  fsumadd  11717  fisum0diag2  11758  fsummulc2  11759  fsumge0  11770  geolim2  11823  cvgratnnlemabsle  11838  cvgratz  11843  mertenslemi1  11846  prodmodclem3  11886  prodmodclem2a  11887  fprodeq0  11928  fprodge0  11948  eff2  11991  tanvalap  12019  zdvdsdc  12123  fzo0dvdseq  12168  oexpneg  12188  oddge22np1  12192  evennn02n  12193  evennn2n  12194  nno  12217  divalglemeunn  12232  divalglemex  12233  divalglemeuneg  12234  divalg  12235  bitsfzolem  12265  bitsinv1lem  12272  divgcdz  12292  bezoutlemmain  12319  bezoutlemmo  12327  bezoutlemeu  12328  bezoutlemle  12329  sqgcd  12350  uzwodc  12358  nninfctlemfo  12361  eucalgval2  12375  eucalglt  12379  lcmneg  12396  lcmgcdlem  12399  ncoprmgcdne1b  12411  prmind2  12442  prmdc  12452  sqnprm  12458  isprm5lem  12463  isprm5  12464  isprm6  12469  sqrt2irrlem  12483  pw2dvdseu  12490  sqpweven  12497  2sqpwodd  12498  sqrt2irrap  12502  qgt0numnn  12521  phicl2  12536  hashdvds  12543  crth  12546  phimullem  12547  eulerthlem1  12549  eulerthlemh  12553  eulerthlemth  12554  hashgcdlem  12560  oddprm  12582  pythagtriplem6  12593  pythagtriplem11  12597  pythagtriplem13  12599  pythagtriplem19  12605  pclem0  12609  pcpremul  12616  pceu  12618  pc2dvds  12653  difsqpwdvds  12661  pcadd  12663  pockthlem  12679  pockthg  12680  1arith  12690  4sqlemffi  12719  4sqlem11  12724  4sqlem12  12725  4sqlem13m  12726  4sqlem14  12727  4sqlem17  12730  oddennn  12763  evenennn  12764  ennnfoneleminc  12782  ennnfonelemf1  12789  ennnfonelemen  12792  exmidunben  12797  ctinf  12801  ctiunctlemfo  12810  nninfdclemlt  12822  nninfdclemf1  12823  ptex  13096  imasaddfnlemg  13146  imasaddflemg  13148  mgmsscl  13193  sgrp0  13242  sgrp1  13243  hashfinmndnn  13264  ismndd  13269  mndpfo  13270  mhmf1o  13302  0mhm  13318  resmhm  13319  resmhm2  13320  resmhm2b  13321  mhmco  13322  gsumvallem2  13325  isgrpd2e  13352  grpinvf1o  13402  grpinvnzcl  13404  dfgrp3m  13431  mhmmnd  13452  ghmgrp  13454  mulgval  13458  mulgfng  13460  subgmulg  13524  issubg4m  13529  isnsg3  13543  nmzsubg  13546  ssnmz  13547  0nsg  13550  nsgid  13551  ghmnsgima  13604  ghmnsgpreima  13605  ghmf1  13609  kerf1ghm  13610  ghmf1o  13611  conjnmzb  13616  isabld  13635  ghmcmn  13663  ghmabl  13664  invghm  13665  srgfcl  13735  srglmhm  13755  srgrmhm  13756  iscrngd  13804  ringsrg  13809  unitabl  13879  rhmf1o  13930  rhmco  13936  ringelnzr  13949  subrngringnsg  13967  subrgcrng  13987  subrgnzr  14004  resrhm  14010  unitrrg  14029  lssneln0  14136  rnglidlmsgrp  14259  quscrng  14295  expghmap  14369  mulgghm2  14370  znf1o  14413  znidom  14419  znidomb  14420  psrbaglesuppg  14434  tgtopon  14538  distopon  14559  epttop  14562  resttopon  14643  resttopon2  14650  cnco  14693  lmss  14718  txtopon  14734  uptx  14746  txdis1cn  14750  hmeocnv  14779  hmeof1o2  14780  hmeores  14787  hmeoco  14788  idhmeo  14789  txhmeo  14791  txswaphmeo  14793  psmetxrge0  14804  isxmet2d  14820  metres2  14853  xmetresbl  14912  comet  14971  bdxmet  14973  bdmet  14974  tgioo  15026  mulc1cncf  15061  mulcncflem  15079  cnrehmeocntop  15082  cnopnap  15083  dedekindeu  15095  dedekindicclemicc  15104  ivthinclemlm  15106  ivthinclemum  15107  ivthinclemlopn  15108  ivthinclemlr  15109  ivthinclemuopn  15110  ivthinclemur  15111  ivthinclemloc  15113  ivthinc  15115  ivthreinc  15117  dvfgg  15160  dvcjbr  15180  dvcj  15181  dvfre  15182  elplyr  15212  plyreres  15236  rplogbval  15417  sgmnncl  15460  mpodvdsmulf1o  15462  mersenne  15469  perfectlem2  15472  lgsfcl2  15483  lgsval2lem  15487  lgsmod  15503  lgsdirprm  15511  lgsne0  15515  gausslemma2dlem0h  15533  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  gausslemma2dlem4  15541  lgseisenlem1  15547  lgseisenlem2  15548  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem2  15559  2sqlem8  15600  2sqlem9  15601  structiedg0val  15637  bj-charfundcALT  15745  bj-nnord  15894  bj-inf2vnlem1  15906  pwf1oexmid  15936  nnsf  15942  nninfall  15946  nninfself  15950  exmidsbthrlem  15961  qdencn  15966