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  6569  tfrlem5  6589  tfrlemibfn  6603  tfr1onlembfn  6619  tfri1dALT  6626  tfrcllembfn  6632  nntri2  6771  eroveu  6904  elixpsn  7021  dom2lem  7062  xpf1o  7148  fidifsnen  7176  finexdc  7211  elssdc  7213  unfidisj  7233  f1finf1o  7269  fidcenumlemrks  7275  sbthlemi9  7287  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  9638  nnnegz  9658  elnnz  9665  elnn0z  9668  peano2z  9691  nn0n0n1ge2  9726  msqznn  9757  eluzaddi  9965  eluzsubi  9966  uzind4  10004  supinfneg  10011  infsupneg  10012  elnn1uz2  10023  uz2mulcl  10024  divfnzn  10037  nnrp  10081  rpaddcl  10095  rpmulcl  10096  rpdivcl  10097  rpgecl  10100  ge0p1rp  10103  elrpd  10111  ge0addcl  10400  ge0mulcl  10401  ge0xaddcl  10402  icoshftf1o  10410  peano2fzr  10458  uzsubsubfz  10469  fzsplit2  10472  fzsplit3  10475  elfznn  10477  fzss1  10486  fzss2  10487  fzp1elp1  10499  elfz1b  10514  elfz0fzfz0  10550  fz0fzelfz0  10551  difelfznle  10559  elfzofz  10587  nn0p1elfzo  10611  fzosplitsnm1  10644  ubmelm1fzo  10661  fzofzp1b  10663  fzosplitsn  10668  zsupcllemstep  10679  zsupcl  10681  infssfzcldc  10686  infssfzledc  10687  exbtwnz  10702  flqge0nn0  10749  flqge1nn  10750  zmodcl  10802  modqmuladdnn0  10826  modsumfzodifsn  10854  frec2uzf1od  10864  frec2uzisod  10865  frecuzrdgrrn  10866  frec2uzrdg  10867  frecuzrdgrcl  10868  frecuzrdgtcl  10870  frecuzrdgsuc  10872  frecuzrdgrclt  10873  frecuzrdgfunlem  10877  frecuzrdgtclt  10879  frecuzrdgsuctlem  10881  uzennn  10894  seq3fveq2  10933  seqfveq2g  10935  monoord  10943  iseqf1olemqcl  10957  iseqf1olemnab  10959  iseqf1olemab  10960  iseqf1olemqf1o  10964  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3id2  10984  exp3val  10999  expcl2lemap  11009  expclzaplem  11021  expge0  11033  expge1  11034  zsqcl2  11075  bcval4  11212  bcn1  11218  bccl2  11228  hashennnuni  11240  hashunlem  11266  hashdifpr  11283  zfz1isolem1  11314  seq3coll  11316  iswrdiz  11333  ccatsymb  11392  ccatrn  11399  ccat2s1fvwd  11437  swrds1  11462  swrdccat2  11465  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12lem3  11526  pfxccatin12  11527  pfxccat3  11528  pfxccat3a  11532  shftfn  11611  shftf  11617  recvguniq  11783  resqrexlemdecn  11800  rersqreu  11816  nn0abscl  11874  nnabscl  11889  abs2dif  11895  nn0maxcl  12014  fiidxsupcl  12018  climuni  12084  2clim  12092  climcn2  12100  summodclem2a  12173  fsum3  12179  fsum3cvg3  12188  fsumcl2lem  12190  fsumadd  12198  fisum0diag2  12239  fsummulc2  12240  fsumge0  12251  geolim2  12304  cvgratnnlemabsle  12319  cvgratz  12324  mertenslemi1  12327  prodmodclem3  12367  prodmodclem2a  12368  fprodeq0  12409  fprodge0  12429  eff2  12472  tanvalap  12500  zdvdsdc  12604  fzo0dvdseq  12649  oexpneg  12669  oddge22np1  12673  evennn02n  12674  evennn2n  12675  nno  12698  divalglemeunn  12713  divalglemex  12714  divalglemeuneg  12715  divalg  12716  bitsfzolem  12746  bitsinv1lem  12753  divgcdz  12773  bezoutlemmain  12800  bezoutlemmo  12808  bezoutlemeu  12809  bezoutlemle  12810  sqgcd  12831  uzwodc  12839  nninfctlemfo  12842  eucalgval2  12856  eucalglt  12860  lcmneg  12877  lcmgcdlem  12880  ncoprmgcdne1b  12892  prmind2  12923  prmdc  12933  sqnprm  12940  isprm5lem  12945  isprm5  12946  isprm6  12951  sqrt2irrlem  12965  pwbdvdseu  12972  sqpweven  12980  2sqpwodd  12981  sqrt2irrap  12985  qgt0numnn  13004  nn0sqdcq  13013  phicl2  13021  crth  13031  phimullem  13032  eulerthlem1  13034  eulerthlemh  13038  eulerthlemth  13039  hashgcdlem  13045  oddprm  13067  pythagtriplem6  13078  pythagtriplem11  13082  pythagtriplem13  13084  pythagtriplem19  13090  pclem0  13094  pcpremul  13101  pceu  13103  pc2dvds  13138  difsqpwdvds  13146  pcadd  13148  pockthlem  13164  pockthg  13165  1arith  13175  4sqlemffi  13204  4sqlem11  13209  4sqlem12  13210  4sqlem13m  13211  4sqlem14  13212  4sqlem17  13215  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemrc  13332  ballotfilemth  13339  oddennn  13341  evenennn  13342  ennnfoneleminc  13360  ennnfonelemf1  13367  ennnfonelemen  13370  exmidunben  13375  ctinf  13379  ctiunctlemfo  13388  nninfdclemlt  13400  nninfdclemf1  13401  ptex  13677  imasaddfnlemg  13694  imasaddflemg  13696  mgmsscl  13740  sgrp0  13784  sgrp1  13785  hashfinmndnn  13804  ismndd  13809  mndpfo  13810  mhmf1o  13836  0mhm  13852  resmhm  13853  resmhm2  13854  resmhm2b  13855  mhmco  13856  gsumvallem2  13859  isgrpd2e  13884  grpinvf1o  13934  grpinvnzcl  13936  dfgrp3m  13963  mhmmnd  13978  ghmgrp  13980  mulgval  13984  mulgfng  13986  subgmulg  14050  issubg4m  14055  isnsg3  14069  nmzsubg  14072  ssnmz  14073  0nsg  14076  nsgid  14077  ghmnsgima  14130  ghmnsgpreima  14131  ghmf1  14135  kerf1ghm  14136  ghmf1o  14137  conjnmzb  14142  cntrsubgnsg  14175  isabld  14192  cmnsubm  14202  ghmcmn  14221  ghmabl  14222  invghm  14223  gsumvalfi  14242  srgfcl  14384  srglmhm  14404  srgrmhm  14405  iscrngd  14454  ringsrg  14459  unitabl  14533  rhmf1o  14584  rhmco  14590  ringelnzr  14603  subrngringnsg  14622  subrgcrng  14642  subrgnzr  14659  resrhm  14665  unitrrg  14685  aprnzr  14708  aprlring  14709  drngnzr  14728  lssneln0  14820  rnglidlmsgrp  14943  quscrng  14979  expghmap  15051  mulgghm2  15052  znf1o  15095  znidom  15101  znidomb  15102  isassad  15120  psrbaglesuppg  15166  psrbagcon  15171  psrbaglefifi  15172  gsumbagdiaglem  15175  gsumbagdiagfi  15176  psrass1filem  15177  tgtopon  15292  distopon  15313  epttop  15316  resttopon  15397  resttopon2  15404  cnco  15447  lmss  15472  txtopon  15488  uptx  15500  txdis1cn  15504  hmeocnv  15533  hmeof1o2  15534  hmeores  15541  hmeoco  15542  idhmeo  15543  txhmeo  15545  txswaphmeo  15547  psmetxrge0  15558  isxmet2d  15574  metres2  15607  xmetresbl  15666  comet  15725  bdxmet  15727  bdmet  15728  tgioo  15780  mulc1cncf  15815  mulcncflem  15833  cnrehmeocntop  15836  cnopnap  15837  dedekindeu  15849  dedekindicclemicc  15858  ivthinclemlm  15860  ivthinclemum  15861  ivthinclemlopn  15862  ivthinclemlr  15863  ivthinclemuopn  15864  ivthinclemur  15865  ivthinclemloc  15867  ivthinc  15869  ivthreinc  15871  dvfgg  15914  dvcjbr  15934  dvcj  15935  dvfre  15936  elplyr  15966  plyreres  15990  rplogbval  16181  ppiqsval  16240  ppiqsval2  16241  ppiqfi  16242  sgmnncl  16257  chtdif  16264  ppidif  16269  ppiqnncl  16278  mpodvdsmulf1o  16284  mersenne  16297  perfectlem2  16300  bcmono  16304  bposlem1  16311  bposlem3  16313  bposlem4  16314  bposlem5  16315  bposlem6  16316  bposlem9  16319  lgsfcl2  16330  lgsval2lem  16334  lgsmod  16350  lgsdirprm  16358  lgsne0  16362  gausslemma2dlem0h  16380  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  gausslemma2dlem4  16388  lgseisenlem1  16394  lgseisenlem2  16395  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem2  16406  2sqlem8  16447  2sqlem9  16448  structiedg0val  16486  ausgrumgrien  16616  usgredgreu  16662  uspgredg2vtxeu  16664  uspgredg2v  16667  usgredg2v  16670  usgr1e  16687  subuhgr  16718  subupgr  16719  subumgr  16720  subusgr  16721  vdegp1aid  16760  trlres  16836  clwwlkbp  16841  clwwlkccatlem  16846  s2elclwwlknon2  16882  clwwlknonex2lem2  16884  clwwlknonex2e  16886  bj-charfundcALT  17040  bj-nnord  17189  bj-inf2vnlem1  17201  pwf1oexmid  17234  idjudju  17252  nnsf  17254  nninfall  17258  nninfself  17262  exmidsbthrlem  17273  qdencn  17278  alsd  17338  ralsd  17339  alseud  17374  ralseud  17375