Theorem sylanbrc 421

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 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  dcand  945  ecase2d  1392  sb2  1820  sbequ1  1821  sbidm  1904  eqeu  2996  euind  3013  reuind  3031  eldifd  3230  eqssd  3265  ssrabdv  3327  elind  3414  dcun  3637  opm  4376  issod  4466  ordsucim  4649  onintonm  4666  ordtri2or2exmidlem  4675  en2lp  4703  ordwe  4725  sosng  4850  sotri2  5188  sotri3  5189  relssdmrn  5311  funun  5425  fnsng  5431  fnprg  5439  fntpg  5440  fntp  5441  fununi  5452  imain  5466  fnco  5494  f00  5587  f1ss  5607  f1ssr  5608  f1ssres  5610  f1f1orn  5653  foimacnv  5660  foun  5661  fun11iun  5663  sefvex  5719  dff3im  5856  fmpt  5861  ffnfv  5869  fmpt2d  5873  ffvresb  5874  fprg  5901  foco2  5962  fcof1  5992  fcofo  5993  fcof1o  5998  fliftf  6008  isoini2  6028  f1oiso  6035  moriotass  6072  fnoprabg  6192  f1ocnvd  6295  f1o3d  6301  suppssov1  6302  1stcof  6401  2ndcof  6402  1stconst  6461  2ndconst  6462  fo2ndf  6467  f1o2ndf1  6468  f1od2  6475  suppssfvg  6507  smores2  6570  tfrlem5  6590  tfrlemibfn  6604  tfr1onlembfn  6620  tfri1dALT  6627  tfrcllembfn  6633  nntri2  6772  eroveu  6905  elixpsn  7023  dom2lem  7064  xpf1o  7150  fidifsnen  7178  finexdc  7213  elssdc  7215  unfidisj  7235  f1finf1o  7271  fidcenumlemrks  7277  sbthlemi9  7289  supeuti  7340  infeuti  7375  casef1  7436  caseinl  7437  caseinr  7438  difinfsnlem  7445  ctmlemr  7454  ctm  7455  ctssdclemn0  7456  ctssdccl  7457  ctssdc  7459  enumctlemm  7460  nnnninf  7472  nninfwlpoimlemg  7521  en2other2  7554  exmidfodomrlemim  7559  pw1if  7590  pw1nel3  7596  dftap2  7623  cc2lem  7638  cc4f  7641  addclpi  7700  mulclpi  7701  nnppipi  7716  recmulnqg  7764  enq0ref  7806  nqnq0pi  7811  genipv  7882  addclpr  7910  nqprxx  7919  prmuloc  7939  mulclpr  7945  distrlem1prl  7955  distrlem1pru  7956  ltexprlempr  7981  ltexprlemrl  7983  ltexprlemru  7985  lteupri  7990  recexprlempr  8005  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemloc  8025  cauappcvgprlemcl  8026  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlem2  8033  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemloc  8048  caucvgprlemcl  8049  caucvgprlemladdfu  8050  caucvgprlem2  8053  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemopu  8072  caucvgprprlemupu  8073  caucvgprprlemloc  8076  caucvgprprlemcl  8077  caucvgprprlem2  8083  suplocexprlemex  8095  suplocsrlem  8181  elrealeu  8202  rereceu  8262  axpre-suploclemres  8274  negf1o  8716  aptap  8986  receuap  9007  divvalap  9012  cju  9299  nn0ge2m1nn  9636  nnnegz  9656  elnnz  9663  elnn0z  9666  peano2z  9689  nn0n0n1ge2  9724  msqznn  9756  eluzaddi  9964  eluzsubi  9965  uzind4  10003  supinfneg  10010  infsupneg  10011  elnn1uz2  10022  uz2mulcl  10023  divfnzn  10036  nnrp  10080  rpaddcl  10094  rpmulcl  10095  rpdivcl  10096  rpgecl  10099  ge0p1rp  10102  elrpd  10110  ge0addcl  10399  ge0mulcl  10400  ge0xaddcl  10401  icoshftf1o  10409  peano2fzr  10457  uzsubsubfz  10468  fzsplit2  10471  fzsplit3  10474  elfznn  10476  fzss1  10485  fzss2  10486  fzp1elp1  10498  elfz1b  10513  elfz0fzfz0  10549  fz0fzelfz0  10550  difelfznle  10558  elfzofz  10586  nn0p1elfzo  10610  fzosplitsnm1  10643  ubmelm1fzo  10660  fzofzp1b  10662  fzosplitsn  10667  zsupcllemstep  10678  zsupcl  10680  infssfzcldc  10685  infssfzledc  10686  exbtwnz  10701  flqge0nn0  10748  flqge1nn  10749  zmodcl  10801  modqmuladdnn0  10825  modsumfzodifsn  10853  frec2uzf1od  10863  frec2uzisod  10864  frecuzrdgrrn  10865  frec2uzrdg  10866  frecuzrdgrcl  10867  frecuzrdgtcl  10869  frecuzrdgsuc  10871  frecuzrdgrclt  10872  frecuzrdgfunlem  10876  frecuzrdgtclt  10878  frecuzrdgsuctlem  10880  uzennn  10893  seq3fveq2  10932  seqfveq2g  10934  monoord  10942  iseqf1olemqcl  10956  iseqf1olemnab  10958  iseqf1olemab  10959  iseqf1olemqf1o  10963  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3id2  10983  exp3val  10998  expcl2lemap  11008  expclzaplem  11020  expge0  11032  expge1  11033  zsqcl2  11074  bcval4  11211  bcn1  11217  bccl2  11227  hashennnuni  11239  hashunlem  11265  hashdifpr  11282  zfz1isolem1  11313  seq3coll  11315  iswrdiz  11332  ccatsymb  11391  ccatrn  11398  ccat2s1fvwd  11436  swrds1  11461  swrdccat2  11464  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12lem3  11525  pfxccatin12  11526  pfxccat3  11527  pfxccat3a  11531  shftfn  11610  shftf  11616  recvguniq  11782  resqrexlemdecn  11799  rersqreu  11815  nn0abscl  11873  nnabscl  11888  abs2dif  11894  nn0maxcl  12013  fiidxsupcl  12017  climuni  12083  2clim  12091  climcn2  12099  summodclem2a  12172  fsum3  12178  fsum3cvg3  12187  fsumcl2lem  12189  fsumadd  12197  fisum0diag2  12238  fsummulc2  12239  fsumge0  12250  geolim2  12303  cvgratnnlemabsle  12318  cvgratz  12323  mertenslemi1  12326  prodmodclem3  12366  prodmodclem2a  12367  fprodeq0  12408  fprodge0  12428  eff2  12471  tanvalap  12499  zdvdsdc  12603  fzo0dvdseq  12648  oexpneg  12668  oddge22np1  12672  evennn02n  12673  evennn2n  12674  nno  12697  divalglemeunn  12712  divalglemex  12713  divalglemeuneg  12714  divalg  12715  bitsfzolem  12745  bitsinv1lem  12752  divgcdz  12772  bezoutlemmain  12799  bezoutlemmo  12807  bezoutlemeu  12808  bezoutlemle  12809  sqgcd  12830  uzwodc  12838  nninfctlemfo  12841  eucalgval2  12855  eucalglt  12859  lcmneg  12876  lcmgcdlem  12879  ncoprmgcdne1b  12891  prmind2  12922  prmdc  12932  sqnprm  12939  isprm5lem  12944  isprm5  12945  isprm6  12950  sqrt2irrlem  12964  pwbdvdseu  12971  sqpweven  12979  2sqpwodd  12980  sqrt2irrap  12984  qgt0numnn  13003  nn0sqdcq  13012  phicl2  13020  crth  13030  phimullem  13031  eulerthlem1  13033  eulerthlemh  13037  eulerthlemth  13038  hashgcdlem  13044  oddprm  13066  pythagtriplem6  13077  pythagtriplem11  13081  pythagtriplem13  13083  pythagtriplem19  13089  pclem0  13093  pcpremul  13100  pceu  13102  pc2dvds  13137  difsqpwdvds  13145  pcadd  13147  pockthlem  13163  pockthg  13164  1arith  13174  4sqlemffi  13203  4sqlem11  13208  4sqlem12  13209  4sqlem13m  13210  4sqlem14  13211  4sqlem17  13214  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemrc  13331  ballotfilemth  13338  oddennn  13340  evenennn  13341  ennnfoneleminc  13359  ennnfonelemf1  13366  ennnfonelemen  13369  exmidunben  13374  ctinf  13378  ctiunctlemfo  13387  nninfdclemlt  13399  nninfdclemf1  13400  ptex  13676  imasaddfnlemg  13693  imasaddflemg  13695  mgmsscl  13739  sgrp0  13783  sgrp1  13784  hashfinmndnn  13803  ismndd  13808  mndpfo  13809  mhmf1o  13835  0mhm  13851  resmhm  13852  resmhm2  13853  resmhm2b  13854  mhmco  13855  gsumvallem2  13858  isgrpd2e  13883  grpinvf1o  13933  grpinvnzcl  13935  dfgrp3m  13962  mhmmnd  13977  ghmgrp  13979  mulgval  13983  mulgfng  13985  subgmulg  14049  issubg4m  14054  isnsg3  14068  nmzsubg  14071  ssnmz  14072  0nsg  14075  nsgid  14076  ghmnsgima  14129  ghmnsgpreima  14130  ghmf1  14134  kerf1ghm  14135  ghmf1o  14136  conjnmzb  14141  cntrsubgnsg  14174  isabld  14191  cmnsubm  14201  ghmcmn  14220  ghmabl  14221  invghm  14222  gsumvalfi  14241  srgfcl  14383  srglmhm  14403  srgrmhm  14404  iscrngd  14453  ringsrg  14458  unitabl  14532  rhmf1o  14583  rhmco  14589  ringelnzr  14602  subrngringnsg  14621  subrgcrng  14641  subrgnzr  14658  resrhm  14664  unitrrg  14684  aprnzr  14707  aprlring  14708  drngnzr  14727  lssneln0  14819  rnglidlmsgrp  14942  quscrng  14978  expghmap  15050  mulgghm2  15051  znf1o  15094  znidom  15100  znidomb  15101  isassad  15119  psrbaglesuppg  15170  psrbagcon  15174  psrbaglefifi  15175  psrbagmaxlem1  15178  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  gsumbagdiaglem  15184  gsumbagdiagfi  15185  psrass1filem  15186  mvrf1fi  15219  mvrclfi  15226  mplsubgfilemm  15231  mplsubgfilemcl  15232  mplsubgfileminv  15233  tgtopon  15309  distopon  15330  epttop  15333  resttopon  15414  resttopon2  15421  cnco  15464  lmss  15489  txtopon  15505  uptx  15517  txdis1cn  15521  hmeocnv  15550  hmeof1o2  15551  hmeores  15558  hmeoco  15559  idhmeo  15560  txhmeo  15562  txswaphmeo  15564  psmetxrge0  15575  isxmet2d  15591  metres2  15624  xmetresbl  15683  comet  15742  bdxmet  15744  bdmet  15745  tgioo  15797  mulc1cncf  15832  mulcncflem  15850  cnrehmeocntop  15853  cnopnap  15854  dedekindeu  15866  dedekindicclemicc  15875  ivthinclemlm  15877  ivthinclemum  15878  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemloc  15884  ivthinc  15886  ivthreinc  15888  dvfgg  15931  dvcjbr  15951  dvcj  15952  dvfre  15953  elplyr  15983  plyreres  16007  rplogbval  16198  ppiqsval  16257  ppiqsval2  16258  ppiqfi  16259  sgmnncl  16274  chtdif  16281  ppidif  16286  ppiqnncl  16295  mpodvdsmulf1o  16301  mersenne  16314  perfectlem2  16317  bcmono  16321  bposlem1  16328  bposlem3  16330  bposlem4  16331  bposlem5  16332  bposlem6  16333  bposlem9  16336  lgsfcl2  16347  lgsval2lem  16351  lgsmod  16367  lgsdirprm  16375  lgsne0  16379  gausslemma2dlem0h  16397  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  gausslemma2dlem4  16405  lgseisenlem1  16411  lgseisenlem2  16412  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem2  16423  2sqlem8  16464  2sqlem9  16465  structiedg0val  16503  ausgrumgrien  16633  usgredgreu  16679  uspgredg2vtxeu  16681  uspgredg2v  16684  usgredg2v  16687  usgr1e  16704  subuhgr  16735  subupgr  16736  subumgr  16737  subusgr  16738  vdegp1aid  16777  trlres  16853  clwwlkbp  16858  clwwlkccatlem  16863  s2elclwwlknon2  16899  clwwlknonex2lem2  16901  clwwlknonex2e  16903  bj-charfundcALT  17057  bj-nnord  17206  bj-inf2vnlem1  17218  pwf1oexmid  17251  idjudju  17269  nnsf  17271  nninfall  17275  nninfself  17279  exmidsbthrlem  17290  qdencn  17295  alsd  17355  ralsd  17356  alseud  17391  ralseud  17392