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  2974  euind  2991  reuind  3009  eldifd  3208  eqssd  3242  ssrabdv  3304  elind  3390  dcun  3602  opm  4324  issod  4414  ordsucim  4596  onintonm  4613  ordtri2or2exmidlem  4622  en2lp  4650  ordwe  4672  sosng  4797  sotri2  5132  sotri3  5133  relssdmrn  5255  funun  5368  fnsng  5374  fnprg  5382  fntpg  5383  fntp  5384  fununi  5395  imain  5409  fnco  5437  f00  5525  f1ss  5545  f1ssr  5546  f1ssres  5548  f1f1orn  5591  foimacnv  5598  foun  5599  fun11iun  5601  sefvex  5656  dff3im  5788  fmpt  5793  ffnfv  5801  fmpt2d  5805  ffvresb  5806  fprg  5832  foco2  5889  fcof1  5919  fcofo  5920  fcof1o  5925  fliftf  5935  isoini2  5955  f1oiso  5962  moriotass  5997  fnoprabg  6117  f1ocnvd  6220  suppssfv  6226  suppssov1  6227  1stcof  6321  2ndcof  6322  1stconst  6381  2ndconst  6382  fo2ndf  6387  f1o2ndf1  6388  f1od2  6395  smores2  6455  tfrlem5  6475  tfrlemibfn  6489  tfr1onlembfn  6505  tfri1dALT  6512  tfrcllembfn  6518  nntri2  6657  eroveu  6790  elixpsn  6899  dom2lem  6940  xpf1o  7025  fidifsnen  7052  finexdc  7087  elssdc  7089  unfidisj  7109  f1finf1o  7140  fidcenumlemrks  7146  sbthlemi9  7158  supeuti  7187  infeuti  7222  casef1  7283  caseinl  7284  caseinr  7285  difinfsnlem  7292  ctmlemr  7301  ctm  7302  ctssdclemn0  7303  ctssdccl  7304  ctssdc  7306  enumctlemm  7307  nnnninf  7319  nninfwlpoimlemg  7368  en2other2  7400  exmidfodomrlemim  7405  pw1if  7436  pw1nel3  7442  dftap2  7463  cc2lem  7478  cc4f  7481  addclpi  7540  mulclpi  7541  nnppipi  7556  recmulnqg  7604  enq0ref  7646  nqnq0pi  7651  genipv  7722  addclpr  7750  nqprxx  7759  prmuloc  7779  mulclpr  7785  distrlem1prl  7795  distrlem1pru  7796  ltexprlempr  7821  ltexprlemrl  7823  ltexprlemru  7825  lteupri  7830  recexprlempr  7845  cauappcvgprlemm  7858  cauappcvgprlemopl  7859  cauappcvgprlemlol  7860  cauappcvgprlemopu  7861  cauappcvgprlemupu  7862  cauappcvgprlemloc  7865  cauappcvgprlemcl  7866  cauappcvgprlemladdfu  7867  cauappcvgprlemladdfl  7868  cauappcvgprlem2  7873  caucvgprlemm  7881  caucvgprlemopl  7882  caucvgprlemlol  7883  caucvgprlemopu  7884  caucvgprlemupu  7885  caucvgprlemloc  7888  caucvgprlemcl  7889  caucvgprlemladdfu  7890  caucvgprlem2  7893  caucvgprprlemml  7907  caucvgprprlemmu  7908  caucvgprprlemopl  7910  caucvgprprlemlol  7911  caucvgprprlemopu  7912  caucvgprprlemupu  7913  caucvgprprlemloc  7916  caucvgprprlemcl  7917  caucvgprprlem2  7923  suplocexprlemex  7935  suplocsrlem  8021  elrealeu  8042  rereceu  8102  axpre-suploclemres  8114  negf1o  8554  aptap  8823  receuap  8842  divvalap  8847  cju  9134  nn0ge2m1nn  9455  nnnegz  9475  elnnz  9482  elnn0z  9485  peano2z  9508  nn0n0n1ge2  9543  msqznn  9573  eluzaddi  9776  eluzsubi  9777  uzind4  9815  supinfneg  9822  infsupneg  9823  elnn1uz2  9834  uz2mulcl  9835  divfnzn  9848  nnrp  9891  rpaddcl  9905  rpmulcl  9906  rpdivcl  9907  rpgecl  9910  ge0p1rp  9913  elrpd  9921  ge0addcl  10209  ge0mulcl  10210  ge0xaddcl  10211  icoshftf1o  10219  peano2fzr  10265  uzsubsubfz  10275  fzsplit2  10278  elfznn  10282  fzss1  10291  fzss2  10292  fzp1elp1  10303  elfz1b  10318  elfz0fzfz0  10354  fz0fzelfz0  10355  difelfznle  10363  elfzofz  10391  fzosplitsnm1  10447  ubmelm1fzo  10464  fzofzp1b  10466  fzosplitsn  10471  zsupcllemstep  10482  zsupcl  10484  exbtwnz  10503  flqge0nn0  10546  flqge1nn  10547  zmodcl  10599  modqmuladdnn0  10623  modsumfzodifsn  10651  frec2uzf1od  10661  frec2uzisod  10662  frecuzrdgrrn  10663  frec2uzrdg  10664  frecuzrdgrcl  10665  frecuzrdgtcl  10667  frecuzrdgsuc  10669  frecuzrdgrclt  10670  frecuzrdgfunlem  10674  frecuzrdgtclt  10676  frecuzrdgsuctlem  10678  uzennn  10691  seq3fveq2  10730  seqfveq2g  10732  monoord  10740  iseqf1olemqcl  10754  iseqf1olemnab  10756  iseqf1olemab  10757  iseqf1olemqf1o  10761  seq3f1olemqsumkj  10766  seq3f1olemqsumk  10767  seq3id2  10781  exp3val  10796  expcl2lemap  10806  expclzaplem  10818  expge0  10830  expge1  10831  zsqcl2  10872  bcval4  11007  bcn1  11013  bccl2  11023  hashennnuni  11034  hashunlem  11060  hashdifpr  11077  zfz1isolem1  11097  seq3coll  11099  iswrdiz  11113  ccatsymb  11172  ccatrn  11179  ccat2s1fvwd  11217  swrds1  11242  swrdccat2  11245  swrdccatin2  11303  pfxccatin12lem2  11305  pfxccatin12lem3  11306  pfxccatin12  11307  pfxccat3  11308  pfxccat3a  11312  shftfn  11378  shftf  11384  recvguniq  11549  resqrexlemdecn  11566  rersqreu  11582  nn0abscl  11639  nnabscl  11654  abs2dif  11660  nn0maxcl  11779  climuni  11847  2clim  11855  climcn2  11863  summodclem2a  11935  fsum3  11941  fsum3cvg3  11950  fsumcl2lem  11952  fsumadd  11960  fisum0diag2  12001  fsummulc2  12002  fsumge0  12013  geolim2  12066  cvgratnnlemabsle  12081  cvgratz  12086  mertenslemi1  12089  prodmodclem3  12129  prodmodclem2a  12130  fprodeq0  12171  fprodge0  12191  eff2  12234  tanvalap  12262  zdvdsdc  12366  fzo0dvdseq  12411  oexpneg  12431  oddge22np1  12435  evennn02n  12436  evennn2n  12437  nno  12460  divalglemeunn  12475  divalglemex  12476  divalglemeuneg  12477  divalg  12478  bitsfzolem  12508  bitsinv1lem  12515  divgcdz  12535  bezoutlemmain  12562  bezoutlemmo  12570  bezoutlemeu  12571  bezoutlemle  12572  sqgcd  12593  uzwodc  12601  nninfctlemfo  12604  eucalgval2  12618  eucalglt  12622  lcmneg  12639  lcmgcdlem  12642  ncoprmgcdne1b  12654  prmind2  12685  prmdc  12695  sqnprm  12701  isprm5lem  12706  isprm5  12707  isprm6  12712  sqrt2irrlem  12726  pw2dvdseu  12733  sqpweven  12740  2sqpwodd  12741  sqrt2irrap  12745  qgt0numnn  12764  phicl2  12779  hashdvds  12786  crth  12789  phimullem  12790  eulerthlem1  12792  eulerthlemh  12796  eulerthlemth  12797  hashgcdlem  12803  oddprm  12825  pythagtriplem6  12836  pythagtriplem11  12840  pythagtriplem13  12842  pythagtriplem19  12848  pclem0  12852  pcpremul  12859  pceu  12861  pc2dvds  12896  difsqpwdvds  12904  pcadd  12906  pockthlem  12922  pockthg  12923  1arith  12933  4sqlemffi  12962  4sqlem11  12967  4sqlem12  12968  4sqlem13m  12969  4sqlem14  12970  4sqlem17  12973  oddennn  13006  evenennn  13007  ennnfoneleminc  13025  ennnfonelemf1  13032  ennnfonelemen  13035  exmidunben  13040  ctinf  13044  ctiunctlemfo  13053  nninfdclemlt  13065  nninfdclemf1  13066  ptex  13340  imasaddfnlemg  13390  imasaddflemg  13392  mgmsscl  13437  sgrp0  13486  sgrp1  13487  hashfinmndnn  13508  ismndd  13513  mndpfo  13514  mhmf1o  13546  0mhm  13562  resmhm  13563  resmhm2  13564  resmhm2b  13565  mhmco  13566  gsumvallem2  13569  isgrpd2e  13596  grpinvf1o  13646  grpinvnzcl  13648  dfgrp3m  13675  mhmmnd  13696  ghmgrp  13698  mulgval  13702  mulgfng  13704  subgmulg  13768  issubg4m  13773  isnsg3  13787  nmzsubg  13790  ssnmz  13791  0nsg  13794  nsgid  13795  ghmnsgima  13848  ghmnsgpreima  13849  ghmf1  13853  kerf1ghm  13854  ghmf1o  13855  conjnmzb  13860  isabld  13879  ghmcmn  13907  ghmabl  13908  invghm  13909  srgfcl  13979  srglmhm  13999  srgrmhm  14000  iscrngd  14048  ringsrg  14053  unitabl  14124  rhmf1o  14175  rhmco  14181  ringelnzr  14194  subrngringnsg  14212  subrgcrng  14232  subrgnzr  14249  resrhm  14255  unitrrg  14274  lssneln0  14381  rnglidlmsgrp  14504  quscrng  14540  expghmap  14614  mulgghm2  14615  znf1o  14658  znidom  14664  znidomb  14665  psrbaglesuppg  14679  tgtopon  14783  distopon  14804  epttop  14807  resttopon  14888  resttopon2  14895  cnco  14938  lmss  14963  txtopon  14979  uptx  14991  txdis1cn  14995  hmeocnv  15024  hmeof1o2  15025  hmeores  15032  hmeoco  15033  idhmeo  15034  txhmeo  15036  txswaphmeo  15038  psmetxrge0  15049  isxmet2d  15065  metres2  15098  xmetresbl  15157  comet  15216  bdxmet  15218  bdmet  15219  tgioo  15271  mulc1cncf  15306  mulcncflem  15324  cnrehmeocntop  15327  cnopnap  15328  dedekindeu  15340  dedekindicclemicc  15349  ivthinclemlm  15351  ivthinclemum  15352  ivthinclemlopn  15353  ivthinclemlr  15354  ivthinclemuopn  15355  ivthinclemur  15356  ivthinclemloc  15358  ivthinc  15360  ivthreinc  15362  dvfgg  15405  dvcjbr  15425  dvcj  15426  dvfre  15427  elplyr  15457  plyreres  15481  rplogbval  15662  sgmnncl  15705  mpodvdsmulf1o  15707  mersenne  15714  perfectlem2  15717  lgsfcl2  15728  lgsval2lem  15732  lgsmod  15748  lgsdirprm  15756  lgsne0  15760  gausslemma2dlem0h  15778  gausslemma2dlem1a  15780  gausslemma2dlem1f1o  15782  gausslemma2dlem4  15786  lgseisenlem1  15792  lgseisenlem2  15793  lgsquadlem1  15799  lgsquadlem2  15800  lgsquad2lem2  15804  2sqlem8  15845  2sqlem9  15846  structiedg0val  15884  ausgrumgrien  16014  usgredgreu  16060  uspgredg2vtxeu  16062  uspgredg2v  16065  usgredg2v  16068  usgr1e  16085  vdegp1aid  16125  trlres  16199  clwwlkbp  16204  clwwlkccatlem  16209  s2elclwwlknon2  16245  clwwlknonex2lem2  16247  clwwlknonex2e  16249  bj-charfundcALT  16354  bj-nnord  16503  bj-inf2vnlem1  16515  pwf1oexmid  16550  nnsf  16557  nninfall  16561  nninfself  16565  exmidsbthrlem  16576  qdencn  16581  gfsumval  16630