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  938  ecase2d  1385  sb2  1813  sbequ1  1814  sbidm  1897  eqeu  2973  euind  2990  reuind  3008  eldifd  3207  eqssd  3241  ssrabdv  3303  elind  3389  dcun  3601  opm  4321  issod  4411  ordsucim  4593  onintonm  4610  ordtri2or2exmidlem  4619  en2lp  4647  ordwe  4669  sosng  4794  sotri2  5129  sotri3  5130  relssdmrn  5252  funun  5365  fnsng  5371  fnprg  5379  fntpg  5380  fntp  5381  fununi  5392  imain  5406  fnco  5434  f00  5522  f1ss  5542  f1ssr  5543  f1ssres  5545  f1f1orn  5588  foimacnv  5595  foun  5596  fun11iun  5598  sefvex  5653  dff3im  5785  fmpt  5790  ffnfv  5798  fmpt2d  5802  ffvresb  5803  fprg  5829  foco2  5886  fcof1  5916  fcofo  5917  fcof1o  5922  fliftf  5932  isoini2  5952  f1oiso  5959  moriotass  5994  fnoprabg  6114  f1ocnvd  6217  suppssfv  6223  suppssov1  6224  1stcof  6318  2ndcof  6319  1stconst  6378  2ndconst  6379  fo2ndf  6384  f1o2ndf1  6385  f1od2  6392  smores2  6451  tfrlem5  6471  tfrlemibfn  6485  tfr1onlembfn  6501  tfri1dALT  6508  tfrcllembfn  6514  nntri2  6653  eroveu  6786  elixpsn  6895  dom2lem  6936  xpf1o  7018  fidifsnen  7045  finexdc  7078  elssdc  7080  unfidisj  7100  f1finf1o  7130  fidcenumlemrks  7136  sbthlemi9  7148  supeuti  7177  infeuti  7212  casef1  7273  caseinl  7274  caseinr  7275  difinfsnlem  7282  ctmlemr  7291  ctm  7292  ctssdclemn0  7293  ctssdccl  7294  ctssdc  7296  enumctlemm  7297  nnnninf  7309  nninfwlpoimlemg  7358  en2other2  7390  exmidfodomrlemim  7395  pw1if  7426  pw1nel3  7432  dftap2  7453  cc2lem  7468  cc4f  7471  addclpi  7530  mulclpi  7531  nnppipi  7546  recmulnqg  7594  enq0ref  7636  nqnq0pi  7641  genipv  7712  addclpr  7740  nqprxx  7749  prmuloc  7769  mulclpr  7775  distrlem1prl  7785  distrlem1pru  7786  ltexprlempr  7811  ltexprlemrl  7813  ltexprlemru  7815  lteupri  7820  recexprlempr  7835  cauappcvgprlemm  7848  cauappcvgprlemopl  7849  cauappcvgprlemlol  7850  cauappcvgprlemopu  7851  cauappcvgprlemupu  7852  cauappcvgprlemloc  7855  cauappcvgprlemcl  7856  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  cauappcvgprlem2  7863  caucvgprlemm  7871  caucvgprlemopl  7872  caucvgprlemlol  7873  caucvgprlemopu  7874  caucvgprlemupu  7875  caucvgprlemloc  7878  caucvgprlemcl  7879  caucvgprlemladdfu  7880  caucvgprlem2  7883  caucvgprprlemml  7897  caucvgprprlemmu  7898  caucvgprprlemopl  7900  caucvgprprlemlol  7901  caucvgprprlemopu  7902  caucvgprprlemupu  7903  caucvgprprlemloc  7906  caucvgprprlemcl  7907  caucvgprprlem2  7913  suplocexprlemex  7925  suplocsrlem  8011  elrealeu  8032  rereceu  8092  axpre-suploclemres  8104  negf1o  8544  aptap  8813  receuap  8832  divvalap  8837  cju  9124  nn0ge2m1nn  9445  nnnegz  9465  elnnz  9472  elnn0z  9475  peano2z  9498  nn0n0n1ge2  9533  msqznn  9563  eluzaddi  9766  eluzsubi  9767  uzind4  9800  supinfneg  9807  infsupneg  9808  elnn1uz2  9819  uz2mulcl  9820  divfnzn  9833  nnrp  9876  rpaddcl  9890  rpmulcl  9891  rpdivcl  9892  rpgecl  9895  ge0p1rp  9898  elrpd  9906  ge0addcl  10194  ge0mulcl  10195  ge0xaddcl  10196  icoshftf1o  10204  peano2fzr  10250  uzsubsubfz  10260  fzsplit2  10263  elfznn  10267  fzss1  10276  fzss2  10277  fzp1elp1  10288  elfz1b  10303  elfz0fzfz0  10339  fz0fzelfz0  10340  difelfznle  10348  elfzofz  10376  fzosplitsnm1  10432  ubmelm1fzo  10449  fzofzp1b  10451  fzosplitsn  10456  zsupcllemstep  10466  zsupcl  10468  exbtwnz  10487  flqge0nn0  10530  flqge1nn  10531  zmodcl  10583  modqmuladdnn0  10607  modsumfzodifsn  10635  frec2uzf1od  10645  frec2uzisod  10646  frecuzrdgrrn  10647  frec2uzrdg  10648  frecuzrdgrcl  10649  frecuzrdgtcl  10651  frecuzrdgsuc  10653  frecuzrdgrclt  10654  frecuzrdgfunlem  10658  frecuzrdgtclt  10660  frecuzrdgsuctlem  10662  uzennn  10675  seq3fveq2  10714  seqfveq2g  10716  monoord  10724  iseqf1olemqcl  10738  iseqf1olemnab  10740  iseqf1olemab  10741  iseqf1olemqf1o  10745  seq3f1olemqsumkj  10750  seq3f1olemqsumk  10751  seq3id2  10765  exp3val  10780  expcl2lemap  10790  expclzaplem  10802  expge0  10814  expge1  10815  zsqcl2  10856  bcval4  10991  bcn1  10997  bccl2  11007  hashennnuni  11018  hashunlem  11043  hashdifpr  11060  zfz1isolem1  11080  seq3coll  11082  iswrdiz  11096  ccatsymb  11155  ccatrn  11162  swrds1  11221  swrdccat2  11224  swrdccatin2  11282  pfxccatin12lem2  11284  pfxccatin12lem3  11285  pfxccatin12  11286  pfxccat3  11287  pfxccat3a  11291  shftfn  11356  shftf  11362  recvguniq  11527  resqrexlemdecn  11544  rersqreu  11560  nn0abscl  11617  nnabscl  11632  abs2dif  11638  nn0maxcl  11757  climuni  11825  2clim  11833  climcn2  11841  summodclem2a  11913  fsum3  11919  fsum3cvg3  11928  fsumcl2lem  11930  fsumadd  11938  fisum0diag2  11979  fsummulc2  11980  fsumge0  11991  geolim2  12044  cvgratnnlemabsle  12059  cvgratz  12064  mertenslemi1  12067  prodmodclem3  12107  prodmodclem2a  12108  fprodeq0  12149  fprodge0  12169  eff2  12212  tanvalap  12240  zdvdsdc  12344  fzo0dvdseq  12389  oexpneg  12409  oddge22np1  12413  evennn02n  12414  evennn2n  12415  nno  12438  divalglemeunn  12453  divalglemex  12454  divalglemeuneg  12455  divalg  12456  bitsfzolem  12486  bitsinv1lem  12493  divgcdz  12513  bezoutlemmain  12540  bezoutlemmo  12548  bezoutlemeu  12549  bezoutlemle  12550  sqgcd  12571  uzwodc  12579  nninfctlemfo  12582  eucalgval2  12596  eucalglt  12600  lcmneg  12617  lcmgcdlem  12620  ncoprmgcdne1b  12632  prmind2  12663  prmdc  12673  sqnprm  12679  isprm5lem  12684  isprm5  12685  isprm6  12690  sqrt2irrlem  12704  pw2dvdseu  12711  sqpweven  12718  2sqpwodd  12719  sqrt2irrap  12723  qgt0numnn  12742  phicl2  12757  hashdvds  12764  crth  12767  phimullem  12768  eulerthlem1  12770  eulerthlemh  12774  eulerthlemth  12775  hashgcdlem  12781  oddprm  12803  pythagtriplem6  12814  pythagtriplem11  12818  pythagtriplem13  12820  pythagtriplem19  12826  pclem0  12830  pcpremul  12837  pceu  12839  pc2dvds  12874  difsqpwdvds  12882  pcadd  12884  pockthlem  12900  pockthg  12901  1arith  12911  4sqlemffi  12940  4sqlem11  12945  4sqlem12  12946  4sqlem13m  12947  4sqlem14  12948  4sqlem17  12951  oddennn  12984  evenennn  12985  ennnfoneleminc  13003  ennnfonelemf1  13010  ennnfonelemen  13013  exmidunben  13018  ctinf  13022  ctiunctlemfo  13031  nninfdclemlt  13043  nninfdclemf1  13044  ptex  13318  imasaddfnlemg  13368  imasaddflemg  13370  mgmsscl  13415  sgrp0  13464  sgrp1  13465  hashfinmndnn  13486  ismndd  13491  mndpfo  13492  mhmf1o  13524  0mhm  13540  resmhm  13541  resmhm2  13542  resmhm2b  13543  mhmco  13544  gsumvallem2  13547  isgrpd2e  13574  grpinvf1o  13624  grpinvnzcl  13626  dfgrp3m  13653  mhmmnd  13674  ghmgrp  13676  mulgval  13680  mulgfng  13682  subgmulg  13746  issubg4m  13751  isnsg3  13765  nmzsubg  13768  ssnmz  13769  0nsg  13772  nsgid  13773  ghmnsgima  13826  ghmnsgpreima  13827  ghmf1  13831  kerf1ghm  13832  ghmf1o  13833  conjnmzb  13838  isabld  13857  ghmcmn  13885  ghmabl  13886  invghm  13887  srgfcl  13957  srglmhm  13977  srgrmhm  13978  iscrngd  14026  ringsrg  14031  unitabl  14102  rhmf1o  14153  rhmco  14159  ringelnzr  14172  subrngringnsg  14190  subrgcrng  14210  subrgnzr  14227  resrhm  14233  unitrrg  14252  lssneln0  14359  rnglidlmsgrp  14482  quscrng  14518  expghmap  14592  mulgghm2  14593  znf1o  14636  znidom  14642  znidomb  14643  psrbaglesuppg  14657  tgtopon  14761  distopon  14782  epttop  14785  resttopon  14866  resttopon2  14873  cnco  14916  lmss  14941  txtopon  14957  uptx  14969  txdis1cn  14973  hmeocnv  15002  hmeof1o2  15003  hmeores  15010  hmeoco  15011  idhmeo  15012  txhmeo  15014  txswaphmeo  15016  psmetxrge0  15027  isxmet2d  15043  metres2  15076  xmetresbl  15135  comet  15194  bdxmet  15196  bdmet  15197  tgioo  15249  mulc1cncf  15284  mulcncflem  15302  cnrehmeocntop  15305  cnopnap  15306  dedekindeu  15318  dedekindicclemicc  15327  ivthinclemlm  15329  ivthinclemum  15330  ivthinclemlopn  15331  ivthinclemlr  15332  ivthinclemuopn  15333  ivthinclemur  15334  ivthinclemloc  15336  ivthinc  15338  ivthreinc  15340  dvfgg  15383  dvcjbr  15403  dvcj  15404  dvfre  15405  elplyr  15435  plyreres  15459  rplogbval  15640  sgmnncl  15683  mpodvdsmulf1o  15685  mersenne  15692  perfectlem2  15695  lgsfcl2  15706  lgsval2lem  15710  lgsmod  15726  lgsdirprm  15734  lgsne0  15738  gausslemma2dlem0h  15756  gausslemma2dlem1a  15758  gausslemma2dlem1f1o  15760  gausslemma2dlem4  15764  lgseisenlem1  15770  lgseisenlem2  15771  lgsquadlem1  15777  lgsquadlem2  15778  lgsquad2lem2  15782  2sqlem8  15823  2sqlem9  15824  structiedg0val  15862  ausgrumgrien  15989  usgredgreu  16035  uspgredg2vtxeu  16037  uspgredg2v  16040  usgredg2v  16043  usgr1e  16060  trlres  16159  clwwlkbp  16164  clwwlkccatlem  16169  bj-charfundcALT  16281  bj-nnord  16430  bj-inf2vnlem1  16442  pwf1oexmid  16478  nnsf  16485  nninfall  16489  nninfself  16493  exmidsbthrlem  16504  qdencn  16509