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  2931  euind  2948  reuind  2966  eldifd  3164  eqssd  3197  ssrabdv  3259  elind  3345  dcun  3557  opm  4264  issod  4351  ordsucim  4533  onintonm  4550  ordtri2or2exmidlem  4559  en2lp  4587  ordwe  4609  sosng  4733  sotri2  5064  sotri3  5065  relssdmrn  5187  funun  5299  fnsng  5302  fnprg  5310  fntpg  5311  fntp  5312  fununi  5323  imain  5337  fnco  5363  f00  5446  f1ss  5466  f1ssr  5467  f1ssres  5469  f1f1orn  5512  foimacnv  5519  foun  5520  fun11iun  5522  sefvex  5576  dff3im  5704  fmpt  5709  ffnfv  5717  fmpt2d  5721  ffvresb  5722  fprg  5742  foco2  5797  fcof1  5827  fcofo  5828  fcof1o  5833  fliftf  5843  isoini2  5863  f1oiso  5870  moriotass  5903  fnoprabg  6020  f1ocnvd  6122  suppssfv  6128  suppssov1  6129  1stcof  6218  2ndcof  6219  1stconst  6276  2ndconst  6277  fo2ndf  6282  f1o2ndf1  6283  f1od2  6290  smores2  6349  tfrlem5  6369  tfrlemibfn  6383  tfr1onlembfn  6399  tfri1dALT  6406  tfrcllembfn  6412  nntri2  6549  eroveu  6682  elixpsn  6791  dom2lem  6828  xpf1o  6902  fidifsnen  6928  finexdc  6960  unfidisj  6980  f1finf1o  7008  fidcenumlemrks  7014  sbthlemi9  7026  supeuti  7055  infeuti  7090  casef1  7151  caseinl  7152  caseinr  7153  difinfsnlem  7160  ctmlemr  7169  ctm  7170  ctssdclemn0  7171  ctssdccl  7172  ctssdc  7174  enumctlemm  7175  nnnninf  7187  nninfwlpoimlemg  7236  en2other2  7258  exmidfodomrlemim  7263  pw1nel3  7293  dftap2  7313  cc2lem  7328  cc4f  7331  addclpi  7389  mulclpi  7390  nnppipi  7405  recmulnqg  7453  enq0ref  7495  nqnq0pi  7500  genipv  7571  addclpr  7599  nqprxx  7608  prmuloc  7628  mulclpr  7634  distrlem1prl  7644  distrlem1pru  7645  ltexprlempr  7670  ltexprlemrl  7672  ltexprlemru  7674  lteupri  7679  recexprlempr  7694  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemopu  7710  cauappcvgprlemupu  7711  cauappcvgprlemloc  7714  cauappcvgprlemcl  7715  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlem2  7722  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemopu  7733  caucvgprlemupu  7734  caucvgprlemloc  7737  caucvgprlemcl  7738  caucvgprlemladdfu  7739  caucvgprlem2  7742  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemupu  7762  caucvgprprlemloc  7765  caucvgprprlemcl  7766  caucvgprprlem2  7772  suplocexprlemex  7784  suplocsrlem  7870  elrealeu  7891  rereceu  7951  axpre-suploclemres  7963  negf1o  8403  aptap  8671  receuap  8690  divvalap  8695  cju  8982  nn0ge2m1nn  9303  nnnegz  9323  elnnz  9330  elnn0z  9333  peano2z  9356  nn0n0n1ge2  9390  msqznn  9420  eluzaddi  9622  eluzsubi  9623  uzind4  9656  supinfneg  9663  infsupneg  9664  elnn1uz2  9675  uz2mulcl  9676  divfnzn  9689  nnrp  9732  rpaddcl  9746  rpmulcl  9747  rpdivcl  9748  rpgecl  9751  ge0p1rp  9754  elrpd  9762  ge0addcl  10050  ge0mulcl  10051  ge0xaddcl  10052  icoshftf1o  10060  peano2fzr  10106  uzsubsubfz  10116  fzsplit2  10119  elfznn  10123  fzss1  10132  fzss2  10133  fzp1elp1  10144  elfz1b  10159  elfz0fzfz0  10195  fz0fzelfz0  10196  difelfznle  10204  elfzofz  10232  fzosplitsnm1  10279  ubmelm1fzo  10296  fzofzp1b  10298  fzosplitsn  10303  exbtwnz  10322  flqge0nn0  10365  flqge1nn  10366  zmodcl  10418  modqmuladdnn0  10442  modsumfzodifsn  10470  frec2uzf1od  10480  frec2uzisod  10481  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgtcl  10486  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgfunlem  10493  frecuzrdgtclt  10495  frecuzrdgsuctlem  10497  uzennn  10510  seq3fveq2  10549  seqfveq2g  10551  monoord  10559  iseqf1olemqcl  10573  iseqf1olemnab  10575  iseqf1olemab  10576  iseqf1olemqf1o  10580  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3id2  10600  exp3val  10615  expcl2lemap  10625  expclzaplem  10637  expge0  10649  expge1  10650  zsqcl2  10691  bcval4  10826  bcn1  10832  bccl2  10842  hashennnuni  10853  hashunlem  10878  hashdifpr  10894  zfz1isolem1  10914  seq3coll  10916  iswrdiz  10924  shftfn  10971  shftf  10977  recvguniq  11142  resqrexlemdecn  11159  rersqreu  11175  nn0abscl  11232  nnabscl  11247  abs2dif  11253  climuni  11439  2clim  11447  climcn2  11455  summodclem2a  11527  fsum3  11533  fsum3cvg3  11542  fsumcl2lem  11544  fsumadd  11552  fisum0diag2  11593  fsummulc2  11594  fsumge0  11605  geolim2  11658  cvgratnnlemabsle  11673  cvgratz  11678  mertenslemi1  11681  prodmodclem3  11721  prodmodclem2a  11722  fprodeq0  11763  fprodge0  11783  eff2  11826  tanvalap  11854  zdvdsdc  11958  fzo0dvdseq  12002  oexpneg  12021  oddge22np1  12025  evennn02n  12026  evennn2n  12027  nno  12050  divalglemeunn  12065  divalglemex  12066  divalglemeuneg  12067  divalg  12068  zsupcllemstep  12085  zsupcl  12087  divgcdz  12111  bezoutlemmain  12138  bezoutlemmo  12146  bezoutlemeu  12147  bezoutlemle  12148  sqgcd  12169  uzwodc  12177  nninfctlemfo  12180  eucalgval2  12194  eucalglt  12198  lcmneg  12215  lcmgcdlem  12218  ncoprmgcdne1b  12230  prmind2  12261  prmdc  12271  sqnprm  12277  isprm5lem  12282  isprm5  12283  isprm6  12288  sqrt2irrlem  12302  pw2dvdseu  12309  sqpweven  12316  2sqpwodd  12317  sqrt2irrap  12321  qgt0numnn  12340  phicl2  12355  hashdvds  12362  crth  12365  phimullem  12366  eulerthlem1  12368  eulerthlemh  12372  eulerthlemth  12373  hashgcdlem  12379  oddprm  12400  pythagtriplem6  12411  pythagtriplem11  12415  pythagtriplem13  12417  pythagtriplem19  12423  pclem0  12427  pcpremul  12434  pceu  12436  pc2dvds  12471  difsqpwdvds  12479  pcadd  12481  pockthlem  12497  pockthg  12498  1arith  12508  4sqlemffi  12537  4sqlem11  12542  4sqlem12  12543  4sqlem13m  12544  4sqlem14  12545  4sqlem17  12548  oddennn  12552  evenennn  12553  ennnfoneleminc  12571  ennnfonelemf1  12578  ennnfonelemen  12581  exmidunben  12586  ctinf  12590  ctiunctlemfo  12599  nninfdclemlt  12611  nninfdclemf1  12612  ptex  12878  imasaddfnlemg  12900  imasaddflemg  12902  mgmsscl  12947  sgrp0  12996  sgrp1  12997  hashfinmndnn  13016  ismndd  13021  mndpfo  13022  mhmf1o  13045  0mhm  13061  resmhm  13062  resmhm2  13063  resmhm2b  13064  mhmco  13065  gsumvallem2  13068  isgrpd2e  13095  grpinvf1o  13145  grpinvnzcl  13147  dfgrp3m  13174  mhmmnd  13189  ghmgrp  13191  mulgval  13195  mulgfng  13197  subgmulg  13261  issubg4m  13266  isnsg3  13280  nmzsubg  13283  ssnmz  13284  0nsg  13287  nsgid  13288  ghmnsgima  13341  ghmnsgpreima  13342  ghmf1  13346  kerf1ghm  13347  ghmf1o  13348  conjnmzb  13353  isabld  13372  ghmcmn  13400  ghmabl  13401  invghm  13402  srgfcl  13472  srglmhm  13492  srgrmhm  13493  iscrngd  13541  ringsrg  13546  unitabl  13616  rhmf1o  13667  rhmco  13673  ringelnzr  13686  subrngringnsg  13704  subrgcrng  13724  subrgnzr  13741  resrhm  13747  unitrrg  13766  lssneln0  13873  rnglidlmsgrp  13996  quscrng  14032  expghmap  14106  mulgghm2  14107  znf1o  14150  znidom  14156  znidomb  14157  psrbaglesuppg  14169  tgtopon  14245  distopon  14266  epttop  14269  resttopon  14350  resttopon2  14357  cnco  14400  lmss  14425  txtopon  14441  uptx  14453  txdis1cn  14457  hmeocnv  14486  hmeof1o2  14487  hmeores  14494  hmeoco  14495  idhmeo  14496  txhmeo  14498  txswaphmeo  14500  psmetxrge0  14511  isxmet2d  14527  metres2  14560  xmetresbl  14619  comet  14678  bdxmet  14680  bdmet  14681  tgioo  14733  mulc1cncf  14768  mulcncflem  14786  cnrehmeocntop  14789  cnopnap  14790  dedekindeu  14802  dedekindicclemicc  14811  ivthinclemlm  14813  ivthinclemum  14814  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemloc  14820  ivthinc  14822  ivthreinc  14824  dvfgg  14867  dvcjbr  14887  dvcj  14888  dvfre  14889  elplyr  14919  plyreres  14942  rplogbval  15118  lgsfcl2  15163  lgsval2lem  15167  lgsmod  15183  lgsdirprm  15191  lgsne0  15195  gausslemma2dlem0h  15213  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  gausslemma2dlem4  15221  lgseisenlem1  15227  lgseisenlem2  15228  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem2  15239  2sqlem8  15280  2sqlem9  15281  bj-charfundcALT  15371  bj-nnord  15520  bj-inf2vnlem1  15532  pwf1oexmid  15560  nnsf  15565  nninfall  15569  nninfself  15573  exmidsbthrlem  15582  qdencn  15587