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  935  sb2  1791  sbequ1  1792  sbidm  1875  eqeu  2945  euind  2962  reuind  2980  eldifd  3178  eqssd  3212  ssrabdv  3274  elind  3360  dcun  3572  opm  4283  issod  4371  ordsucim  4553  onintonm  4570  ordtri2or2exmidlem  4579  en2lp  4607  ordwe  4629  sosng  4753  sotri2  5086  sotri3  5087  relssdmrn  5209  funun  5321  fnsng  5327  fnprg  5335  fntpg  5336  fntp  5337  fununi  5348  imain  5362  fnco  5390  f00  5476  f1ss  5496  f1ssr  5497  f1ssres  5499  f1f1orn  5542  foimacnv  5549  foun  5550  fun11iun  5552  sefvex  5607  dff3im  5735  fmpt  5740  ffnfv  5748  fmpt2d  5752  ffvresb  5753  fprg  5777  foco2  5832  fcof1  5862  fcofo  5863  fcof1o  5868  fliftf  5878  isoini2  5898  f1oiso  5905  moriotass  5938  fnoprabg  6056  f1ocnvd  6158  suppssfv  6164  suppssov1  6165  1stcof  6259  2ndcof  6260  1stconst  6317  2ndconst  6318  fo2ndf  6323  f1o2ndf1  6324  f1od2  6331  smores2  6390  tfrlem5  6410  tfrlemibfn  6424  tfr1onlembfn  6440  tfri1dALT  6447  tfrcllembfn  6453  nntri2  6590  eroveu  6723  elixpsn  6832  dom2lem  6873  xpf1o  6953  fidifsnen  6979  finexdc  7011  unfidisj  7031  f1finf1o  7061  fidcenumlemrks  7067  sbthlemi9  7079  supeuti  7108  infeuti  7143  casef1  7204  caseinl  7205  caseinr  7206  difinfsnlem  7213  ctmlemr  7222  ctm  7223  ctssdclemn0  7224  ctssdccl  7225  ctssdc  7227  enumctlemm  7228  nnnninf  7240  nninfwlpoimlemg  7289  en2other2  7317  exmidfodomrlemim  7322  pw1nel3  7356  dftap2  7376  cc2lem  7391  cc4f  7394  addclpi  7453  mulclpi  7454  nnppipi  7469  recmulnqg  7517  enq0ref  7559  nqnq0pi  7564  genipv  7635  addclpr  7663  nqprxx  7672  prmuloc  7692  mulclpr  7698  distrlem1prl  7708  distrlem1pru  7709  ltexprlempr  7734  ltexprlemrl  7736  ltexprlemru  7738  lteupri  7743  recexprlempr  7758  cauappcvgprlemm  7771  cauappcvgprlemopl  7772  cauappcvgprlemlol  7773  cauappcvgprlemopu  7774  cauappcvgprlemupu  7775  cauappcvgprlemloc  7778  cauappcvgprlemcl  7779  cauappcvgprlemladdfu  7780  cauappcvgprlemladdfl  7781  cauappcvgprlem2  7786  caucvgprlemm  7794  caucvgprlemopl  7795  caucvgprlemlol  7796  caucvgprlemopu  7797  caucvgprlemupu  7798  caucvgprlemloc  7801  caucvgprlemcl  7802  caucvgprlemladdfu  7803  caucvgprlem2  7806  caucvgprprlemml  7820  caucvgprprlemmu  7821  caucvgprprlemopl  7823  caucvgprprlemlol  7824  caucvgprprlemopu  7825  caucvgprprlemupu  7826  caucvgprprlemloc  7829  caucvgprprlemcl  7830  caucvgprprlem2  7836  suplocexprlemex  7848  suplocsrlem  7934  elrealeu  7955  rereceu  8015  axpre-suploclemres  8027  negf1o  8467  aptap  8736  receuap  8755  divvalap  8760  cju  9047  nn0ge2m1nn  9368  nnnegz  9388  elnnz  9395  elnn0z  9398  peano2z  9421  nn0n0n1ge2  9456  msqznn  9486  eluzaddi  9688  eluzsubi  9689  uzind4  9722  supinfneg  9729  infsupneg  9730  elnn1uz2  9741  uz2mulcl  9742  divfnzn  9755  nnrp  9798  rpaddcl  9812  rpmulcl  9813  rpdivcl  9814  rpgecl  9817  ge0p1rp  9820  elrpd  9828  ge0addcl  10116  ge0mulcl  10117  ge0xaddcl  10118  icoshftf1o  10126  peano2fzr  10172  uzsubsubfz  10182  fzsplit2  10185  elfznn  10189  fzss1  10198  fzss2  10199  fzp1elp1  10210  elfz1b  10225  elfz0fzfz0  10261  fz0fzelfz0  10262  difelfznle  10270  elfzofz  10298  fzosplitsnm1  10351  ubmelm1fzo  10368  fzofzp1b  10370  fzosplitsn  10375  zsupcllemstep  10385  zsupcl  10387  exbtwnz  10406  flqge0nn0  10449  flqge1nn  10450  zmodcl  10502  modqmuladdnn0  10526  modsumfzodifsn  10554  frec2uzf1od  10564  frec2uzisod  10565  frecuzrdgrrn  10566  frec2uzrdg  10567  frecuzrdgrcl  10568  frecuzrdgtcl  10570  frecuzrdgsuc  10572  frecuzrdgrclt  10573  frecuzrdgfunlem  10577  frecuzrdgtclt  10579  frecuzrdgsuctlem  10581  uzennn  10594  seq3fveq2  10633  seqfveq2g  10635  monoord  10643  iseqf1olemqcl  10657  iseqf1olemnab  10659  iseqf1olemab  10660  iseqf1olemqf1o  10664  seq3f1olemqsumkj  10669  seq3f1olemqsumk  10670  seq3id2  10684  exp3val  10699  expcl2lemap  10709  expclzaplem  10721  expge0  10733  expge1  10734  zsqcl2  10775  bcval4  10910  bcn1  10916  bccl2  10926  hashennnuni  10937  hashunlem  10962  hashdifpr  10978  zfz1isolem1  10998  seq3coll  11000  iswrdiz  11014  ccatsymb  11072  ccatrn  11079  swrds1  11135  swrdccat2  11138  shftfn  11185  shftf  11191  recvguniq  11356  resqrexlemdecn  11373  rersqreu  11389  nn0abscl  11446  nnabscl  11461  abs2dif  11467  nn0maxcl  11586  climuni  11654  2clim  11662  climcn2  11670  summodclem2a  11742  fsum3  11748  fsum3cvg3  11757  fsumcl2lem  11759  fsumadd  11767  fisum0diag2  11808  fsummulc2  11809  fsumge0  11820  geolim2  11873  cvgratnnlemabsle  11888  cvgratz  11893  mertenslemi1  11896  prodmodclem3  11936  prodmodclem2a  11937  fprodeq0  11978  fprodge0  11998  eff2  12041  tanvalap  12069  zdvdsdc  12173  fzo0dvdseq  12218  oexpneg  12238  oddge22np1  12242  evennn02n  12243  evennn2n  12244  nno  12267  divalglemeunn  12282  divalglemex  12283  divalglemeuneg  12284  divalg  12285  bitsfzolem  12315  bitsinv1lem  12322  divgcdz  12342  bezoutlemmain  12369  bezoutlemmo  12377  bezoutlemeu  12378  bezoutlemle  12379  sqgcd  12400  uzwodc  12408  nninfctlemfo  12411  eucalgval2  12425  eucalglt  12429  lcmneg  12446  lcmgcdlem  12449  ncoprmgcdne1b  12461  prmind2  12492  prmdc  12502  sqnprm  12508  isprm5lem  12513  isprm5  12514  isprm6  12519  sqrt2irrlem  12533  pw2dvdseu  12540  sqpweven  12547  2sqpwodd  12548  sqrt2irrap  12552  qgt0numnn  12571  phicl2  12586  hashdvds  12593  crth  12596  phimullem  12597  eulerthlem1  12599  eulerthlemh  12603  eulerthlemth  12604  hashgcdlem  12610  oddprm  12632  pythagtriplem6  12643  pythagtriplem11  12647  pythagtriplem13  12649  pythagtriplem19  12655  pclem0  12659  pcpremul  12666  pceu  12668  pc2dvds  12703  difsqpwdvds  12711  pcadd  12713  pockthlem  12729  pockthg  12730  1arith  12740  4sqlemffi  12769  4sqlem11  12774  4sqlem12  12775  4sqlem13m  12776  4sqlem14  12777  4sqlem17  12780  oddennn  12813  evenennn  12814  ennnfoneleminc  12832  ennnfonelemf1  12839  ennnfonelemen  12842  exmidunben  12847  ctinf  12851  ctiunctlemfo  12860  nninfdclemlt  12872  nninfdclemf1  12873  ptex  13146  imasaddfnlemg  13196  imasaddflemg  13198  mgmsscl  13243  sgrp0  13292  sgrp1  13293  hashfinmndnn  13314  ismndd  13319  mndpfo  13320  mhmf1o  13352  0mhm  13368  resmhm  13369  resmhm2  13370  resmhm2b  13371  mhmco  13372  gsumvallem2  13375  isgrpd2e  13402  grpinvf1o  13452  grpinvnzcl  13454  dfgrp3m  13481  mhmmnd  13502  ghmgrp  13504  mulgval  13508  mulgfng  13510  subgmulg  13574  issubg4m  13579  isnsg3  13593  nmzsubg  13596  ssnmz  13597  0nsg  13600  nsgid  13601  ghmnsgima  13654  ghmnsgpreima  13655  ghmf1  13659  kerf1ghm  13660  ghmf1o  13661  conjnmzb  13666  isabld  13685  ghmcmn  13713  ghmabl  13714  invghm  13715  srgfcl  13785  srglmhm  13805  srgrmhm  13806  iscrngd  13854  ringsrg  13859  unitabl  13929  rhmf1o  13980  rhmco  13986  ringelnzr  13999  subrngringnsg  14017  subrgcrng  14037  subrgnzr  14054  resrhm  14060  unitrrg  14079  lssneln0  14186  rnglidlmsgrp  14309  quscrng  14345  expghmap  14419  mulgghm2  14420  znf1o  14463  znidom  14469  znidomb  14470  psrbaglesuppg  14484  tgtopon  14588  distopon  14609  epttop  14612  resttopon  14693  resttopon2  14700  cnco  14743  lmss  14768  txtopon  14784  uptx  14796  txdis1cn  14800  hmeocnv  14829  hmeof1o2  14830  hmeores  14837  hmeoco  14838  idhmeo  14839  txhmeo  14841  txswaphmeo  14843  psmetxrge0  14854  isxmet2d  14870  metres2  14903  xmetresbl  14962  comet  15021  bdxmet  15023  bdmet  15024  tgioo  15076  mulc1cncf  15111  mulcncflem  15129  cnrehmeocntop  15132  cnopnap  15133  dedekindeu  15145  dedekindicclemicc  15154  ivthinclemlm  15156  ivthinclemum  15157  ivthinclemlopn  15158  ivthinclemlr  15159  ivthinclemuopn  15160  ivthinclemur  15161  ivthinclemloc  15163  ivthinc  15165  ivthreinc  15167  dvfgg  15210  dvcjbr  15230  dvcj  15231  dvfre  15232  elplyr  15262  plyreres  15286  rplogbval  15467  sgmnncl  15510  mpodvdsmulf1o  15512  mersenne  15519  perfectlem2  15522  lgsfcl2  15533  lgsval2lem  15537  lgsmod  15553  lgsdirprm  15561  lgsne0  15565  gausslemma2dlem0h  15583  gausslemma2dlem1a  15585  gausslemma2dlem1f1o  15587  gausslemma2dlem4  15591  lgseisenlem1  15597  lgseisenlem2  15598  lgsquadlem1  15604  lgsquadlem2  15605  lgsquad2lem2  15609  2sqlem8  15650  2sqlem9  15651  structiedg0val  15689  bj-charfundcALT  15859  bj-nnord  16008  bj-inf2vnlem1  16020  pwf1oexmid  16051  nnsf  16057  nninfall  16061  nninfself  16065  exmidsbthrlem  16076  qdencn  16081