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  7275  exmidfodomrlemim  7280  pw1nel3  7314  dftap2  7334  cc2lem  7349  cc4f  7352  addclpi  7411  mulclpi  7412  nnppipi  7427  recmulnqg  7475  enq0ref  7517  nqnq0pi  7522  genipv  7593  addclpr  7621  nqprxx  7630  prmuloc  7650  mulclpr  7656  distrlem1prl  7666  distrlem1pru  7667  ltexprlempr  7692  ltexprlemrl  7694  ltexprlemru  7696  lteupri  7701  recexprlempr  7716  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemopu  7732  cauappcvgprlemupu  7733  cauappcvgprlemloc  7736  cauappcvgprlemcl  7737  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlem2  7744  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemopu  7755  caucvgprlemupu  7756  caucvgprlemloc  7759  caucvgprlemcl  7760  caucvgprlemladdfu  7761  caucvgprlem2  7764  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemopu  7783  caucvgprprlemupu  7784  caucvgprprlemloc  7787  caucvgprprlemcl  7788  caucvgprprlem2  7794  suplocexprlemex  7806  suplocsrlem  7892  elrealeu  7913  rereceu  7973  axpre-suploclemres  7985  negf1o  8425  aptap  8694  receuap  8713  divvalap  8718  cju  9005  nn0ge2m1nn  9326  nnnegz  9346  elnnz  9353  elnn0z  9356  peano2z  9379  nn0n0n1ge2  9413  msqznn  9443  eluzaddi  9645  eluzsubi  9646  uzind4  9679  supinfneg  9686  infsupneg  9687  elnn1uz2  9698  uz2mulcl  9699  divfnzn  9712  nnrp  9755  rpaddcl  9769  rpmulcl  9770  rpdivcl  9771  rpgecl  9774  ge0p1rp  9777  elrpd  9785  ge0addcl  10073  ge0mulcl  10074  ge0xaddcl  10075  icoshftf1o  10083  peano2fzr  10129  uzsubsubfz  10139  fzsplit2  10142  elfznn  10146  fzss1  10155  fzss2  10156  fzp1elp1  10167  elfz1b  10182  elfz0fzfz0  10218  fz0fzelfz0  10219  difelfznle  10227  elfzofz  10255  fzosplitsnm1  10302  ubmelm1fzo  10319  fzofzp1b  10321  fzosplitsn  10326  zsupcllemstep  10336  zsupcl  10338  exbtwnz  10357  flqge0nn0  10400  flqge1nn  10401  zmodcl  10453  modqmuladdnn0  10477  modsumfzodifsn  10505  frec2uzf1od  10515  frec2uzisod  10516  frecuzrdgrrn  10517  frec2uzrdg  10518  frecuzrdgrcl  10519  frecuzrdgtcl  10521  frecuzrdgsuc  10523  frecuzrdgrclt  10524  frecuzrdgfunlem  10528  frecuzrdgtclt  10530  frecuzrdgsuctlem  10532  uzennn  10545  seq3fveq2  10584  seqfveq2g  10586  monoord  10594  iseqf1olemqcl  10608  iseqf1olemnab  10610  iseqf1olemab  10611  iseqf1olemqf1o  10615  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3id2  10635  exp3val  10650  expcl2lemap  10660  expclzaplem  10672  expge0  10684  expge1  10685  zsqcl2  10726  bcval4  10861  bcn1  10867  bccl2  10877  hashennnuni  10888  hashunlem  10913  hashdifpr  10929  zfz1isolem1  10949  seq3coll  10951  iswrdiz  10959  shftfn  11006  shftf  11012  recvguniq  11177  resqrexlemdecn  11194  rersqreu  11210  nn0abscl  11267  nnabscl  11282  abs2dif  11288  nn0maxcl  11407  climuni  11475  2clim  11483  climcn2  11491  summodclem2a  11563  fsum3  11569  fsum3cvg3  11578  fsumcl2lem  11580  fsumadd  11588  fisum0diag2  11629  fsummulc2  11630  fsumge0  11641  geolim2  11694  cvgratnnlemabsle  11709  cvgratz  11714  mertenslemi1  11717  prodmodclem3  11757  prodmodclem2a  11758  fprodeq0  11799  fprodge0  11819  eff2  11862  tanvalap  11890  zdvdsdc  11994  fzo0dvdseq  12039  oexpneg  12059  oddge22np1  12063  evennn02n  12064  evennn2n  12065  nno  12088  divalglemeunn  12103  divalglemex  12104  divalglemeuneg  12105  divalg  12106  bitsfzolem  12136  bitsinv1lem  12143  divgcdz  12163  bezoutlemmain  12190  bezoutlemmo  12198  bezoutlemeu  12199  bezoutlemle  12200  sqgcd  12221  uzwodc  12229  nninfctlemfo  12232  eucalgval2  12246  eucalglt  12250  lcmneg  12267  lcmgcdlem  12270  ncoprmgcdne1b  12282  prmind2  12313  prmdc  12323  sqnprm  12329  isprm5lem  12334  isprm5  12335  isprm6  12340  sqrt2irrlem  12354  pw2dvdseu  12361  sqpweven  12368  2sqpwodd  12369  sqrt2irrap  12373  qgt0numnn  12392  phicl2  12407  hashdvds  12414  crth  12417  phimullem  12418  eulerthlem1  12420  eulerthlemh  12424  eulerthlemth  12425  hashgcdlem  12431  oddprm  12453  pythagtriplem6  12464  pythagtriplem11  12468  pythagtriplem13  12470  pythagtriplem19  12476  pclem0  12480  pcpremul  12487  pceu  12489  pc2dvds  12524  difsqpwdvds  12532  pcadd  12534  pockthlem  12550  pockthg  12551  1arith  12561  4sqlemffi  12590  4sqlem11  12595  4sqlem12  12596  4sqlem13m  12597  4sqlem14  12598  4sqlem17  12601  oddennn  12634  evenennn  12635  ennnfoneleminc  12653  ennnfonelemf1  12660  ennnfonelemen  12663  exmidunben  12668  ctinf  12672  ctiunctlemfo  12681  nninfdclemlt  12693  nninfdclemf1  12694  ptex  12966  imasaddfnlemg  13016  imasaddflemg  13018  mgmsscl  13063  sgrp0  13112  sgrp1  13113  hashfinmndnn  13134  ismndd  13139  mndpfo  13140  mhmf1o  13172  0mhm  13188  resmhm  13189  resmhm2  13190  resmhm2b  13191  mhmco  13192  gsumvallem2  13195  isgrpd2e  13222  grpinvf1o  13272  grpinvnzcl  13274  dfgrp3m  13301  mhmmnd  13322  ghmgrp  13324  mulgval  13328  mulgfng  13330  subgmulg  13394  issubg4m  13399  isnsg3  13413  nmzsubg  13416  ssnmz  13417  0nsg  13420  nsgid  13421  ghmnsgima  13474  ghmnsgpreima  13475  ghmf1  13479  kerf1ghm  13480  ghmf1o  13481  conjnmzb  13486  isabld  13505  ghmcmn  13533  ghmabl  13534  invghm  13535  srgfcl  13605  srglmhm  13625  srgrmhm  13626  iscrngd  13674  ringsrg  13679  unitabl  13749  rhmf1o  13800  rhmco  13806  ringelnzr  13819  subrngringnsg  13837  subrgcrng  13857  subrgnzr  13874  resrhm  13880  unitrrg  13899  lssneln0  14006  rnglidlmsgrp  14129  quscrng  14165  expghmap  14239  mulgghm2  14240  znf1o  14283  znidom  14289  znidomb  14290  psrbaglesuppg  14302  tgtopon  14386  distopon  14407  epttop  14410  resttopon  14491  resttopon2  14498  cnco  14541  lmss  14566  txtopon  14582  uptx  14594  txdis1cn  14598  hmeocnv  14627  hmeof1o2  14628  hmeores  14635  hmeoco  14636  idhmeo  14637  txhmeo  14639  txswaphmeo  14641  psmetxrge0  14652  isxmet2d  14668  metres2  14701  xmetresbl  14760  comet  14819  bdxmet  14821  bdmet  14822  tgioo  14874  mulc1cncf  14909  mulcncflem  14927  cnrehmeocntop  14930  cnopnap  14931  dedekindeu  14943  dedekindicclemicc  14952  ivthinclemlm  14954  ivthinclemum  14955  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemloc  14961  ivthinc  14963  ivthreinc  14965  dvfgg  15008  dvcjbr  15028  dvcj  15029  dvfre  15030  elplyr  15060  plyreres  15084  rplogbval  15265  sgmnncl  15308  mpodvdsmulf1o  15310  mersenne  15317  perfectlem2  15320  lgsfcl2  15331  lgsval2lem  15335  lgsmod  15351  lgsdirprm  15359  lgsne0  15363  gausslemma2dlem0h  15381  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  gausslemma2dlem4  15389  lgseisenlem1  15395  lgseisenlem2  15396  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem2  15407  2sqlem8  15448  2sqlem9  15449  bj-charfundcALT  15539  bj-nnord  15688  bj-inf2vnlem1  15700  pwf1oexmid  15730  nnsf  15736  nninfall  15740  nninfself  15744  exmidsbthrlem  15753  qdencn  15758