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  2990  euind  3007  reuind  3025  eldifd  3224  eqssd  3259  ssrabdv  3321  elind  3408  dcun  3623  opm  4355  issod  4445  ordsucim  4627  onintonm  4644  ordtri2or2exmidlem  4653  en2lp  4681  ordwe  4703  sosng  4828  sotri2  5165  sotri3  5166  relssdmrn  5288  funun  5402  fnsng  5408  fnprg  5416  fntpg  5417  fntp  5418  fununi  5429  imain  5443  fnco  5471  f00  5564  f1ss  5584  f1ssr  5585  f1ssres  5587  f1f1orn  5630  foimacnv  5637  foun  5638  fun11iun  5640  sefvex  5696  dff3im  5827  fmpt  5832  ffnfv  5840  fmpt2d  5844  ffvresb  5845  fprg  5872  foco2  5932  fcof1  5962  fcofo  5963  fcof1o  5968  fliftf  5978  isoini2  5998  f1oiso  6005  moriotass  6042  fnoprabg  6162  f1ocnvd  6265  f1o3d  6271  suppssov1  6272  1stcof  6370  2ndcof  6371  1stconst  6430  2ndconst  6431  fo2ndf  6436  f1o2ndf1  6437  f1od2  6444  suppssfvg  6476  smores2  6538  tfrlem5  6558  tfrlemibfn  6572  tfr1onlembfn  6588  tfri1dALT  6595  tfrcllembfn  6601  nntri2  6740  eroveu  6873  elixpsn  6983  dom2lem  7024  xpf1o  7110  fidifsnen  7138  finexdc  7173  elssdc  7175  unfidisj  7195  f1finf1o  7230  fidcenumlemrks  7236  sbthlemi9  7248  supeuti  7298  infeuti  7333  casef1  7394  caseinl  7395  caseinr  7396  difinfsnlem  7403  ctmlemr  7412  ctm  7413  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumctlemm  7418  nnnninf  7430  nninfwlpoimlemg  7479  en2other2  7512  exmidfodomrlemim  7517  pw1if  7548  pw1nel3  7554  dftap2  7581  cc2lem  7596  cc4f  7599  addclpi  7658  mulclpi  7659  nnppipi  7674  recmulnqg  7722  enq0ref  7764  nqnq0pi  7769  genipv  7840  addclpr  7868  nqprxx  7877  prmuloc  7897  mulclpr  7903  distrlem1prl  7913  distrlem1pru  7914  ltexprlempr  7939  ltexprlemrl  7941  ltexprlemru  7943  lteupri  7948  recexprlempr  7963  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemloc  7983  cauappcvgprlemcl  7984  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlem2  7991  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlem2  8011  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemupu  8031  caucvgprprlemloc  8034  caucvgprprlemcl  8035  caucvgprprlem2  8041  suplocexprlemex  8053  suplocsrlem  8139  elrealeu  8160  rereceu  8220  axpre-suploclemres  8232  negf1o  8673  aptap  8942  receuap  8963  divvalap  8968  cju  9255  nn0ge2m1nn  9580  nnnegz  9600  elnnz  9607  elnn0z  9610  peano2z  9633  nn0n0n1ge2  9668  msqznn  9699  eluzaddi  9902  eluzsubi  9903  uzind4  9941  supinfneg  9948  infsupneg  9949  elnn1uz2  9960  uz2mulcl  9961  divfnzn  9974  nnrp  10017  rpaddcl  10031  rpmulcl  10032  rpdivcl  10033  rpgecl  10036  ge0p1rp  10039  elrpd  10047  ge0addcl  10336  ge0mulcl  10337  ge0xaddcl  10338  icoshftf1o  10346  peano2fzr  10394  uzsubsubfz  10404  fzsplit2  10407  fzsplit3  10410  elfznn  10412  fzss1  10421  fzss2  10422  fzp1elp1  10434  elfz1b  10449  elfz0fzfz0  10485  fz0fzelfz0  10486  difelfznle  10494  elfzofz  10522  nn0p1elfzo  10546  fzosplitsnm1  10579  ubmelm1fzo  10596  fzofzp1b  10598  fzosplitsn  10603  zsupcllemstep  10614  zsupcl  10616  infssfzcldc  10621  infssfzledc  10622  exbtwnz  10637  flqge0nn0  10680  flqge1nn  10681  zmodcl  10733  modqmuladdnn0  10757  modsumfzodifsn  10785  frec2uzf1od  10795  frec2uzisod  10796  frecuzrdgrrn  10797  frec2uzrdg  10798  frecuzrdgrcl  10799  frecuzrdgtcl  10801  frecuzrdgsuc  10803  frecuzrdgrclt  10804  frecuzrdgfunlem  10808  frecuzrdgtclt  10810  frecuzrdgsuctlem  10812  uzennn  10825  seq3fveq2  10864  seqfveq2g  10866  monoord  10874  iseqf1olemqcl  10888  iseqf1olemnab  10890  iseqf1olemab  10891  iseqf1olemqf1o  10895  seq3f1olemqsumkj  10900  seq3f1olemqsumk  10901  seq3id2  10915  exp3val  10930  expcl2lemap  10940  expclzaplem  10952  expge0  10964  expge1  10965  zsqcl2  11006  bcval4  11142  bcn1  11148  bccl2  11158  hashennnuni  11170  hashunlem  11196  hashdifpr  11213  zfz1isolem1  11240  seq3coll  11242  iswrdiz  11259  ccatsymb  11318  ccatrn  11325  ccat2s1fvwd  11363  swrds1  11388  swrdccat2  11391  swrdccatin2  11449  pfxccatin12lem2  11451  pfxccatin12lem3  11452  pfxccatin12  11453  pfxccat3  11454  pfxccat3a  11458  shftfn  11537  shftf  11543  recvguniq  11709  resqrexlemdecn  11726  rersqreu  11742  nn0abscl  11799  nnabscl  11814  abs2dif  11820  nn0maxcl  11939  climuni  12007  2clim  12015  climcn2  12023  summodclem2a  12096  fsum3  12102  fsum3cvg3  12111  fsumcl2lem  12113  fsumadd  12121  fisum0diag2  12162  fsummulc2  12163  fsumge0  12174  geolim2  12227  cvgratnnlemabsle  12242  cvgratz  12247  mertenslemi1  12250  prodmodclem3  12290  prodmodclem2a  12291  fprodeq0  12332  fprodge0  12352  eff2  12395  tanvalap  12423  zdvdsdc  12527  fzo0dvdseq  12572  oexpneg  12592  oddge22np1  12596  evennn02n  12597  evennn2n  12598  nno  12621  divalglemeunn  12636  divalglemex  12637  divalglemeuneg  12638  divalg  12639  bitsfzolem  12669  bitsinv1lem  12676  divgcdz  12696  bezoutlemmain  12723  bezoutlemmo  12731  bezoutlemeu  12732  bezoutlemle  12733  sqgcd  12754  uzwodc  12762  nninfctlemfo  12765  eucalgval2  12779  eucalglt  12783  lcmneg  12800  lcmgcdlem  12803  ncoprmgcdne1b  12815  prmind2  12846  prmdc  12856  sqnprm  12862  isprm5lem  12867  isprm5  12868  isprm6  12873  sqrt2irrlem  12887  pw2dvdseu  12894  sqpweven  12901  2sqpwodd  12902  sqrt2irrap  12906  qgt0numnn  12925  phicl2  12940  crth  12950  phimullem  12951  eulerthlem1  12953  eulerthlemh  12957  eulerthlemth  12958  hashgcdlem  12964  oddprm  12986  pythagtriplem6  12997  pythagtriplem11  13001  pythagtriplem13  13003  pythagtriplem19  13009  pclem0  13013  pcpremul  13020  pceu  13022  pc2dvds  13057  difsqpwdvds  13065  pcadd  13067  pockthlem  13083  pockthg  13084  1arith  13094  4sqlemffi  13123  4sqlem11  13128  4sqlem12  13129  4sqlem13m  13130  4sqlem14  13131  4sqlem17  13134  ballotfilemic  13198  ballotfilem1c  13199  ballotfilemrc  13222  ballotfilemth  13229  oddennn  13231  evenennn  13232  ennnfoneleminc  13250  ennnfonelemf1  13257  ennnfonelemen  13260  exmidunben  13265  ctinf  13269  ctiunctlemfo  13278  nninfdclemlt  13290  nninfdclemf1  13291  ptex  13565  imasaddfnlemg  13582  imasaddflemg  13584  mgmsscl  13628  sgrp0  13677  sgrp1  13678  hashfinmndnn  13697  ismndd  13702  mndpfo  13703  mhmf1o  13729  0mhm  13745  resmhm  13746  resmhm2  13747  resmhm2b  13748  mhmco  13749  gsumvallem2  13752  isgrpd2e  13779  grpinvf1o  13829  grpinvnzcl  13831  dfgrp3m  13858  mhmmnd  13873  ghmgrp  13875  mulgval  13879  mulgfng  13881  subgmulg  13945  issubg4m  13950  isnsg3  13964  nmzsubg  13967  ssnmz  13968  0nsg  13971  nsgid  13972  ghmnsgima  14025  ghmnsgpreima  14026  ghmf1  14030  kerf1ghm  14031  ghmf1o  14032  conjnmzb  14037  isabld  14056  ghmcmn  14084  ghmabl  14085  invghm  14086  gfsumval  14106  srgfcl  14220  srglmhm  14240  srgrmhm  14241  iscrngd  14289  ringsrg  14294  unitabl  14366  rhmf1o  14417  rhmco  14423  ringelnzr  14436  subrngringnsg  14455  subrgcrng  14475  subrgnzr  14492  resrhm  14498  unitrrg  14518  aprnzr  14541  aprlring  14542  drngnzr  14561  lssneln0  14652  rnglidlmsgrp  14775  quscrng  14811  expghmap  14885  mulgghm2  14886  znf1o  14929  znidom  14935  znidomb  14936  psrbaglesuppg  14951  psrbagcon  14956  tgtopon  15061  distopon  15082  epttop  15085  resttopon  15166  resttopon2  15173  cnco  15216  lmss  15241  txtopon  15257  uptx  15269  txdis1cn  15273  hmeocnv  15302  hmeof1o2  15303  hmeores  15310  hmeoco  15311  idhmeo  15312  txhmeo  15314  txswaphmeo  15316  psmetxrge0  15327  isxmet2d  15343  metres2  15376  xmetresbl  15435  comet  15494  bdxmet  15496  bdmet  15497  tgioo  15549  mulc1cncf  15584  mulcncflem  15602  cnrehmeocntop  15605  cnopnap  15606  dedekindeu  15618  dedekindicclemicc  15627  ivthinclemlm  15629  ivthinclemum  15630  ivthinclemlopn  15631  ivthinclemlr  15632  ivthinclemuopn  15633  ivthinclemur  15634  ivthinclemloc  15636  ivthinc  15638  ivthreinc  15640  dvfgg  15683  dvcjbr  15703  dvcj  15704  dvfre  15705  elplyr  15735  plyreres  15759  rplogbval  15940  sgmnncl  15986  mpodvdsmulf1o  15988  mersenne  15995  perfectlem2  15998  lgsfcl2  16009  lgsval2lem  16013  lgsmod  16029  lgsdirprm  16037  lgsne0  16041  gausslemma2dlem0h  16059  gausslemma2dlem1a  16061  gausslemma2dlem1f1o  16063  gausslemma2dlem4  16067  lgseisenlem1  16073  lgseisenlem2  16074  lgsquadlem1  16080  lgsquadlem2  16081  lgsquad2lem2  16085  2sqlem8  16126  2sqlem9  16127  structiedg0val  16165  ausgrumgrien  16295  usgredgreu  16341  uspgredg2vtxeu  16343  uspgredg2v  16346  usgredg2v  16349  usgr1e  16366  subuhgr  16397  subupgr  16398  subumgr  16399  subusgr  16400  vdegp1aid  16439  trlres  16515  clwwlkbp  16520  clwwlkccatlem  16525  s2elclwwlknon2  16561  clwwlknonex2lem2  16563  clwwlknonex2e  16565  bj-charfundcALT  16719  bj-nnord  16868  bj-inf2vnlem1  16880  pwf1oexmid  16913  nnsf  16923  nninfall  16927  nninfself  16931  exmidsbthrlem  16942  qdencn  16947