Theorem sylanbrc 421

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 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  dcand  945  ecase2d  1392  sb2  1820  sbequ1  1821  sbidm  1904  eqeu  2996  euind  3013  reuind  3031  eldifd  3230  eqssd  3265  ssrabdv  3327  elind  3414  dcun  3637  opm  4374  issod  4464  ordsucim  4647  onintonm  4664  ordtri2or2exmidlem  4673  en2lp  4701  ordwe  4723  sosng  4848  sotri2  5185  sotri3  5186  relssdmrn  5308  funun  5422  fnsng  5428  fnprg  5436  fntpg  5437  fntp  5438  fununi  5449  imain  5463  fnco  5491  f00  5584  f1ss  5604  f1ssr  5605  f1ssres  5607  f1f1orn  5650  foimacnv  5657  foun  5658  fun11iun  5660  sefvex  5716  dff3im  5853  fmpt  5858  ffnfv  5866  fmpt2d  5870  ffvresb  5871  fprg  5898  foco2  5959  fcof1  5989  fcofo  5990  fcof1o  5995  fliftf  6005  isoini2  6025  f1oiso  6032  moriotass  6069  fnoprabg  6189  f1ocnvd  6292  f1o3d  6298  suppssov1  6299  1stcof  6397  2ndcof  6398  1stconst  6457  2ndconst  6458  fo2ndf  6463  f1o2ndf1  6464  f1od2  6471  suppssfvg  6503  smores2  6565  tfrlem5  6585  tfrlemibfn  6599  tfr1onlembfn  6615  tfri1dALT  6622  tfrcllembfn  6628  nntri2  6767  eroveu  6900  elixpsn  7017  dom2lem  7058  xpf1o  7144  fidifsnen  7172  finexdc  7207  elssdc  7209  unfidisj  7229  f1finf1o  7264  fidcenumlemrks  7270  sbthlemi9  7282  supeuti  7335  infeuti  7370  casef1  7431  caseinl  7432  caseinr  7433  difinfsnlem  7440  ctmlemr  7449  ctm  7450  ctssdclemn0  7451  ctssdccl  7452  ctssdc  7454  enumctlemm  7455  nnnninf  7467  nninfwlpoimlemg  7516  en2other2  7549  exmidfodomrlemim  7554  pw1if  7585  pw1nel3  7591  dftap2  7618  cc2lem  7633  cc4f  7636  addclpi  7695  mulclpi  7696  nnppipi  7711  recmulnqg  7759  enq0ref  7801  nqnq0pi  7806  genipv  7877  addclpr  7905  nqprxx  7914  prmuloc  7934  mulclpr  7940  distrlem1prl  7950  distrlem1pru  7951  ltexprlempr  7976  ltexprlemrl  7978  ltexprlemru  7980  lteupri  7985  recexprlempr  8000  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemloc  8020  cauappcvgprlemcl  8021  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlem2  8028  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlem2  8048  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemupu  8068  caucvgprprlemloc  8071  caucvgprprlemcl  8072  caucvgprprlem2  8078  suplocexprlemex  8090  suplocsrlem  8176  elrealeu  8197  rereceu  8257  axpre-suploclemres  8269  negf1o  8711  aptap  8981  receuap  9002  divvalap  9007  cju  9294  nn0ge2m1nn  9632  nnnegz  9652  elnnz  9659  elnn0z  9662  peano2z  9685  nn0n0n1ge2  9720  msqznn  9751  eluzaddi  9959  eluzsubi  9960  uzind4  9998  supinfneg  10005  infsupneg  10006  elnn1uz2  10017  uz2mulcl  10018  divfnzn  10031  nnrp  10075  rpaddcl  10089  rpmulcl  10090  rpdivcl  10091  rpgecl  10094  ge0p1rp  10097  elrpd  10105  ge0addcl  10394  ge0mulcl  10395  ge0xaddcl  10396  icoshftf1o  10404  peano2fzr  10452  uzsubsubfz  10463  fzsplit2  10466  fzsplit3  10469  elfznn  10471  fzss1  10480  fzss2  10481  fzp1elp1  10493  elfz1b  10508  elfz0fzfz0  10544  fz0fzelfz0  10545  difelfznle  10553  elfzofz  10581  nn0p1elfzo  10605  fzosplitsnm1  10638  ubmelm1fzo  10655  fzofzp1b  10657  fzosplitsn  10662  zsupcllemstep  10673  zsupcl  10675  infssfzcldc  10680  infssfzledc  10681  exbtwnz  10696  flqge0nn0  10742  flqge1nn  10743  zmodcl  10795  modqmuladdnn0  10819  modsumfzodifsn  10847  frec2uzf1od  10857  frec2uzisod  10858  frecuzrdgrrn  10859  frec2uzrdg  10860  frecuzrdgrcl  10861  frecuzrdgtcl  10863  frecuzrdgsuc  10865  frecuzrdgrclt  10866  frecuzrdgfunlem  10870  frecuzrdgtclt  10872  frecuzrdgsuctlem  10874  uzennn  10887  seq3fveq2  10926  seqfveq2g  10928  monoord  10936  iseqf1olemqcl  10950  iseqf1olemnab  10952  iseqf1olemab  10953  iseqf1olemqf1o  10957  seq3f1olemqsumkj  10962  seq3f1olemqsumk  10963  seq3id2  10977  exp3val  10992  expcl2lemap  11002  expclzaplem  11014  expge0  11026  expge1  11027  zsqcl2  11068  bcval4  11205  bcn1  11211  bccl2  11221  hashennnuni  11233  hashunlem  11259  hashdifpr  11276  zfz1isolem1  11307  seq3coll  11309  iswrdiz  11326  ccatsymb  11385  ccatrn  11392  ccat2s1fvwd  11430  swrds1  11455  swrdccat2  11458  swrdccatin2  11516  pfxccatin12lem2  11518  pfxccatin12lem3  11519  pfxccatin12  11520  pfxccat3  11521  pfxccat3a  11525  shftfn  11604  shftf  11610  recvguniq  11776  resqrexlemdecn  11793  rersqreu  11809  nn0abscl  11867  nnabscl  11882  abs2dif  11888  nn0maxcl  12007  fiidxsupcl  12011  climuni  12077  2clim  12085  climcn2  12093  summodclem2a  12166  fsum3  12172  fsum3cvg3  12181  fsumcl2lem  12183  fsumadd  12191  fisum0diag2  12232  fsummulc2  12233  fsumge0  12244  geolim2  12297  cvgratnnlemabsle  12312  cvgratz  12317  mertenslemi1  12320  prodmodclem3  12360  prodmodclem2a  12361  fprodeq0  12402  fprodge0  12422  eff2  12465  tanvalap  12493  zdvdsdc  12597  fzo0dvdseq  12642  oexpneg  12662  oddge22np1  12666  evennn02n  12667  evennn2n  12668  nno  12691  divalglemeunn  12706  divalglemex  12707  divalglemeuneg  12708  divalg  12709  bitsfzolem  12739  bitsinv1lem  12746  divgcdz  12766  bezoutlemmain  12793  bezoutlemmo  12801  bezoutlemeu  12802  bezoutlemle  12803  sqgcd  12824  uzwodc  12832  nninfctlemfo  12835  eucalgval2  12849  eucalglt  12853  lcmneg  12870  lcmgcdlem  12873  ncoprmgcdne1b  12885  prmind2  12916  prmdc  12926  sqnprm  12933  isprm5lem  12938  isprm5  12939  isprm6  12944  sqrt2irrlem  12958  pwbdvdseu  12965  sqpweven  12973  2sqpwodd  12974  sqrt2irrap  12978  qgt0numnn  12997  nn0sqdcq  13006  phicl2  13014  crth  13024  phimullem  13025  eulerthlem1  13027  eulerthlemh  13031  eulerthlemth  13032  hashgcdlem  13038  oddprm  13060  pythagtriplem6  13071  pythagtriplem11  13075  pythagtriplem13  13077  pythagtriplem19  13083  pclem0  13087  pcpremul  13094  pceu  13096  pc2dvds  13131  difsqpwdvds  13139  pcadd  13141  pockthlem  13157  pockthg  13158  1arith  13168  4sqlemffi  13197  4sqlem11  13202  4sqlem12  13203  4sqlem13m  13204  4sqlem14  13205  4sqlem17  13208  ballotfilemic  13301  ballotfilem1c  13302  ballotfilemrc  13325  ballotfilemth  13332  oddennn  13334  evenennn  13335  ennnfoneleminc  13353  ennnfonelemf1  13360  ennnfonelemen  13363  exmidunben  13368  ctinf  13372  ctiunctlemfo  13381  nninfdclemlt  13393  nninfdclemf1  13394  ptex  13669  imasaddfnlemg  13686  imasaddflemg  13688  mgmsscl  13732  sgrp0  13776  sgrp1  13777  hashfinmndnn  13796  ismndd  13801  mndpfo  13802  mhmf1o  13828  0mhm  13844  resmhm  13845  resmhm2  13846  resmhm2b  13847  mhmco  13848  gsumvallem2  13851  isgrpd2e  13876  grpinvf1o  13926  grpinvnzcl  13928  dfgrp3m  13955  mhmmnd  13970  ghmgrp  13972  mulgval  13976  mulgfng  13978  subgmulg  14042  issubg4m  14047  isnsg3  14061  nmzsubg  14064  ssnmz  14065  0nsg  14068  nsgid  14069  ghmnsgima  14122  ghmnsgpreima  14123  ghmf1  14127  kerf1ghm  14128  ghmf1o  14129  conjnmzb  14134  isabld  14153  cmnsubm  14163  ghmcmn  14182  ghmabl  14183  invghm  14184  gsumvalfi  14203  srgfcl  14328  srglmhm  14348  srgrmhm  14349  iscrngd  14398  ringsrg  14403  unitabl  14475  rhmf1o  14526  rhmco  14532  ringelnzr  14545  subrngringnsg  14564  subrgcrng  14584  subrgnzr  14601  resrhm  14607  unitrrg  14627  aprnzr  14650  aprlring  14651  drngnzr  14670  lssneln0  14762  rnglidlmsgrp  14885  quscrng  14921  expghmap  14993  mulgghm2  14994  znf1o  15037  znidom  15043  znidomb  15044  isassad  15062  psrbaglesuppg  15108  psrbagcon  15113  psrbaglefifi  15114  tgtopon  15219  distopon  15240  epttop  15243  resttopon  15324  resttopon2  15331  cnco  15374  lmss  15399  txtopon  15415  uptx  15427  txdis1cn  15431  hmeocnv  15460  hmeof1o2  15461  hmeores  15468  hmeoco  15469  idhmeo  15470  txhmeo  15472  txswaphmeo  15474  psmetxrge0  15485  isxmet2d  15501  metres2  15534  xmetresbl  15593  comet  15652  bdxmet  15654  bdmet  15655  tgioo  15707  mulc1cncf  15742  mulcncflem  15760  cnrehmeocntop  15763  cnopnap  15764  dedekindeu  15776  dedekindicclemicc  15785  ivthinclemlm  15787  ivthinclemum  15788  ivthinclemlopn  15789  ivthinclemlr  15790  ivthinclemuopn  15791  ivthinclemur  15792  ivthinclemloc  15794  ivthinc  15796  ivthreinc  15798  dvfgg  15841  dvcjbr  15861  dvcj  15862  dvfre  15863  elplyr  15893  plyreres  15917  rplogbval  16103  ppiqsval  16162  ppiqsval2  16163  ppiqfi  16164  sgmnncl  16179  chtdif  16186  ppidif  16191  ppiqnncl  16200  mpodvdsmulf1o  16206  mersenne  16219  perfectlem2  16222  bcmono  16226  bposlem1  16233  bposlem3  16235  bposlem4  16236  bposlem5  16237  lgsfcl2  16247  lgsval2lem  16251  lgsmod  16267  lgsdirprm  16275  lgsne0  16279  gausslemma2dlem0h  16297  gausslemma2dlem1a  16299  gausslemma2dlem1f1o  16301  gausslemma2dlem4  16305  lgseisenlem1  16311  lgseisenlem2  16312  lgsquadlem1  16318  lgsquadlem2  16319  lgsquad2lem2  16323  2sqlem8  16364  2sqlem9  16365  structiedg0val  16403  ausgrumgrien  16533  usgredgreu  16579  uspgredg2vtxeu  16581  uspgredg2v  16584  usgredg2v  16587  usgr1e  16604  subuhgr  16635  subupgr  16636  subumgr  16637  subusgr  16638  vdegp1aid  16677  trlres  16753  clwwlkbp  16758  clwwlkccatlem  16763  s2elclwwlknon2  16799  clwwlknonex2lem2  16801  clwwlknonex2e  16803  bj-charfundcALT  16957  bj-nnord  17106  bj-inf2vnlem1  17118  pwf1oexmid  17151  nnsf  17170  nninfall  17174  nninfself  17178  exmidsbthrlem  17189  qdencn  17194  alsd  17253  ralsd  17254  alseud  17289  ralseud  17290