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  940  ecase2d  1387  sb2  1815  sbequ1  1816  sbidm  1899  eqeu  2976  euind  2993  reuind  3011  eldifd  3210  eqssd  3244  ssrabdv  3306  elind  3392  dcun  3604  opm  4326  issod  4416  ordsucim  4598  onintonm  4615  ordtri2or2exmidlem  4624  en2lp  4652  ordwe  4674  sosng  4799  sotri2  5134  sotri3  5135  relssdmrn  5257  funun  5371  fnsng  5377  fnprg  5385  fntpg  5386  fntp  5387  fununi  5398  imain  5412  fnco  5440  f00  5528  f1ss  5548  f1ssr  5549  f1ssres  5551  f1f1orn  5594  foimacnv  5601  foun  5602  fun11iun  5604  sefvex  5660  dff3im  5792  fmpt  5797  ffnfv  5805  fmpt2d  5809  ffvresb  5810  fprg  5836  foco2  5893  fcof1  5923  fcofo  5924  fcof1o  5929  fliftf  5939  isoini2  5959  f1oiso  5966  moriotass  6001  fnoprabg  6121  f1ocnvd  6224  suppssfv  6230  suppssov1  6231  1stcof  6325  2ndcof  6326  1stconst  6385  2ndconst  6386  fo2ndf  6391  f1o2ndf1  6392  f1od2  6399  smores2  6459  tfrlem5  6479  tfrlemibfn  6493  tfr1onlembfn  6509  tfri1dALT  6516  tfrcllembfn  6522  nntri2  6661  eroveu  6794  elixpsn  6903  dom2lem  6944  xpf1o  7029  fidifsnen  7056  finexdc  7091  elssdc  7093  unfidisj  7113  f1finf1o  7145  fidcenumlemrks  7151  sbthlemi9  7163  supeuti  7192  infeuti  7227  casef1  7288  caseinl  7289  caseinr  7290  difinfsnlem  7297  ctmlemr  7306  ctm  7307  ctssdclemn0  7308  ctssdccl  7309  ctssdc  7311  enumctlemm  7312  nnnninf  7324  nninfwlpoimlemg  7373  en2other2  7406  exmidfodomrlemim  7411  pw1if  7442  pw1nel3  7448  dftap2  7469  cc2lem  7484  cc4f  7487  addclpi  7546  mulclpi  7547  nnppipi  7562  recmulnqg  7610  enq0ref  7652  nqnq0pi  7657  genipv  7728  addclpr  7756  nqprxx  7765  prmuloc  7785  mulclpr  7791  distrlem1prl  7801  distrlem1pru  7802  ltexprlempr  7827  ltexprlemrl  7829  ltexprlemru  7831  lteupri  7836  recexprlempr  7851  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemopu  7867  cauappcvgprlemupu  7868  cauappcvgprlemloc  7871  cauappcvgprlemcl  7872  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlem2  7879  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemopu  7890  caucvgprlemupu  7891  caucvgprlemloc  7894  caucvgprlemcl  7895  caucvgprlemladdfu  7896  caucvgprlem2  7899  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemupu  7919  caucvgprprlemloc  7922  caucvgprprlemcl  7923  caucvgprprlem2  7929  suplocexprlemex  7941  suplocsrlem  8027  elrealeu  8048  rereceu  8108  axpre-suploclemres  8120  negf1o  8560  aptap  8829  receuap  8848  divvalap  8853  cju  9140  nn0ge2m1nn  9461  nnnegz  9481  elnnz  9488  elnn0z  9491  peano2z  9514  nn0n0n1ge2  9549  msqznn  9579  eluzaddi  9782  eluzsubi  9783  uzind4  9821  supinfneg  9828  infsupneg  9829  elnn1uz2  9840  uz2mulcl  9841  divfnzn  9854  nnrp  9897  rpaddcl  9911  rpmulcl  9912  rpdivcl  9913  rpgecl  9916  ge0p1rp  9919  elrpd  9927  ge0addcl  10215  ge0mulcl  10216  ge0xaddcl  10217  icoshftf1o  10225  peano2fzr  10271  uzsubsubfz  10281  fzsplit2  10284  elfznn  10288  fzss1  10297  fzss2  10298  fzp1elp1  10309  elfz1b  10324  elfz0fzfz0  10360  fz0fzelfz0  10361  difelfznle  10369  elfzofz  10397  fzosplitsnm1  10453  ubmelm1fzo  10470  fzofzp1b  10472  fzosplitsn  10477  zsupcllemstep  10488  zsupcl  10490  exbtwnz  10509  flqge0nn0  10552  flqge1nn  10553  zmodcl  10605  modqmuladdnn0  10629  modsumfzodifsn  10657  frec2uzf1od  10667  frec2uzisod  10668  frecuzrdgrrn  10669  frec2uzrdg  10670  frecuzrdgrcl  10671  frecuzrdgtcl  10673  frecuzrdgsuc  10675  frecuzrdgrclt  10676  frecuzrdgfunlem  10680  frecuzrdgtclt  10682  frecuzrdgsuctlem  10684  uzennn  10697  seq3fveq2  10736  seqfveq2g  10738  monoord  10746  iseqf1olemqcl  10760  iseqf1olemnab  10762  iseqf1olemab  10763  iseqf1olemqf1o  10767  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3id2  10787  exp3val  10802  expcl2lemap  10812  expclzaplem  10824  expge0  10836  expge1  10837  zsqcl2  10878  bcval4  11013  bcn1  11019  bccl2  11029  hashennnuni  11040  hashunlem  11066  hashdifpr  11083  zfz1isolem1  11103  seq3coll  11105  iswrdiz  11119  ccatsymb  11178  ccatrn  11185  ccat2s1fvwd  11223  swrds1  11248  swrdccat2  11251  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12lem3  11312  pfxccatin12  11313  pfxccat3  11314  pfxccat3a  11318  shftfn  11384  shftf  11390  recvguniq  11555  resqrexlemdecn  11572  rersqreu  11588  nn0abscl  11645  nnabscl  11660  abs2dif  11666  nn0maxcl  11785  climuni  11853  2clim  11861  climcn2  11869  summodclem2a  11941  fsum3  11947  fsum3cvg3  11956  fsumcl2lem  11958  fsumadd  11966  fisum0diag2  12007  fsummulc2  12008  fsumge0  12019  geolim2  12072  cvgratnnlemabsle  12087  cvgratz  12092  mertenslemi1  12095  prodmodclem3  12135  prodmodclem2a  12136  fprodeq0  12177  fprodge0  12197  eff2  12240  tanvalap  12268  zdvdsdc  12372  fzo0dvdseq  12417  oexpneg  12437  oddge22np1  12441  evennn02n  12442  evennn2n  12443  nno  12466  divalglemeunn  12481  divalglemex  12482  divalglemeuneg  12483  divalg  12484  bitsfzolem  12514  bitsinv1lem  12521  divgcdz  12541  bezoutlemmain  12568  bezoutlemmo  12576  bezoutlemeu  12577  bezoutlemle  12578  sqgcd  12599  uzwodc  12607  nninfctlemfo  12610  eucalgval2  12624  eucalglt  12628  lcmneg  12645  lcmgcdlem  12648  ncoprmgcdne1b  12660  prmind2  12691  prmdc  12701  sqnprm  12707  isprm5lem  12712  isprm5  12713  isprm6  12718  sqrt2irrlem  12732  pw2dvdseu  12739  sqpweven  12746  2sqpwodd  12747  sqrt2irrap  12751  qgt0numnn  12770  phicl2  12785  hashdvds  12792  crth  12795  phimullem  12796  eulerthlem1  12798  eulerthlemh  12802  eulerthlemth  12803  hashgcdlem  12809  oddprm  12831  pythagtriplem6  12842  pythagtriplem11  12846  pythagtriplem13  12848  pythagtriplem19  12854  pclem0  12858  pcpremul  12865  pceu  12867  pc2dvds  12902  difsqpwdvds  12910  pcadd  12912  pockthlem  12928  pockthg  12929  1arith  12939  4sqlemffi  12968  4sqlem11  12973  4sqlem12  12974  4sqlem13m  12975  4sqlem14  12976  4sqlem17  12979  oddennn  13012  evenennn  13013  ennnfoneleminc  13031  ennnfonelemf1  13038  ennnfonelemen  13041  exmidunben  13046  ctinf  13050  ctiunctlemfo  13059  nninfdclemlt  13071  nninfdclemf1  13072  ptex  13346  imasaddfnlemg  13396  imasaddflemg  13398  mgmsscl  13443  sgrp0  13492  sgrp1  13493  hashfinmndnn  13514  ismndd  13519  mndpfo  13520  mhmf1o  13552  0mhm  13568  resmhm  13569  resmhm2  13570  resmhm2b  13571  mhmco  13572  gsumvallem2  13575  isgrpd2e  13602  grpinvf1o  13652  grpinvnzcl  13654  dfgrp3m  13681  mhmmnd  13702  ghmgrp  13704  mulgval  13708  mulgfng  13710  subgmulg  13774  issubg4m  13779  isnsg3  13793  nmzsubg  13796  ssnmz  13797  0nsg  13800  nsgid  13801  ghmnsgima  13854  ghmnsgpreima  13855  ghmf1  13859  kerf1ghm  13860  ghmf1o  13861  conjnmzb  13866  isabld  13885  ghmcmn  13913  ghmabl  13914  invghm  13915  srgfcl  13985  srglmhm  14005  srgrmhm  14006  iscrngd  14054  ringsrg  14059  unitabl  14130  rhmf1o  14181  rhmco  14187  ringelnzr  14200  subrngringnsg  14218  subrgcrng  14238  subrgnzr  14255  resrhm  14261  unitrrg  14280  lssneln0  14387  rnglidlmsgrp  14510  quscrng  14546  expghmap  14620  mulgghm2  14621  znf1o  14664  znidom  14670  znidomb  14671  psrbaglesuppg  14685  tgtopon  14789  distopon  14810  epttop  14813  resttopon  14894  resttopon2  14901  cnco  14944  lmss  14969  txtopon  14985  uptx  14997  txdis1cn  15001  hmeocnv  15030  hmeof1o2  15031  hmeores  15038  hmeoco  15039  idhmeo  15040  txhmeo  15042  txswaphmeo  15044  psmetxrge0  15055  isxmet2d  15071  metres2  15104  xmetresbl  15163  comet  15222  bdxmet  15224  bdmet  15225  tgioo  15277  mulc1cncf  15312  mulcncflem  15330  cnrehmeocntop  15333  cnopnap  15334  dedekindeu  15346  dedekindicclemicc  15355  ivthinclemlm  15357  ivthinclemum  15358  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemloc  15364  ivthinc  15366  ivthreinc  15368  dvfgg  15411  dvcjbr  15431  dvcj  15432  dvfre  15433  elplyr  15463  plyreres  15487  rplogbval  15668  sgmnncl  15711  mpodvdsmulf1o  15713  mersenne  15720  perfectlem2  15723  lgsfcl2  15734  lgsval2lem  15738  lgsmod  15754  lgsdirprm  15762  lgsne0  15766  gausslemma2dlem0h  15784  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  gausslemma2dlem4  15792  lgseisenlem1  15798  lgseisenlem2  15799  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem2  15810  2sqlem8  15851  2sqlem9  15852  structiedg0val  15890  ausgrumgrien  16020  usgredgreu  16066  uspgredg2vtxeu  16068  uspgredg2v  16071  usgredg2v  16074  usgr1e  16091  subuhgr  16122  subupgr  16123  subumgr  16124  subusgr  16125  vdegp1aid  16164  trlres  16240  clwwlkbp  16245  clwwlkccatlem  16250  s2elclwwlknon2  16286  clwwlknonex2lem2  16288  clwwlknonex2e  16290  bj-charfundcALT  16404  bj-nnord  16553  bj-inf2vnlem1  16565  pwf1oexmid  16600  nnsf  16607  nninfall  16611  nninfself  16615  exmidsbthrlem  16626  qdencn  16631  gfsumval  16680