Theorem sylanbrc 417

Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylanbrc.1	⊢ (𝜑 → 𝜓)
sylanbrc.2	⊢ (𝜑 → 𝜒)
sylanbrc.3	⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
sylanbrc	⊢ (𝜑 → 𝜃)

Proof of Theorem sylanbrc

Step	Hyp	Ref	Expression
1		sylanbrc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylanbrc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 306	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		sylanbrc.3	. 2 ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))
5	3, 4	sylibr 134	1 ⊢ (𝜑 → 𝜃)

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  941  ecase2d  1388  sb2  1816  sbequ1  1817  sbidm  1900  eqeu  2986  euind  3003  reuind  3021  eldifd  3220  eqssd  3254  ssrabdv  3316  elind  3403  dcun  3618  opm  4349  issod  4439  ordsucim  4621  onintonm  4638  ordtri2or2exmidlem  4647  en2lp  4675  ordwe  4697  sosng  4822  sotri2  5159  sotri3  5160  relssdmrn  5282  funun  5396  fnsng  5402  fnprg  5410  fntpg  5411  fntp  5412  fununi  5423  imain  5437  fnco  5465  f00  5558  f1ss  5578  f1ssr  5579  f1ssres  5581  f1f1orn  5624  foimacnv  5631  foun  5632  fun11iun  5634  sefvex  5690  dff3im  5821  fmpt  5826  ffnfv  5834  fmpt2d  5838  ffvresb  5839  fprg  5866  foco2  5925  fcof1  5955  fcofo  5956  fcof1o  5961  fliftf  5971  isoini2  5991  f1oiso  5998  moriotass  6033  fnoprabg  6153  f1ocnvd  6256  suppssov1  6262  1stcof  6356  2ndcof  6357  1stconst  6416  2ndconst  6417  fo2ndf  6422  f1o2ndf1  6423  f1od2  6430  suppssfvg  6462  smores2  6524  tfrlem5  6544  tfrlemibfn  6558  tfr1onlembfn  6574  tfri1dALT  6581  tfrcllembfn  6587  nntri2  6726  eroveu  6859  elixpsn  6969  dom2lem  7010  xpf1o  7096  fidifsnen  7124  finexdc  7159  elssdc  7161  unfidisj  7181  f1finf1o  7216  fidcenumlemrks  7222  sbthlemi9  7234  supeuti  7284  infeuti  7319  casef1  7380  caseinl  7381  caseinr  7382  difinfsnlem  7389  ctmlemr  7398  ctm  7399  ctssdclemn0  7400  ctssdccl  7401  ctssdc  7403  enumctlemm  7404  nnnninf  7416  nninfwlpoimlemg  7465  en2other2  7498  exmidfodomrlemim  7503  pw1if  7534  pw1nel3  7540  dftap2  7564  cc2lem  7579  cc4f  7582  addclpi  7641  mulclpi  7642  nnppipi  7657  recmulnqg  7705  enq0ref  7747  nqnq0pi  7752  genipv  7823  addclpr  7851  nqprxx  7860  prmuloc  7880  mulclpr  7886  distrlem1prl  7896  distrlem1pru  7897  ltexprlempr  7922  ltexprlemrl  7924  ltexprlemru  7926  lteupri  7931  recexprlempr  7946  cauappcvgprlemm  7959  cauappcvgprlemopl  7960  cauappcvgprlemlol  7961  cauappcvgprlemopu  7962  cauappcvgprlemupu  7963  cauappcvgprlemloc  7966  cauappcvgprlemcl  7967  cauappcvgprlemladdfu  7968  cauappcvgprlemladdfl  7969  cauappcvgprlem2  7974  caucvgprlemm  7982  caucvgprlemopl  7983  caucvgprlemlol  7984  caucvgprlemopu  7985  caucvgprlemupu  7986  caucvgprlemloc  7989  caucvgprlemcl  7990  caucvgprlemladdfu  7991  caucvgprlem2  7994  caucvgprprlemml  8008  caucvgprprlemmu  8009  caucvgprprlemopl  8011  caucvgprprlemlol  8012  caucvgprprlemopu  8013  caucvgprprlemupu  8014  caucvgprprlemloc  8017  caucvgprprlemcl  8018  caucvgprprlem2  8024  suplocexprlemex  8036  suplocsrlem  8122  elrealeu  8143  rereceu  8203  axpre-suploclemres  8215  negf1o  8654  aptap  8923  receuap  8942  divvalap  8947  cju  9234  nn0ge2m1nn  9559  nnnegz  9579  elnnz  9586  elnn0z  9589  peano2z  9612  nn0n0n1ge2  9647  msqznn  9677  eluzaddi  9880  eluzsubi  9881  uzind4  9919  supinfneg  9926  infsupneg  9927  elnn1uz2  9938  uz2mulcl  9939  divfnzn  9952  nnrp  9995  rpaddcl  10009  rpmulcl  10010  rpdivcl  10011  rpgecl  10014  ge0p1rp  10017  elrpd  10025  ge0addcl  10313  ge0mulcl  10314  ge0xaddcl  10315  icoshftf1o  10323  peano2fzr  10370  uzsubsubfz  10380  fzsplit2  10383  elfznn  10387  fzss1  10396  fzss2  10397  fzp1elp1  10408  elfz1b  10423  elfz0fzfz0  10459  fz0fzelfz0  10460  difelfznle  10468  elfzofz  10496  nn0p1elfzo  10520  fzosplitsnm1  10553  ubmelm1fzo  10570  fzofzp1b  10572  fzosplitsn  10577  zsupcllemstep  10588  zsupcl  10590  exbtwnz  10609  flqge0nn0  10652  flqge1nn  10653  zmodcl  10705  modqmuladdnn0  10729  modsumfzodifsn  10757  frec2uzf1od  10767  frec2uzisod  10768  frecuzrdgrrn  10769  frec2uzrdg  10770  frecuzrdgrcl  10771  frecuzrdgtcl  10773  frecuzrdgsuc  10775  frecuzrdgrclt  10776  frecuzrdgfunlem  10780  frecuzrdgtclt  10782  frecuzrdgsuctlem  10784  uzennn  10797  seq3fveq2  10836  seqfveq2g  10838  monoord  10846  iseqf1olemqcl  10860  iseqf1olemnab  10862  iseqf1olemab  10863  iseqf1olemqf1o  10867  seq3f1olemqsumkj  10872  seq3f1olemqsumk  10873  seq3id2  10887  exp3val  10902  expcl2lemap  10912  expclzaplem  10924  expge0  10936  expge1  10937  zsqcl2  10978  bcval4  11113  bcn1  11119  bccl2  11129  hashennnuni  11140  hashunlem  11166  hashdifpr  11183  zfz1isolem1  11208  seq3coll  11210  iswrdiz  11227  ccatsymb  11286  ccatrn  11293  ccat2s1fvwd  11331  swrds1  11356  swrdccat2  11359  swrdccatin2  11417  pfxccatin12lem2  11419  pfxccatin12lem3  11420  pfxccatin12  11421  pfxccat3  11422  pfxccat3a  11426  shftfn  11505  shftf  11511  recvguniq  11676  resqrexlemdecn  11693  rersqreu  11709  nn0abscl  11766  nnabscl  11781  abs2dif  11787  nn0maxcl  11906  climuni  11974  2clim  11982  climcn2  11990  summodclem2a  12063  fsum3  12069  fsum3cvg3  12078  fsumcl2lem  12080  fsumadd  12088  fisum0diag2  12129  fsummulc2  12130  fsumge0  12141  geolim2  12194  cvgratnnlemabsle  12209  cvgratz  12214  mertenslemi1  12217  prodmodclem3  12257  prodmodclem2a  12258  fprodeq0  12299  fprodge0  12319  eff2  12362  tanvalap  12390  zdvdsdc  12494  fzo0dvdseq  12539  oexpneg  12559  oddge22np1  12563  evennn02n  12564  evennn2n  12565  nno  12588  divalglemeunn  12603  divalglemex  12604  divalglemeuneg  12605  divalg  12606  bitsfzolem  12636  bitsinv1lem  12643  divgcdz  12663  bezoutlemmain  12690  bezoutlemmo  12698  bezoutlemeu  12699  bezoutlemle  12700  sqgcd  12721  uzwodc  12729  nninfctlemfo  12732  eucalgval2  12746  eucalglt  12750  lcmneg  12767  lcmgcdlem  12770  ncoprmgcdne1b  12782  prmind2  12813  prmdc  12823  sqnprm  12829  isprm5lem  12834  isprm5  12835  isprm6  12840  sqrt2irrlem  12854  pw2dvdseu  12861  sqpweven  12868  2sqpwodd  12869  sqrt2irrap  12873  qgt0numnn  12892  phicl2  12907  crth  12917  phimullem  12918  eulerthlem1  12920  eulerthlemh  12924  eulerthlemth  12925  hashgcdlem  12931  oddprm  12953  pythagtriplem6  12964  pythagtriplem11  12968  pythagtriplem13  12970  pythagtriplem19  12976  pclem0  12980  pcpremul  12987  pceu  12989  pc2dvds  13024  difsqpwdvds  13032  pcadd  13034  pockthlem  13050  pockthg  13051  1arith  13061  4sqlemffi  13090  4sqlem11  13095  4sqlem12  13096  4sqlem13m  13097  4sqlem14  13098  4sqlem17  13101  oddennn  13135  evenennn  13136  ennnfoneleminc  13154  ennnfonelemf1  13161  ennnfonelemen  13164  exmidunben  13169  ctinf  13173  ctiunctlemfo  13182  nninfdclemlt  13194  nninfdclemf1  13195  ptex  13469  imasaddfnlemg  13519  imasaddflemg  13521  mgmsscl  13566  sgrp0  13615  sgrp1  13616  hashfinmndnn  13637  ismndd  13642  mndpfo  13643  mhmf1o  13675  0mhm  13691  resmhm  13692  resmhm2  13693  resmhm2b  13694  mhmco  13695  gsumvallem2  13698  isgrpd2e  13725  grpinvf1o  13775  grpinvnzcl  13777  dfgrp3m  13804  mhmmnd  13825  ghmgrp  13827  mulgval  13831  mulgfng  13833  subgmulg  13897  issubg4m  13902  isnsg3  13916  nmzsubg  13919  ssnmz  13920  0nsg  13923  nsgid  13924  ghmnsgima  13977  ghmnsgpreima  13978  ghmf1  13982  kerf1ghm  13983  ghmf1o  13984  conjnmzb  13989  isabld  14008  ghmcmn  14036  ghmabl  14037  invghm  14038  srgfcl  14109  srglmhm  14129  srgrmhm  14130  iscrngd  14178  ringsrg  14183  unitabl  14254  rhmf1o  14305  rhmco  14311  ringelnzr  14324  subrngringnsg  14342  subrgcrng  14362  subrgnzr  14379  resrhm  14385  unitrrg  14405  aprnzr  14425  aprlring  14426  lssneln0  14514  rnglidlmsgrp  14637  quscrng  14673  expghmap  14747  mulgghm2  14748  znf1o  14791  znidom  14797  znidomb  14798  psrbaglesuppg  14813  psrbagcon  14818  tgtopon  14923  distopon  14944  epttop  14947  resttopon  15028  resttopon2  15035  cnco  15078  lmss  15103  txtopon  15119  uptx  15131  txdis1cn  15135  hmeocnv  15164  hmeof1o2  15165  hmeores  15172  hmeoco  15173  idhmeo  15174  txhmeo  15176  txswaphmeo  15178  psmetxrge0  15189  isxmet2d  15205  metres2  15238  xmetresbl  15297  comet  15356  bdxmet  15358  bdmet  15359  tgioo  15411  mulc1cncf  15446  mulcncflem  15464  cnrehmeocntop  15467  cnopnap  15468  dedekindeu  15480  dedekindicclemicc  15489  ivthinclemlm  15491  ivthinclemum  15492  ivthinclemlopn  15493  ivthinclemlr  15494  ivthinclemuopn  15495  ivthinclemur  15496  ivthinclemloc  15498  ivthinc  15500  ivthreinc  15502  dvfgg  15545  dvcjbr  15565  dvcj  15566  dvfre  15567  elplyr  15597  plyreres  15621  rplogbval  15802  sgmnncl  15848  mpodvdsmulf1o  15850  mersenne  15857  perfectlem2  15860  lgsfcl2  15871  lgsval2lem  15875  lgsmod  15891  lgsdirprm  15899  lgsne0  15903  gausslemma2dlem0h  15921  gausslemma2dlem1a  15923  gausslemma2dlem1f1o  15925  gausslemma2dlem4  15929  lgseisenlem1  15935  lgseisenlem2  15936  lgsquadlem1  15942  lgsquadlem2  15943  lgsquad2lem2  15947  2sqlem8  15988  2sqlem9  15989  structiedg0val  16027  ausgrumgrien  16157  usgredgreu  16203  uspgredg2vtxeu  16205  uspgredg2v  16208  usgredg2v  16211  usgr1e  16228  subuhgr  16259  subupgr  16260  subumgr  16261  subusgr  16262  vdegp1aid  16301  trlres  16377  clwwlkbp  16382  clwwlkccatlem  16387  s2elclwwlknon2  16423  clwwlknonex2lem2  16425  clwwlknonex2e  16427  bj-charfundcALT  16571  bj-nnord  16720  bj-inf2vnlem1  16732  pwf1oexmid  16765  nnsf  16775  nninfall  16779  nninfself  16783  exmidsbthrlem  16794  qdencn  16799  gfsumval  16853