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  1815  sbequ1  1816  sbidm  1899  eqeu  2977  euind  2994  reuind  3012  eldifd  3211  eqssd  3245  ssrabdv  3307  elind  3394  dcun  3606  opm  4332  issod  4422  ordsucim  4604  onintonm  4621  ordtri2or2exmidlem  4630  en2lp  4658  ordwe  4680  sosng  4805  sotri2  5141  sotri3  5142  relssdmrn  5264  funun  5378  fnsng  5384  fnprg  5392  fntpg  5393  fntp  5394  fununi  5405  imain  5419  fnco  5447  f00  5537  f1ss  5557  f1ssr  5558  f1ssres  5560  f1f1orn  5603  foimacnv  5610  foun  5611  fun11iun  5613  sefvex  5669  dff3im  5800  fmpt  5805  ffnfv  5813  fmpt2d  5817  ffvresb  5818  fprg  5845  foco2  5904  fcof1  5934  fcofo  5935  fcof1o  5940  fliftf  5950  isoini2  5970  f1oiso  5977  moriotass  6012  fnoprabg  6132  f1ocnvd  6235  suppssov1  6241  1stcof  6335  2ndcof  6336  1stconst  6395  2ndconst  6396  fo2ndf  6401  f1o2ndf1  6402  f1od2  6409  suppssfvg  6441  smores2  6503  tfrlem5  6523  tfrlemibfn  6537  tfr1onlembfn  6553  tfri1dALT  6560  tfrcllembfn  6566  nntri2  6705  eroveu  6838  elixpsn  6947  dom2lem  6988  xpf1o  7073  fidifsnen  7100  finexdc  7135  elssdc  7137  unfidisj  7157  f1finf1o  7189  fidcenumlemrks  7195  sbthlemi9  7207  supeuti  7236  infeuti  7271  casef1  7332  caseinl  7333  caseinr  7334  difinfsnlem  7341  ctmlemr  7350  ctm  7351  ctssdclemn0  7352  ctssdccl  7353  ctssdc  7355  enumctlemm  7356  nnnninf  7368  nninfwlpoimlemg  7417  en2other2  7450  exmidfodomrlemim  7455  pw1if  7486  pw1nel3  7492  dftap2  7513  cc2lem  7528  cc4f  7531  addclpi  7590  mulclpi  7591  nnppipi  7606  recmulnqg  7654  enq0ref  7696  nqnq0pi  7701  genipv  7772  addclpr  7800  nqprxx  7809  prmuloc  7829  mulclpr  7835  distrlem1prl  7845  distrlem1pru  7846  ltexprlempr  7871  ltexprlemrl  7873  ltexprlemru  7875  lteupri  7880  recexprlempr  7895  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemlol  7910  cauappcvgprlemopu  7911  cauappcvgprlemupu  7912  cauappcvgprlemloc  7915  cauappcvgprlemcl  7916  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlem2  7923  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemopu  7934  caucvgprlemupu  7935  caucvgprlemloc  7938  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlem2  7943  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemupu  7963  caucvgprprlemloc  7966  caucvgprprlemcl  7967  caucvgprprlem2  7973  suplocexprlemex  7985  suplocsrlem  8071  elrealeu  8092  rereceu  8152  axpre-suploclemres  8164  negf1o  8604  aptap  8873  receuap  8892  divvalap  8897  cju  9184  nn0ge2m1nn  9505  nnnegz  9525  elnnz  9532  elnn0z  9535  peano2z  9558  nn0n0n1ge2  9593  msqznn  9623  eluzaddi  9826  eluzsubi  9827  uzind4  9865  supinfneg  9872  infsupneg  9873  elnn1uz2  9884  uz2mulcl  9885  divfnzn  9898  nnrp  9941  rpaddcl  9955  rpmulcl  9956  rpdivcl  9957  rpgecl  9960  ge0p1rp  9963  elrpd  9971  ge0addcl  10259  ge0mulcl  10260  ge0xaddcl  10261  icoshftf1o  10269  peano2fzr  10315  uzsubsubfz  10325  fzsplit2  10328  elfznn  10332  fzss1  10341  fzss2  10342  fzp1elp1  10353  elfz1b  10368  elfz0fzfz0  10404  fz0fzelfz0  10405  difelfznle  10413  elfzofz  10441  nn0p1elfzo  10465  fzosplitsnm1  10498  ubmelm1fzo  10515  fzofzp1b  10517  fzosplitsn  10522  zsupcllemstep  10533  zsupcl  10535  exbtwnz  10554  flqge0nn0  10597  flqge1nn  10598  zmodcl  10650  modqmuladdnn0  10674  modsumfzodifsn  10702  frec2uzf1od  10712  frec2uzisod  10713  frecuzrdgrrn  10714  frec2uzrdg  10715  frecuzrdgrcl  10716  frecuzrdgtcl  10718  frecuzrdgsuc  10720  frecuzrdgrclt  10721  frecuzrdgfunlem  10725  frecuzrdgtclt  10727  frecuzrdgsuctlem  10729  uzennn  10742  seq3fveq2  10781  seqfveq2g  10783  monoord  10791  iseqf1olemqcl  10805  iseqf1olemnab  10807  iseqf1olemab  10808  iseqf1olemqf1o  10812  seq3f1olemqsumkj  10817  seq3f1olemqsumk  10818  seq3id2  10832  exp3val  10847  expcl2lemap  10857  expclzaplem  10869  expge0  10881  expge1  10882  zsqcl2  10923  bcval4  11058  bcn1  11064  bccl2  11074  hashennnuni  11085  hashunlem  11111  hashdifpr  11128  zfz1isolem1  11148  seq3coll  11150  iswrdiz  11167  ccatsymb  11226  ccatrn  11233  ccat2s1fvwd  11271  swrds1  11296  swrdccat2  11299  swrdccatin2  11357  pfxccatin12lem2  11359  pfxccatin12lem3  11360  pfxccatin12  11361  pfxccat3  11362  pfxccat3a  11366  shftfn  11445  shftf  11451  recvguniq  11616  resqrexlemdecn  11633  rersqreu  11649  nn0abscl  11706  nnabscl  11721  abs2dif  11727  nn0maxcl  11846  climuni  11914  2clim  11922  climcn2  11930  summodclem2a  12003  fsum3  12009  fsum3cvg3  12018  fsumcl2lem  12020  fsumadd  12028  fisum0diag2  12069  fsummulc2  12070  fsumge0  12081  geolim2  12134  cvgratnnlemabsle  12149  cvgratz  12154  mertenslemi1  12157  prodmodclem3  12197  prodmodclem2a  12198  fprodeq0  12239  fprodge0  12259  eff2  12302  tanvalap  12330  zdvdsdc  12434  fzo0dvdseq  12479  oexpneg  12499  oddge22np1  12503  evennn02n  12504  evennn2n  12505  nno  12528  divalglemeunn  12543  divalglemex  12544  divalglemeuneg  12545  divalg  12546  bitsfzolem  12576  bitsinv1lem  12583  divgcdz  12603  bezoutlemmain  12630  bezoutlemmo  12638  bezoutlemeu  12639  bezoutlemle  12640  sqgcd  12661  uzwodc  12669  nninfctlemfo  12672  eucalgval2  12686  eucalglt  12690  lcmneg  12707  lcmgcdlem  12710  ncoprmgcdne1b  12722  prmind2  12753  prmdc  12763  sqnprm  12769  isprm5lem  12774  isprm5  12775  isprm6  12780  sqrt2irrlem  12794  pw2dvdseu  12801  sqpweven  12808  2sqpwodd  12809  sqrt2irrap  12813  qgt0numnn  12832  phicl2  12847  hashdvds  12854  crth  12857  phimullem  12858  eulerthlem1  12860  eulerthlemh  12864  eulerthlemth  12865  hashgcdlem  12871  oddprm  12893  pythagtriplem6  12904  pythagtriplem11  12908  pythagtriplem13  12910  pythagtriplem19  12916  pclem0  12920  pcpremul  12927  pceu  12929  pc2dvds  12964  difsqpwdvds  12972  pcadd  12974  pockthlem  12990  pockthg  12991  1arith  13001  4sqlemffi  13030  4sqlem11  13035  4sqlem12  13036  4sqlem13m  13037  4sqlem14  13038  4sqlem17  13041  oddennn  13074  evenennn  13075  ennnfoneleminc  13093  ennnfonelemf1  13100  ennnfonelemen  13103  exmidunben  13108  ctinf  13112  ctiunctlemfo  13121  nninfdclemlt  13133  nninfdclemf1  13134  ptex  13408  imasaddfnlemg  13458  imasaddflemg  13460  mgmsscl  13505  sgrp0  13554  sgrp1  13555  hashfinmndnn  13576  ismndd  13581  mndpfo  13582  mhmf1o  13614  0mhm  13630  resmhm  13631  resmhm2  13632  resmhm2b  13633  mhmco  13634  gsumvallem2  13637  isgrpd2e  13664  grpinvf1o  13714  grpinvnzcl  13716  dfgrp3m  13743  mhmmnd  13764  ghmgrp  13766  mulgval  13770  mulgfng  13772  subgmulg  13836  issubg4m  13841  isnsg3  13855  nmzsubg  13858  ssnmz  13859  0nsg  13862  nsgid  13863  ghmnsgima  13916  ghmnsgpreima  13917  ghmf1  13921  kerf1ghm  13922  ghmf1o  13923  conjnmzb  13928  isabld  13947  ghmcmn  13975  ghmabl  13976  invghm  13977  srgfcl  14048  srglmhm  14068  srgrmhm  14069  iscrngd  14117  ringsrg  14122  unitabl  14193  rhmf1o  14244  rhmco  14250  ringelnzr  14263  subrngringnsg  14281  subrgcrng  14301  subrgnzr  14318  resrhm  14324  unitrrg  14343  lssneln0  14450  rnglidlmsgrp  14573  quscrng  14609  expghmap  14683  mulgghm2  14684  znf1o  14727  znidom  14733  znidomb  14734  psrbaglesuppg  14748  psrbagcon  14752  tgtopon  14857  distopon  14878  epttop  14881  resttopon  14962  resttopon2  14969  cnco  15012  lmss  15037  txtopon  15053  uptx  15065  txdis1cn  15069  hmeocnv  15098  hmeof1o2  15099  hmeores  15106  hmeoco  15107  idhmeo  15108  txhmeo  15110  txswaphmeo  15112  psmetxrge0  15123  isxmet2d  15139  metres2  15172  xmetresbl  15231  comet  15290  bdxmet  15292  bdmet  15293  tgioo  15345  mulc1cncf  15380  mulcncflem  15398  cnrehmeocntop  15401  cnopnap  15402  dedekindeu  15414  dedekindicclemicc  15423  ivthinclemlm  15425  ivthinclemum  15426  ivthinclemlopn  15427  ivthinclemlr  15428  ivthinclemuopn  15429  ivthinclemur  15430  ivthinclemloc  15432  ivthinc  15434  ivthreinc  15436  dvfgg  15479  dvcjbr  15499  dvcj  15500  dvfre  15501  elplyr  15531  plyreres  15555  rplogbval  15736  sgmnncl  15782  mpodvdsmulf1o  15784  mersenne  15791  perfectlem2  15794  lgsfcl2  15805  lgsval2lem  15809  lgsmod  15825  lgsdirprm  15833  lgsne0  15837  gausslemma2dlem0h  15855  gausslemma2dlem1a  15857  gausslemma2dlem1f1o  15859  gausslemma2dlem4  15863  lgseisenlem1  15869  lgseisenlem2  15870  lgsquadlem1  15876  lgsquadlem2  15877  lgsquad2lem2  15881  2sqlem8  15922  2sqlem9  15923  structiedg0val  15961  ausgrumgrien  16091  usgredgreu  16137  uspgredg2vtxeu  16139  uspgredg2v  16142  usgredg2v  16145  usgr1e  16162  subuhgr  16193  subupgr  16194  subumgr  16195  subusgr  16196  vdegp1aid  16235  trlres  16311  clwwlkbp  16316  clwwlkccatlem  16321  s2elclwwlknon2  16357  clwwlknonex2lem2  16359  clwwlknonex2e  16361  bj-charfundcALT  16505  bj-nnord  16654  bj-inf2vnlem1  16666  pwf1oexmid  16701  nnsf  16711  nninfall  16715  nninfself  16719  exmidsbthrlem  16730  qdencn  16735  gfsumval  16789