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  1781  sbequ1  1782  sbidm  1865  eqeu  2934  euind  2951  reuind  2969  eldifd  3167  eqssd  3201  ssrabdv  3263  elind  3349  dcun  3561  opm  4268  issod  4355  ordsucim  4537  onintonm  4554  ordtri2or2exmidlem  4563  en2lp  4591  ordwe  4613  sosng  4737  sotri2  5068  sotri3  5069  relssdmrn  5191  funun  5303  fnsng  5306  fnprg  5314  fntpg  5315  fntp  5316  fununi  5327  imain  5341  fnco  5369  f00  5452  f1ss  5472  f1ssr  5473  f1ssres  5475  f1f1orn  5518  foimacnv  5525  foun  5526  fun11iun  5528  sefvex  5582  dff3im  5710  fmpt  5715  ffnfv  5723  fmpt2d  5727  ffvresb  5728  fprg  5748  foco2  5803  fcof1  5833  fcofo  5834  fcof1o  5839  fliftf  5849  isoini2  5869  f1oiso  5876  moriotass  5909  fnoprabg  6027  f1ocnvd  6129  suppssfv  6135  suppssov1  6136  1stcof  6230  2ndcof  6231  1stconst  6288  2ndconst  6289  fo2ndf  6294  f1o2ndf1  6295  f1od2  6302  smores2  6361  tfrlem5  6381  tfrlemibfn  6395  tfr1onlembfn  6411  tfri1dALT  6418  tfrcllembfn  6424  nntri2  6561  eroveu  6694  elixpsn  6803  dom2lem  6840  xpf1o  6914  fidifsnen  6940  finexdc  6972  unfidisj  6992  f1finf1o  7022  fidcenumlemrks  7028  sbthlemi9  7040  supeuti  7069  infeuti  7104  casef1  7165  caseinl  7166  caseinr  7167  difinfsnlem  7174  ctmlemr  7183  ctm  7184  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumctlemm  7189  nnnninf  7201  nninfwlpoimlemg  7250  en2other2  7277  exmidfodomrlemim  7282  pw1nel3  7316  dftap2  7336  cc2lem  7351  cc4f  7354  addclpi  7413  mulclpi  7414  nnppipi  7429  recmulnqg  7477  enq0ref  7519  nqnq0pi  7524  genipv  7595  addclpr  7623  nqprxx  7632  prmuloc  7652  mulclpr  7658  distrlem1prl  7668  distrlem1pru  7669  ltexprlempr  7694  ltexprlemrl  7696  ltexprlemru  7698  lteupri  7703  recexprlempr  7718  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemopu  7734  cauappcvgprlemupu  7735  cauappcvgprlemloc  7738  cauappcvgprlemcl  7739  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlem2  7746  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemopu  7757  caucvgprlemupu  7758  caucvgprlemloc  7761  caucvgprlemcl  7762  caucvgprlemladdfu  7763  caucvgprlem2  7766  caucvgprprlemml  7780  caucvgprprlemmu  7781  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemopu  7785  caucvgprprlemupu  7786  caucvgprprlemloc  7789  caucvgprprlemcl  7790  caucvgprprlem2  7796  suplocexprlemex  7808  suplocsrlem  7894  elrealeu  7915  rereceu  7975  axpre-suploclemres  7987  negf1o  8427  aptap  8696  receuap  8715  divvalap  8720  cju  9007  nn0ge2m1nn  9328  nnnegz  9348  elnnz  9355  elnn0z  9358  peano2z  9381  nn0n0n1ge2  9415  msqznn  9445  eluzaddi  9647  eluzsubi  9648  uzind4  9681  supinfneg  9688  infsupneg  9689  elnn1uz2  9700  uz2mulcl  9701  divfnzn  9714  nnrp  9757  rpaddcl  9771  rpmulcl  9772  rpdivcl  9773  rpgecl  9776  ge0p1rp  9779  elrpd  9787  ge0addcl  10075  ge0mulcl  10076  ge0xaddcl  10077  icoshftf1o  10085  peano2fzr  10131  uzsubsubfz  10141  fzsplit2  10144  elfznn  10148  fzss1  10157  fzss2  10158  fzp1elp1  10169  elfz1b  10184  elfz0fzfz0  10220  fz0fzelfz0  10221  difelfznle  10229  elfzofz  10257  fzosplitsnm1  10304  ubmelm1fzo  10321  fzofzp1b  10323  fzosplitsn  10328  zsupcllemstep  10338  zsupcl  10340  exbtwnz  10359  flqge0nn0  10402  flqge1nn  10403  zmodcl  10455  modqmuladdnn0  10479  modsumfzodifsn  10507  frec2uzf1od  10517  frec2uzisod  10518  frecuzrdgrrn  10519  frec2uzrdg  10520  frecuzrdgrcl  10521  frecuzrdgtcl  10523  frecuzrdgsuc  10525  frecuzrdgrclt  10526  frecuzrdgfunlem  10530  frecuzrdgtclt  10532  frecuzrdgsuctlem  10534  uzennn  10547  seq3fveq2  10586  seqfveq2g  10588  monoord  10596  iseqf1olemqcl  10610  iseqf1olemnab  10612  iseqf1olemab  10613  iseqf1olemqf1o  10617  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3id2  10637  exp3val  10652  expcl2lemap  10662  expclzaplem  10674  expge0  10686  expge1  10687  zsqcl2  10728  bcval4  10863  bcn1  10869  bccl2  10879  hashennnuni  10890  hashunlem  10915  hashdifpr  10931  zfz1isolem1  10951  seq3coll  10953  iswrdiz  10961  shftfn  11008  shftf  11014  recvguniq  11179  resqrexlemdecn  11196  rersqreu  11212  nn0abscl  11269  nnabscl  11284  abs2dif  11290  nn0maxcl  11409  climuni  11477  2clim  11485  climcn2  11493  summodclem2a  11565  fsum3  11571  fsum3cvg3  11580  fsumcl2lem  11582  fsumadd  11590  fisum0diag2  11631  fsummulc2  11632  fsumge0  11643  geolim2  11696  cvgratnnlemabsle  11711  cvgratz  11716  mertenslemi1  11719  prodmodclem3  11759  prodmodclem2a  11760  fprodeq0  11801  fprodge0  11821  eff2  11864  tanvalap  11892  zdvdsdc  11996  fzo0dvdseq  12041  oexpneg  12061  oddge22np1  12065  evennn02n  12066  evennn2n  12067  nno  12090  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  divalg  12108  bitsfzolem  12138  bitsinv1lem  12145  divgcdz  12165  bezoutlemmain  12192  bezoutlemmo  12200  bezoutlemeu  12201  bezoutlemle  12202  sqgcd  12223  uzwodc  12231  nninfctlemfo  12234  eucalgval2  12248  eucalglt  12252  lcmneg  12269  lcmgcdlem  12272  ncoprmgcdne1b  12284  prmind2  12315  prmdc  12325  sqnprm  12331  isprm5lem  12336  isprm5  12337  isprm6  12342  sqrt2irrlem  12356  pw2dvdseu  12363  sqpweven  12370  2sqpwodd  12371  sqrt2irrap  12375  qgt0numnn  12394  phicl2  12409  hashdvds  12416  crth  12419  phimullem  12420  eulerthlem1  12422  eulerthlemh  12426  eulerthlemth  12427  hashgcdlem  12433  oddprm  12455  pythagtriplem6  12466  pythagtriplem11  12470  pythagtriplem13  12472  pythagtriplem19  12478  pclem0  12482  pcpremul  12489  pceu  12491  pc2dvds  12526  difsqpwdvds  12534  pcadd  12536  pockthlem  12552  pockthg  12553  1arith  12563  4sqlemffi  12592  4sqlem11  12597  4sqlem12  12598  4sqlem13m  12599  4sqlem14  12600  4sqlem17  12603  oddennn  12636  evenennn  12637  ennnfoneleminc  12655  ennnfonelemf1  12662  ennnfonelemen  12665  exmidunben  12670  ctinf  12674  ctiunctlemfo  12683  nninfdclemlt  12695  nninfdclemf1  12696  ptex  12968  imasaddfnlemg  13018  imasaddflemg  13020  mgmsscl  13065  sgrp0  13114  sgrp1  13115  hashfinmndnn  13136  ismndd  13141  mndpfo  13142  mhmf1o  13174  0mhm  13190  resmhm  13191  resmhm2  13192  resmhm2b  13193  mhmco  13194  gsumvallem2  13197  isgrpd2e  13224  grpinvf1o  13274  grpinvnzcl  13276  dfgrp3m  13303  mhmmnd  13324  ghmgrp  13326  mulgval  13330  mulgfng  13332  subgmulg  13396  issubg4m  13401  isnsg3  13415  nmzsubg  13418  ssnmz  13419  0nsg  13422  nsgid  13423  ghmnsgima  13476  ghmnsgpreima  13477  ghmf1  13481  kerf1ghm  13482  ghmf1o  13483  conjnmzb  13488  isabld  13507  ghmcmn  13535  ghmabl  13536  invghm  13537  srgfcl  13607  srglmhm  13627  srgrmhm  13628  iscrngd  13676  ringsrg  13681  unitabl  13751  rhmf1o  13802  rhmco  13808  ringelnzr  13821  subrngringnsg  13839  subrgcrng  13859  subrgnzr  13876  resrhm  13882  unitrrg  13901  lssneln0  14008  rnglidlmsgrp  14131  quscrng  14167  expghmap  14241  mulgghm2  14242  znf1o  14285  znidom  14291  znidomb  14292  psrbaglesuppg  14306  tgtopon  14410  distopon  14431  epttop  14434  resttopon  14515  resttopon2  14522  cnco  14565  lmss  14590  txtopon  14606  uptx  14618  txdis1cn  14622  hmeocnv  14651  hmeof1o2  14652  hmeores  14659  hmeoco  14660  idhmeo  14661  txhmeo  14663  txswaphmeo  14665  psmetxrge0  14676  isxmet2d  14692  metres2  14725  xmetresbl  14784  comet  14843  bdxmet  14845  bdmet  14846  tgioo  14898  mulc1cncf  14933  mulcncflem  14951  cnrehmeocntop  14954  cnopnap  14955  dedekindeu  14967  dedekindicclemicc  14976  ivthinclemlm  14978  ivthinclemum  14979  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemloc  14985  ivthinc  14987  ivthreinc  14989  dvfgg  15032  dvcjbr  15052  dvcj  15053  dvfre  15054  elplyr  15084  plyreres  15108  rplogbval  15289  sgmnncl  15332  mpodvdsmulf1o  15334  mersenne  15341  perfectlem2  15344  lgsfcl2  15355  lgsval2lem  15359  lgsmod  15375  lgsdirprm  15383  lgsne0  15387  gausslemma2dlem0h  15405  gausslemma2dlem1a  15407  gausslemma2dlem1f1o  15409  gausslemma2dlem4  15413  lgseisenlem1  15419  lgseisenlem2  15420  lgsquadlem1  15426  lgsquadlem2  15427  lgsquad2lem2  15431  2sqlem8  15472  2sqlem9  15473  bj-charfundcALT  15563  bj-nnord  15712  bj-inf2vnlem1  15724  pwf1oexmid  15754  nnsf  15760  nninfall  15764  nninfself  15768  exmidsbthrlem  15779  qdencn  15784