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  1816  sbequ1  1817  sbidm  1900  eqeu  2990  euind  3007  reuind  3025  eldifd  3224  eqssd  3259  ssrabdv  3321  elind  3408  dcun  3623  opm  4355  issod  4445  ordsucim  4627  onintonm  4644  ordtri2or2exmidlem  4653  en2lp  4681  ordwe  4703  sosng  4828  sotri2  5165  sotri3  5166  relssdmrn  5288  funun  5402  fnsng  5408  fnprg  5416  fntpg  5417  fntp  5418  fununi  5429  imain  5443  fnco  5471  f00  5564  f1ss  5584  f1ssr  5585  f1ssres  5587  f1f1orn  5630  foimacnv  5637  foun  5638  fun11iun  5640  sefvex  5696  dff3im  5827  fmpt  5832  ffnfv  5840  fmpt2d  5844  ffvresb  5845  fprg  5872  foco2  5932  fcof1  5962  fcofo  5963  fcof1o  5968  fliftf  5978  isoini2  5998  f1oiso  6005  moriotass  6042  fnoprabg  6162  f1ocnvd  6265  f1o3d  6271  suppssov1  6272  1stcof  6370  2ndcof  6371  1stconst  6430  2ndconst  6431  fo2ndf  6436  f1o2ndf1  6437  f1od2  6444  suppssfvg  6476  smores2  6538  tfrlem5  6558  tfrlemibfn  6572  tfr1onlembfn  6588  tfri1dALT  6595  tfrcllembfn  6601  nntri2  6740  eroveu  6873  elixpsn  6983  dom2lem  7024  xpf1o  7110  fidifsnen  7138  finexdc  7173  elssdc  7175  unfidisj  7195  f1finf1o  7230  fidcenumlemrks  7236  sbthlemi9  7248  supeuti  7298  infeuti  7333  casef1  7394  caseinl  7395  caseinr  7396  difinfsnlem  7403  ctmlemr  7412  ctm  7413  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  enumctlemm  7418  nnnninf  7430  nninfwlpoimlemg  7479  en2other2  7512  exmidfodomrlemim  7517  pw1if  7548  pw1nel3  7554  dftap2  7581  cc2lem  7596  cc4f  7599  addclpi  7658  mulclpi  7659  nnppipi  7674  recmulnqg  7722  enq0ref  7764  nqnq0pi  7769  genipv  7840  addclpr  7868  nqprxx  7877  prmuloc  7897  mulclpr  7903  distrlem1prl  7913  distrlem1pru  7914  ltexprlempr  7939  ltexprlemrl  7941  ltexprlemru  7943  lteupri  7948  recexprlempr  7963  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemloc  7983  cauappcvgprlemcl  7984  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlem2  7991  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlem2  8011  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemupu  8031  caucvgprprlemloc  8034  caucvgprprlemcl  8035  caucvgprprlem2  8041  suplocexprlemex  8053  suplocsrlem  8139  elrealeu  8160  rereceu  8220  axpre-suploclemres  8232  negf1o  8672  aptap  8941  receuap  8960  divvalap  8965  cju  9252  nn0ge2m1nn  9577  nnnegz  9597  elnnz  9604  elnn0z  9607  peano2z  9630  nn0n0n1ge2  9665  msqznn  9696  eluzaddi  9899  eluzsubi  9900  uzind4  9938  supinfneg  9945  infsupneg  9946  elnn1uz2  9957  uz2mulcl  9958  divfnzn  9971  nnrp  10014  rpaddcl  10028  rpmulcl  10029  rpdivcl  10030  rpgecl  10033  ge0p1rp  10036  elrpd  10044  ge0addcl  10333  ge0mulcl  10334  ge0xaddcl  10335  icoshftf1o  10343  peano2fzr  10391  uzsubsubfz  10401  fzsplit2  10404  fzsplit3  10407  elfznn  10409  fzss1  10418  fzss2  10419  fzp1elp1  10431  elfz1b  10446  elfz0fzfz0  10482  fz0fzelfz0  10483  difelfznle  10491  elfzofz  10519  nn0p1elfzo  10543  fzosplitsnm1  10576  ubmelm1fzo  10593  fzofzp1b  10595  fzosplitsn  10600  zsupcllemstep  10611  zsupcl  10613  infssfzcldc  10618  infssfzledc  10619  exbtwnz  10634  flqge0nn0  10677  flqge1nn  10678  zmodcl  10730  modqmuladdnn0  10754  modsumfzodifsn  10782  frec2uzf1od  10792  frec2uzisod  10793  frecuzrdgrrn  10794  frec2uzrdg  10795  frecuzrdgrcl  10796  frecuzrdgtcl  10798  frecuzrdgsuc  10800  frecuzrdgrclt  10801  frecuzrdgfunlem  10805  frecuzrdgtclt  10807  frecuzrdgsuctlem  10809  uzennn  10822  seq3fveq2  10861  seqfveq2g  10863  monoord  10871  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemab  10888  iseqf1olemqf1o  10892  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3id2  10912  exp3val  10927  expcl2lemap  10937  expclzaplem  10949  expge0  10961  expge1  10962  zsqcl2  11003  bcval4  11139  bcn1  11145  bccl2  11155  hashennnuni  11167  hashunlem  11193  hashdifpr  11210  zfz1isolem1  11237  seq3coll  11239  iswrdiz  11256  ccatsymb  11315  ccatrn  11322  ccat2s1fvwd  11360  swrds1  11385  swrdccat2  11388  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccatin12  11450  pfxccat3  11451  pfxccat3a  11455  shftfn  11534  shftf  11540  recvguniq  11705  resqrexlemdecn  11722  rersqreu  11738  nn0abscl  11795  nnabscl  11810  abs2dif  11816  nn0maxcl  11935  climuni  12003  2clim  12011  climcn2  12019  summodclem2a  12092  fsum3  12098  fsum3cvg3  12107  fsumcl2lem  12109  fsumadd  12117  fisum0diag2  12158  fsummulc2  12159  fsumge0  12170  geolim2  12223  cvgratnnlemabsle  12238  cvgratz  12243  mertenslemi1  12246  prodmodclem3  12286  prodmodclem2a  12287  fprodeq0  12328  fprodge0  12348  eff2  12391  tanvalap  12419  zdvdsdc  12523  fzo0dvdseq  12568  oexpneg  12588  oddge22np1  12592  evennn02n  12593  evennn2n  12594  nno  12617  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  divalg  12635  bitsfzolem  12665  bitsinv1lem  12672  divgcdz  12692  bezoutlemmain  12719  bezoutlemmo  12727  bezoutlemeu  12728  bezoutlemle  12729  sqgcd  12750  uzwodc  12758  nninfctlemfo  12761  eucalgval2  12775  eucalglt  12779  lcmneg  12796  lcmgcdlem  12799  ncoprmgcdne1b  12811  prmind2  12842  prmdc  12852  sqnprm  12858  isprm5lem  12863  isprm5  12864  isprm6  12869  sqrt2irrlem  12883  pw2dvdseu  12890  sqpweven  12897  2sqpwodd  12898  sqrt2irrap  12902  qgt0numnn  12921  phicl2  12936  crth  12946  phimullem  12947  eulerthlem1  12949  eulerthlemh  12953  eulerthlemth  12954  hashgcdlem  12960  oddprm  12982  pythagtriplem6  12993  pythagtriplem11  12997  pythagtriplem13  12999  pythagtriplem19  13005  pclem0  13009  pcpremul  13016  pceu  13018  pc2dvds  13053  difsqpwdvds  13061  pcadd  13063  pockthlem  13079  pockthg  13080  1arith  13090  4sqlemffi  13119  4sqlem11  13124  4sqlem12  13125  4sqlem13m  13126  4sqlem14  13127  4sqlem17  13130  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemrc  13218  ballotfilemth  13225  oddennn  13227  evenennn  13228  ennnfoneleminc  13246  ennnfonelemf1  13253  ennnfonelemen  13256  exmidunben  13261  ctinf  13265  ctiunctlemfo  13274  nninfdclemlt  13286  nninfdclemf1  13287  ptex  13561  imasaddfnlemg  13611  imasaddflemg  13613  mgmsscl  13658  sgrp0  13707  sgrp1  13708  hashfinmndnn  13729  ismndd  13734  mndpfo  13735  mhmf1o  13767  0mhm  13783  resmhm  13784  resmhm2  13785  resmhm2b  13786  mhmco  13787  gsumvallem2  13790  isgrpd2e  13817  grpinvf1o  13867  grpinvnzcl  13869  dfgrp3m  13896  mhmmnd  13917  ghmgrp  13919  mulgval  13923  mulgfng  13925  subgmulg  13989  issubg4m  13994  isnsg3  14008  nmzsubg  14011  ssnmz  14012  0nsg  14015  nsgid  14016  ghmnsgima  14069  ghmnsgpreima  14070  ghmf1  14074  kerf1ghm  14075  ghmf1o  14076  conjnmzb  14081  isabld  14100  ghmcmn  14128  ghmabl  14129  invghm  14130  srgfcl  14201  srglmhm  14221  srgrmhm  14222  iscrngd  14270  ringsrg  14275  unitabl  14347  rhmf1o  14398  rhmco  14404  ringelnzr  14417  subrngringnsg  14436  subrgcrng  14456  subrgnzr  14473  resrhm  14479  unitrrg  14499  aprnzr  14522  aprlring  14523  drngnzr  14542  lssneln0  14634  rnglidlmsgrp  14757  quscrng  14793  expghmap  14867  mulgghm2  14868  znf1o  14911  znidom  14917  znidomb  14918  psrbaglesuppg  14933  psrbagcon  14938  tgtopon  15043  distopon  15064  epttop  15067  resttopon  15148  resttopon2  15155  cnco  15198  lmss  15223  txtopon  15239  uptx  15251  txdis1cn  15255  hmeocnv  15284  hmeof1o2  15285  hmeores  15292  hmeoco  15293  idhmeo  15294  txhmeo  15296  txswaphmeo  15298  psmetxrge0  15309  isxmet2d  15325  metres2  15358  xmetresbl  15417  comet  15476  bdxmet  15478  bdmet  15479  tgioo  15531  mulc1cncf  15566  mulcncflem  15584  cnrehmeocntop  15587  cnopnap  15588  dedekindeu  15600  dedekindicclemicc  15609  ivthinclemlm  15611  ivthinclemum  15612  ivthinclemlopn  15613  ivthinclemlr  15614  ivthinclemuopn  15615  ivthinclemur  15616  ivthinclemloc  15618  ivthinc  15620  ivthreinc  15622  dvfgg  15665  dvcjbr  15685  dvcj  15686  dvfre  15687  elplyr  15717  plyreres  15741  rplogbval  15922  sgmnncl  15968  mpodvdsmulf1o  15970  mersenne  15977  perfectlem2  15980  lgsfcl2  15991  lgsval2lem  15995  lgsmod  16011  lgsdirprm  16019  lgsne0  16023  gausslemma2dlem0h  16041  gausslemma2dlem1a  16043  gausslemma2dlem1f1o  16045  gausslemma2dlem4  16049  lgseisenlem1  16055  lgseisenlem2  16056  lgsquadlem1  16062  lgsquadlem2  16063  lgsquad2lem2  16067  2sqlem8  16108  2sqlem9  16109  structiedg0val  16147  ausgrumgrien  16277  usgredgreu  16323  uspgredg2vtxeu  16325  uspgredg2v  16328  usgredg2v  16331  usgr1e  16348  subuhgr  16379  subupgr  16380  subumgr  16381  subusgr  16382  vdegp1aid  16421  trlres  16497  clwwlkbp  16502  clwwlkccatlem  16507  s2elclwwlknon2  16543  clwwlknonex2lem2  16545  clwwlknonex2e  16547  bj-charfundcALT  16691  bj-nnord  16840  bj-inf2vnlem1  16852  pwf1oexmid  16885  nnsf  16895  nninfall  16899  nninfself  16903  exmidsbthrlem  16914  qdencn  16919  gfsumval  16974