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  940  ecase2d  1387  sb2  1815  sbequ1  1816  sbidm  1899  eqeu  2976  euind  2993  reuind  3011  eldifd  3210  eqssd  3244  ssrabdv  3306  elind  3392  dcun  3604  opm  4326  issod  4416  ordsucim  4598  onintonm  4615  ordtri2or2exmidlem  4624  en2lp  4652  ordwe  4674  sosng  4799  sotri2  5134  sotri3  5135  relssdmrn  5257  funun  5371  fnsng  5377  fnprg  5385  fntpg  5386  fntp  5387  fununi  5398  imain  5412  fnco  5440  f00  5528  f1ss  5548  f1ssr  5549  f1ssres  5551  f1f1orn  5594  foimacnv  5601  foun  5602  fun11iun  5604  sefvex  5660  dff3im  5792  fmpt  5797  ffnfv  5805  fmpt2d  5809  ffvresb  5810  fprg  5837  foco2  5894  fcof1  5924  fcofo  5925  fcof1o  5930  fliftf  5940  isoini2  5960  f1oiso  5967  moriotass  6002  fnoprabg  6122  f1ocnvd  6225  suppssfv  6231  suppssov1  6232  1stcof  6326  2ndcof  6327  1stconst  6386  2ndconst  6387  fo2ndf  6392  f1o2ndf1  6393  f1od2  6400  smores2  6460  tfrlem5  6480  tfrlemibfn  6494  tfr1onlembfn  6510  tfri1dALT  6517  tfrcllembfn  6523  nntri2  6662  eroveu  6795  elixpsn  6904  dom2lem  6945  xpf1o  7030  fidifsnen  7057  finexdc  7092  elssdc  7094  unfidisj  7114  f1finf1o  7146  fidcenumlemrks  7152  sbthlemi9  7164  supeuti  7193  infeuti  7228  casef1  7289  caseinl  7290  caseinr  7291  difinfsnlem  7298  ctmlemr  7307  ctm  7308  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  nnnninf  7325  nninfwlpoimlemg  7374  en2other2  7407  exmidfodomrlemim  7412  pw1if  7443  pw1nel3  7449  dftap2  7470  cc2lem  7485  cc4f  7488  addclpi  7547  mulclpi  7548  nnppipi  7563  recmulnqg  7611  enq0ref  7653  nqnq0pi  7658  genipv  7729  addclpr  7757  nqprxx  7766  prmuloc  7786  mulclpr  7792  distrlem1prl  7802  distrlem1pru  7803  ltexprlempr  7828  ltexprlemrl  7830  ltexprlemru  7832  lteupri  7837  recexprlempr  7852  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemloc  7872  cauappcvgprlemcl  7873  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlem2  7880  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlem2  7900  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemupu  7920  caucvgprprlemloc  7923  caucvgprprlemcl  7924  caucvgprprlem2  7930  suplocexprlemex  7942  suplocsrlem  8028  elrealeu  8049  rereceu  8109  axpre-suploclemres  8121  negf1o  8561  aptap  8830  receuap  8849  divvalap  8854  cju  9141  nn0ge2m1nn  9462  nnnegz  9482  elnnz  9489  elnn0z  9492  peano2z  9515  nn0n0n1ge2  9550  msqznn  9580  eluzaddi  9783  eluzsubi  9784  uzind4  9822  supinfneg  9829  infsupneg  9830  elnn1uz2  9841  uz2mulcl  9842  divfnzn  9855  nnrp  9898  rpaddcl  9912  rpmulcl  9913  rpdivcl  9914  rpgecl  9917  ge0p1rp  9920  elrpd  9928  ge0addcl  10216  ge0mulcl  10217  ge0xaddcl  10218  icoshftf1o  10226  peano2fzr  10272  uzsubsubfz  10282  fzsplit2  10285  elfznn  10289  fzss1  10298  fzss2  10299  fzp1elp1  10310  elfz1b  10325  elfz0fzfz0  10361  fz0fzelfz0  10362  difelfznle  10370  elfzofz  10398  nn0p1elfzo  10422  fzosplitsnm1  10455  ubmelm1fzo  10472  fzofzp1b  10474  fzosplitsn  10479  zsupcllemstep  10490  zsupcl  10492  exbtwnz  10511  flqge0nn0  10554  flqge1nn  10555  zmodcl  10607  modqmuladdnn0  10631  modsumfzodifsn  10659  frec2uzf1od  10669  frec2uzisod  10670  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgtcl  10675  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgfunlem  10682  frecuzrdgtclt  10684  frecuzrdgsuctlem  10686  uzennn  10699  seq3fveq2  10738  seqfveq2g  10740  monoord  10748  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemqf1o  10769  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3id2  10789  exp3val  10804  expcl2lemap  10814  expclzaplem  10826  expge0  10838  expge1  10839  zsqcl2  10880  bcval4  11015  bcn1  11021  bccl2  11031  hashennnuni  11042  hashunlem  11068  hashdifpr  11085  zfz1isolem1  11105  seq3coll  11107  iswrdiz  11124  ccatsymb  11183  ccatrn  11190  ccat2s1fvwd  11228  swrds1  11253  swrdccat2  11256  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccatin12  11318  pfxccat3  11319  pfxccat3a  11323  shftfn  11389  shftf  11395  recvguniq  11560  resqrexlemdecn  11577  rersqreu  11593  nn0abscl  11650  nnabscl  11665  abs2dif  11671  nn0maxcl  11790  climuni  11858  2clim  11866  climcn2  11874  summodclem2a  11947  fsum3  11953  fsum3cvg3  11962  fsumcl2lem  11964  fsumadd  11972  fisum0diag2  12013  fsummulc2  12014  fsumge0  12025  geolim2  12078  cvgratnnlemabsle  12093  cvgratz  12098  mertenslemi1  12101  prodmodclem3  12141  prodmodclem2a  12142  fprodeq0  12183  fprodge0  12203  eff2  12246  tanvalap  12274  zdvdsdc  12378  fzo0dvdseq  12423  oexpneg  12443  oddge22np1  12447  evennn02n  12448  evennn2n  12449  nno  12472  divalglemeunn  12487  divalglemex  12488  divalglemeuneg  12489  divalg  12490  bitsfzolem  12520  bitsinv1lem  12527  divgcdz  12547  bezoutlemmain  12574  bezoutlemmo  12582  bezoutlemeu  12583  bezoutlemle  12584  sqgcd  12605  uzwodc  12613  nninfctlemfo  12616  eucalgval2  12630  eucalglt  12634  lcmneg  12651  lcmgcdlem  12654  ncoprmgcdne1b  12666  prmind2  12697  prmdc  12707  sqnprm  12713  isprm5lem  12718  isprm5  12719  isprm6  12724  sqrt2irrlem  12738  pw2dvdseu  12745  sqpweven  12752  2sqpwodd  12753  sqrt2irrap  12757  qgt0numnn  12776  phicl2  12791  hashdvds  12798  crth  12801  phimullem  12802  eulerthlem1  12804  eulerthlemh  12808  eulerthlemth  12809  hashgcdlem  12815  oddprm  12837  pythagtriplem6  12848  pythagtriplem11  12852  pythagtriplem13  12854  pythagtriplem19  12860  pclem0  12864  pcpremul  12871  pceu  12873  pc2dvds  12908  difsqpwdvds  12916  pcadd  12918  pockthlem  12934  pockthg  12935  1arith  12945  4sqlemffi  12974  4sqlem11  12979  4sqlem12  12980  4sqlem13m  12981  4sqlem14  12982  4sqlem17  12985  oddennn  13018  evenennn  13019  ennnfoneleminc  13037  ennnfonelemf1  13044  ennnfonelemen  13047  exmidunben  13052  ctinf  13056  ctiunctlemfo  13065  nninfdclemlt  13077  nninfdclemf1  13078  ptex  13352  imasaddfnlemg  13402  imasaddflemg  13404  mgmsscl  13449  sgrp0  13498  sgrp1  13499  hashfinmndnn  13520  ismndd  13525  mndpfo  13526  mhmf1o  13558  0mhm  13574  resmhm  13575  resmhm2  13576  resmhm2b  13577  mhmco  13578  gsumvallem2  13581  isgrpd2e  13608  grpinvf1o  13658  grpinvnzcl  13660  dfgrp3m  13687  mhmmnd  13708  ghmgrp  13710  mulgval  13714  mulgfng  13716  subgmulg  13780  issubg4m  13785  isnsg3  13799  nmzsubg  13802  ssnmz  13803  0nsg  13806  nsgid  13807  ghmnsgima  13860  ghmnsgpreima  13861  ghmf1  13865  kerf1ghm  13866  ghmf1o  13867  conjnmzb  13872  isabld  13891  ghmcmn  13919  ghmabl  13920  invghm  13921  srgfcl  13992  srglmhm  14012  srgrmhm  14013  iscrngd  14061  ringsrg  14066  unitabl  14137  rhmf1o  14188  rhmco  14194  ringelnzr  14207  subrngringnsg  14225  subrgcrng  14245  subrgnzr  14262  resrhm  14268  unitrrg  14287  lssneln0  14394  rnglidlmsgrp  14517  quscrng  14553  expghmap  14627  mulgghm2  14628  znf1o  14671  znidom  14677  znidomb  14678  psrbaglesuppg  14692  tgtopon  14796  distopon  14817  epttop  14820  resttopon  14901  resttopon2  14908  cnco  14951  lmss  14976  txtopon  14992  uptx  15004  txdis1cn  15008  hmeocnv  15037  hmeof1o2  15038  hmeores  15045  hmeoco  15046  idhmeo  15047  txhmeo  15049  txswaphmeo  15051  psmetxrge0  15062  isxmet2d  15078  metres2  15111  xmetresbl  15170  comet  15229  bdxmet  15231  bdmet  15232  tgioo  15284  mulc1cncf  15319  mulcncflem  15337  cnrehmeocntop  15340  cnopnap  15341  dedekindeu  15353  dedekindicclemicc  15362  ivthinclemlm  15364  ivthinclemum  15365  ivthinclemlopn  15366  ivthinclemlr  15367  ivthinclemuopn  15368  ivthinclemur  15369  ivthinclemloc  15371  ivthinc  15373  ivthreinc  15375  dvfgg  15418  dvcjbr  15438  dvcj  15439  dvfre  15440  elplyr  15470  plyreres  15494  rplogbval  15675  sgmnncl  15718  mpodvdsmulf1o  15720  mersenne  15727  perfectlem2  15730  lgsfcl2  15741  lgsval2lem  15745  lgsmod  15761  lgsdirprm  15769  lgsne0  15773  gausslemma2dlem0h  15791  gausslemma2dlem1a  15793  gausslemma2dlem1f1o  15795  gausslemma2dlem4  15799  lgseisenlem1  15805  lgseisenlem2  15806  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2lem2  15817  2sqlem8  15858  2sqlem9  15859  structiedg0val  15897  ausgrumgrien  16027  usgredgreu  16073  uspgredg2vtxeu  16075  uspgredg2v  16078  usgredg2v  16081  usgr1e  16098  subuhgr  16129  subupgr  16130  subumgr  16131  subusgr  16132  vdegp1aid  16171  trlres  16247  clwwlkbp  16252  clwwlkccatlem  16257  s2elclwwlknon2  16293  clwwlknonex2lem2  16295  clwwlknonex2e  16297  bj-charfundcALT  16430  bj-nnord  16579  bj-inf2vnlem1  16591  pwf1oexmid  16626  nnsf  16633  nninfall  16637  nninfself  16641  exmidsbthrlem  16652  qdencn  16657  gfsumval  16706