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  934  sb2  1778  sbequ1  1779  sbidm  1862  eqeu  2930  euind  2947  reuind  2965  eldifd  3163  eqssd  3196  ssrabdv  3258  elind  3344  dcun  3556  opm  4263  issod  4350  ordsucim  4532  onintonm  4549  ordtri2or2exmidlem  4558  en2lp  4586  ordwe  4608  sosng  4732  sotri2  5063  sotri3  5064  relssdmrn  5186  funun  5298  fnsng  5301  fnprg  5309  fntpg  5310  fntp  5311  fununi  5322  imain  5336  fnco  5362  f00  5445  f1ss  5465  f1ssr  5466  f1ssres  5468  f1f1orn  5511  foimacnv  5518  foun  5519  fun11iun  5521  sefvex  5575  dff3im  5703  fmpt  5708  ffnfv  5716  fmpt2d  5720  ffvresb  5721  fprg  5741  foco2  5796  fcof1  5826  fcofo  5827  fcof1o  5832  fliftf  5842  isoini2  5862  f1oiso  5869  moriotass  5902  fnoprabg  6019  f1ocnvd  6120  suppssfv  6126  suppssov1  6127  1stcof  6216  2ndcof  6217  1stconst  6274  2ndconst  6275  fo2ndf  6280  f1o2ndf1  6281  f1od2  6288  smores2  6347  tfrlem5  6367  tfrlemibfn  6381  tfr1onlembfn  6397  tfri1dALT  6404  tfrcllembfn  6410  nntri2  6547  eroveu  6680  elixpsn  6789  dom2lem  6826  xpf1o  6900  fidifsnen  6926  finexdc  6958  unfidisj  6978  f1finf1o  7006  fidcenumlemrks  7012  sbthlemi9  7024  supeuti  7053  infeuti  7088  casef1  7149  caseinl  7150  caseinr  7151  difinfsnlem  7158  ctmlemr  7167  ctm  7168  ctssdclemn0  7169  ctssdccl  7170  ctssdc  7172  enumctlemm  7173  nnnninf  7185  nninfwlpoimlemg  7234  en2other2  7256  exmidfodomrlemim  7261  pw1nel3  7291  dftap2  7311  cc2lem  7326  cc4f  7329  addclpi  7387  mulclpi  7388  nnppipi  7403  recmulnqg  7451  enq0ref  7493  nqnq0pi  7498  genipv  7569  addclpr  7597  nqprxx  7606  prmuloc  7626  mulclpr  7632  distrlem1prl  7642  distrlem1pru  7643  ltexprlempr  7668  ltexprlemrl  7670  ltexprlemru  7672  lteupri  7677  recexprlempr  7692  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemopu  7708  cauappcvgprlemupu  7709  cauappcvgprlemloc  7712  cauappcvgprlemcl  7713  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlem2  7720  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemopu  7731  caucvgprlemupu  7732  caucvgprlemloc  7735  caucvgprlemcl  7736  caucvgprlemladdfu  7737  caucvgprlem2  7740  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemopu  7759  caucvgprprlemupu  7760  caucvgprprlemloc  7763  caucvgprprlemcl  7764  caucvgprprlem2  7770  suplocexprlemex  7782  suplocsrlem  7868  elrealeu  7889  rereceu  7949  axpre-suploclemres  7961  negf1o  8401  aptap  8669  receuap  8688  divvalap  8693  cju  8980  nn0ge2m1nn  9300  nnnegz  9320  elnnz  9327  elnn0z  9330  peano2z  9353  nn0n0n1ge2  9387  msqznn  9417  eluzaddi  9619  eluzsubi  9620  uzind4  9653  supinfneg  9660  infsupneg  9661  elnn1uz2  9672  uz2mulcl  9673  divfnzn  9686  nnrp  9729  rpaddcl  9743  rpmulcl  9744  rpdivcl  9745  rpgecl  9748  ge0p1rp  9751  elrpd  9759  ge0addcl  10047  ge0mulcl  10048  ge0xaddcl  10049  icoshftf1o  10057  peano2fzr  10103  uzsubsubfz  10113  fzsplit2  10116  elfznn  10120  fzss1  10129  fzss2  10130  fzp1elp1  10141  elfz1b  10156  elfz0fzfz0  10192  fz0fzelfz0  10193  difelfznle  10201  elfzofz  10229  fzosplitsnm1  10276  ubmelm1fzo  10293  fzofzp1b  10295  fzosplitsn  10300  exbtwnz  10319  flqge0nn0  10362  flqge1nn  10363  zmodcl  10415  modqmuladdnn0  10439  modsumfzodifsn  10467  frec2uzf1od  10477  frec2uzisod  10478  frecuzrdgrrn  10479  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgtcl  10483  frecuzrdgsuc  10485  frecuzrdgrclt  10486  frecuzrdgfunlem  10490  frecuzrdgtclt  10492  frecuzrdgsuctlem  10494  uzennn  10507  seq3fveq2  10546  seqfveq2g  10548  monoord  10556  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemab  10573  iseqf1olemqf1o  10577  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3id2  10597  exp3val  10612  expcl2lemap  10622  expclzaplem  10634  expge0  10646  expge1  10647  zsqcl2  10688  bcval4  10823  bcn1  10829  bccl2  10839  hashennnuni  10850  hashunlem  10875  hashdifpr  10891  zfz1isolem1  10911  seq3coll  10913  iswrdiz  10921  shftfn  10968  shftf  10974  recvguniq  11139  resqrexlemdecn  11156  rersqreu  11172  nn0abscl  11229  nnabscl  11244  abs2dif  11250  climuni  11436  2clim  11444  climcn2  11452  summodclem2a  11524  fsum3  11530  fsum3cvg3  11539  fsumcl2lem  11541  fsumadd  11549  fisum0diag2  11590  fsummulc2  11591  fsumge0  11602  geolim2  11655  cvgratnnlemabsle  11670  cvgratz  11675  mertenslemi1  11678  prodmodclem3  11718  prodmodclem2a  11719  fprodeq0  11760  fprodge0  11780  eff2  11823  tanvalap  11851  zdvdsdc  11955  fzo0dvdseq  11999  oexpneg  12018  oddge22np1  12022  evennn02n  12023  evennn2n  12024  nno  12047  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  divalg  12065  zsupcllemstep  12082  zsupcl  12084  divgcdz  12108  bezoutlemmain  12135  bezoutlemmo  12143  bezoutlemeu  12144  bezoutlemle  12145  sqgcd  12166  uzwodc  12174  nninfctlemfo  12177  eucalgval2  12191  eucalglt  12195  lcmneg  12212  lcmgcdlem  12215  ncoprmgcdne1b  12227  prmind2  12258  prmdc  12268  sqnprm  12274  isprm5lem  12279  isprm5  12280  isprm6  12285  sqrt2irrlem  12299  pw2dvdseu  12306  sqpweven  12313  2sqpwodd  12314  sqrt2irrap  12318  qgt0numnn  12337  phicl2  12352  hashdvds  12359  crth  12362  phimullem  12363  eulerthlem1  12365  eulerthlemh  12369  eulerthlemth  12370  hashgcdlem  12376  oddprm  12397  pythagtriplem6  12408  pythagtriplem11  12412  pythagtriplem13  12414  pythagtriplem19  12420  pclem0  12424  pcpremul  12431  pceu  12433  pc2dvds  12468  difsqpwdvds  12476  pcadd  12478  pockthlem  12494  pockthg  12495  1arith  12505  4sqlemffi  12534  4sqlem11  12539  4sqlem12  12540  4sqlem13m  12541  4sqlem14  12542  4sqlem17  12545  oddennn  12549  evenennn  12550  ennnfoneleminc  12568  ennnfonelemf1  12575  ennnfonelemen  12578  exmidunben  12583  ctinf  12587  ctiunctlemfo  12596  nninfdclemlt  12608  nninfdclemf1  12609  ptex  12875  imasaddfnlemg  12897  imasaddflemg  12899  mgmsscl  12944  sgrp0  12993  sgrp1  12994  hashfinmndnn  13013  ismndd  13018  mndpfo  13019  mhmf1o  13042  0mhm  13058  resmhm  13059  resmhm2  13060  resmhm2b  13061  mhmco  13062  gsumvallem2  13065  isgrpd2e  13092  grpinvf1o  13142  grpinvnzcl  13144  dfgrp3m  13171  mhmmnd  13186  ghmgrp  13188  mulgval  13192  mulgfng  13194  subgmulg  13258  issubg4m  13263  isnsg3  13277  nmzsubg  13280  ssnmz  13281  0nsg  13284  nsgid  13285  ghmnsgima  13338  ghmnsgpreima  13339  ghmf1  13343  kerf1ghm  13344  ghmf1o  13345  conjnmzb  13350  isabld  13369  ghmcmn  13397  ghmabl  13398  invghm  13399  srgfcl  13469  srglmhm  13489  srgrmhm  13490  iscrngd  13538  ringsrg  13543  unitabl  13613  rhmf1o  13664  rhmco  13670  ringelnzr  13683  subrngringnsg  13701  subrgcrng  13721  subrgnzr  13738  resrhm  13744  unitrrg  13763  lssneln0  13870  rnglidlmsgrp  13993  quscrng  14029  expghmap  14095  mulgghm2  14096  znf1o  14139  znidom  14145  znidomb  14146  psrbaglesuppg  14158  tgtopon  14234  distopon  14255  epttop  14258  resttopon  14339  resttopon2  14346  cnco  14389  lmss  14414  txtopon  14430  uptx  14442  txdis1cn  14446  hmeocnv  14475  hmeof1o2  14476  hmeores  14483  hmeoco  14484  idhmeo  14485  txhmeo  14487  txswaphmeo  14489  psmetxrge0  14500  isxmet2d  14516  metres2  14549  xmetresbl  14608  comet  14667  bdxmet  14669  bdmet  14670  tgioo  14714  mulc1cncf  14744  mulcncflem  14761  cnrehmeocntop  14764  cnopnap  14765  dedekindeu  14777  dedekindicclemicc  14786  ivthinclemlm  14788  ivthinclemum  14789  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemloc  14795  ivthinc  14797  ivthreinc  14799  dvfgg  14842  dvcjbr  14857  dvcj  14858  dvfre  14859  elplyr  14886  rplogbval  15077  lgsfcl2  15122  lgsval2lem  15126  lgsmod  15142  lgsdirprm  15150  lgsne0  15154  gausslemma2dlem0h  15172  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  gausslemma2dlem4  15180  lgseisenlem1  15186  lgseisenlem2  15187  lgsquadlem1  15191  2sqlem8  15210  2sqlem9  15211  bj-charfundcALT  15301  bj-nnord  15450  bj-inf2vnlem1  15462  pwf1oexmid  15490  nnsf  15495  nninfall  15499  nninfself  15503  exmidsbthrlem  15512  qdencn  15517