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  7334  infeuti  7369  casef1  7430  caseinl  7431  caseinr  7432  difinfsnlem  7439  ctmlemr  7448  ctm  7449  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  enumctlemm  7454  nnnninf  7466  nninfwlpoimlemg  7515  en2other2  7548  exmidfodomrlemim  7553  pw1if  7584  pw1nel3  7590  dftap2  7617  cc2lem  7632  cc4f  7635  addclpi  7694  mulclpi  7695  nnppipi  7710  recmulnqg  7758  enq0ref  7800  nqnq0pi  7805  genipv  7876  addclpr  7904  nqprxx  7913  prmuloc  7933  mulclpr  7939  distrlem1prl  7949  distrlem1pru  7950  ltexprlempr  7975  ltexprlemrl  7977  ltexprlemru  7979  lteupri  7984  recexprlempr  7999  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemloc  8019  cauappcvgprlemcl  8020  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlem2  8027  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlem2  8047  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemupu  8067  caucvgprprlemloc  8070  caucvgprprlemcl  8071  caucvgprprlem2  8077  suplocexprlemex  8089  suplocsrlem  8175  elrealeu  8196  rereceu  8256  axpre-suploclemres  8268  negf1o  8709  aptap  8979  receuap  9000  divvalap  9005  cju  9292  nn0ge2m1nn  9629  nnnegz  9649  elnnz  9656  elnn0z  9659  peano2z  9682  nn0n0n1ge2  9717  msqznn  9748  eluzaddi  9951  eluzsubi  9952  uzind4  9990  supinfneg  9997  infsupneg  9998  elnn1uz2  10009  uz2mulcl  10010  divfnzn  10023  nnrp  10066  rpaddcl  10080  rpmulcl  10081  rpdivcl  10082  rpgecl  10085  ge0p1rp  10088  elrpd  10096  ge0addcl  10385  ge0mulcl  10386  ge0xaddcl  10387  icoshftf1o  10395  peano2fzr  10443  uzsubsubfz  10454  fzsplit2  10457  fzsplit3  10460  elfznn  10462  fzss1  10471  fzss2  10472  fzp1elp1  10484  elfz1b  10499  elfz0fzfz0  10535  fz0fzelfz0  10536  difelfznle  10544  elfzofz  10572  nn0p1elfzo  10596  fzosplitsnm1  10629  ubmelm1fzo  10646  fzofzp1b  10648  fzosplitsn  10653  zsupcllemstep  10664  zsupcl  10666  infssfzcldc  10671  infssfzledc  10672  exbtwnz  10687  flqge0nn0  10730  flqge1nn  10731  zmodcl  10783  modqmuladdnn0  10807  modsumfzodifsn  10835  frec2uzf1od  10845  frec2uzisod  10846  frecuzrdgrrn  10847  frec2uzrdg  10848  frecuzrdgrcl  10849  frecuzrdgtcl  10851  frecuzrdgsuc  10853  frecuzrdgrclt  10854  frecuzrdgfunlem  10858  frecuzrdgtclt  10860  frecuzrdgsuctlem  10862  uzennn  10875  seq3fveq2  10914  seqfveq2g  10916  monoord  10924  iseqf1olemqcl  10938  iseqf1olemnab  10940  iseqf1olemab  10941  iseqf1olemqf1o  10945  seq3f1olemqsumkj  10950  seq3f1olemqsumk  10951  seq3id2  10965  exp3val  10980  expcl2lemap  10990  expclzaplem  11002  expge0  11014  expge1  11015  zsqcl2  11056  bcval4  11192  bcn1  11198  bccl2  11208  hashennnuni  11220  hashunlem  11246  hashdifpr  11263  zfz1isolem1  11294  seq3coll  11296  iswrdiz  11313  ccatsymb  11372  ccatrn  11379  ccat2s1fvwd  11417  swrds1  11442  swrdccat2  11445  swrdccatin2  11503  pfxccatin12lem2  11505  pfxccatin12lem3  11506  pfxccatin12  11507  pfxccat3  11508  pfxccat3a  11512  shftfn  11591  shftf  11597  recvguniq  11763  resqrexlemdecn  11780  rersqreu  11796  nn0abscl  11853  nnabscl  11868  abs2dif  11874  nn0maxcl  11993  climuni  12061  2clim  12069  climcn2  12077  summodclem2a  12150  fsum3  12156  fsum3cvg3  12165  fsumcl2lem  12167  fsumadd  12175  fisum0diag2  12216  fsummulc2  12217  fsumge0  12228  geolim2  12281  cvgratnnlemabsle  12296  cvgratz  12301  mertenslemi1  12304  prodmodclem3  12344  prodmodclem2a  12345  fprodeq0  12386  fprodge0  12406  eff2  12449  tanvalap  12477  zdvdsdc  12581  fzo0dvdseq  12626  oexpneg  12646  oddge22np1  12650  evennn02n  12651  evennn2n  12652  nno  12675  divalglemeunn  12690  divalglemex  12691  divalglemeuneg  12692  divalg  12693  bitsfzolem  12723  bitsinv1lem  12730  divgcdz  12750  bezoutlemmain  12777  bezoutlemmo  12785  bezoutlemeu  12786  bezoutlemle  12787  sqgcd  12808  uzwodc  12816  nninfctlemfo  12819  eucalgval2  12833  eucalglt  12837  lcmneg  12854  lcmgcdlem  12857  ncoprmgcdne1b  12869  prmind2  12900  prmdc  12910  sqnprm  12916  isprm5lem  12921  isprm5  12922  isprm6  12927  sqrt2irrlem  12941  pw2dvdseu  12948  sqpweven  12955  2sqpwodd  12956  sqrt2irrap  12960  qgt0numnn  12979  phicl2  12994  crth  13004  phimullem  13005  eulerthlem1  13007  eulerthlemh  13011  eulerthlemth  13012  hashgcdlem  13018  oddprm  13040  pythagtriplem6  13051  pythagtriplem11  13055  pythagtriplem13  13057  pythagtriplem19  13063  pclem0  13067  pcpremul  13074  pceu  13076  pc2dvds  13111  difsqpwdvds  13119  pcadd  13121  pockthlem  13137  pockthg  13138  1arith  13148  4sqlemffi  13177  4sqlem11  13182  4sqlem12  13183  4sqlem13m  13184  4sqlem14  13185  4sqlem17  13188  ballotfilemic  13252  ballotfilem1c  13253  ballotfilemrc  13276  ballotfilemth  13283  oddennn  13285  evenennn  13286  ennnfoneleminc  13304  ennnfonelemf1  13311  ennnfonelemen  13314  exmidunben  13319  ctinf  13323  ctiunctlemfo  13332  nninfdclemlt  13344  nninfdclemf1  13345  ptex  13620  imasaddfnlemg  13637  imasaddflemg  13639  mgmsscl  13683  sgrp0  13727  sgrp1  13728  hashfinmndnn  13747  ismndd  13752  mndpfo  13753  mhmf1o  13779  0mhm  13795  resmhm  13796  resmhm2  13797  resmhm2b  13798  mhmco  13799  gsumvallem2  13802  isgrpd2e  13827  grpinvf1o  13877  grpinvnzcl  13879  dfgrp3m  13906  mhmmnd  13921  ghmgrp  13923  mulgval  13927  mulgfng  13929  subgmulg  13993  issubg4m  13998  isnsg3  14012  nmzsubg  14015  ssnmz  14016  0nsg  14019  nsgid  14020  ghmnsgima  14073  ghmnsgpreima  14074  ghmf1  14078  kerf1ghm  14079  ghmf1o  14080  conjnmzb  14085  isabld  14104  cmnsubm  14114  ghmcmn  14133  ghmabl  14134  invghm  14135  gsumvalfi  14154  srgfcl  14279  srglmhm  14299  srgrmhm  14300  iscrngd  14349  ringsrg  14354  unitabl  14426  rhmf1o  14477  rhmco  14483  ringelnzr  14496  subrngringnsg  14515  subrgcrng  14535  subrgnzr  14552  resrhm  14558  unitrrg  14578  aprnzr  14601  aprlring  14602  drngnzr  14621  lssneln0  14713  rnglidlmsgrp  14836  quscrng  14872  expghmap  14944  mulgghm2  14945  znf1o  14988  znidom  14994  znidomb  14995  isassad  15013  psrbaglesuppg  15059  psrbagcon  15064  tgtopon  15169  distopon  15190  epttop  15193  resttopon  15274  resttopon2  15281  cnco  15324  lmss  15349  txtopon  15365  uptx  15377  txdis1cn  15381  hmeocnv  15410  hmeof1o2  15411  hmeores  15418  hmeoco  15419  idhmeo  15420  txhmeo  15422  txswaphmeo  15424  psmetxrge0  15435  isxmet2d  15451  metres2  15484  xmetresbl  15543  comet  15602  bdxmet  15604  bdmet  15605  tgioo  15657  mulc1cncf  15692  mulcncflem  15710  cnrehmeocntop  15713  cnopnap  15714  dedekindeu  15726  dedekindicclemicc  15735  ivthinclemlm  15737  ivthinclemum  15738  ivthinclemlopn  15739  ivthinclemlr  15740  ivthinclemuopn  15741  ivthinclemur  15742  ivthinclemloc  15744  ivthinc  15746  ivthreinc  15748  dvfgg  15791  dvcjbr  15811  dvcj  15812  dvfre  15813  elplyr  15843  plyreres  15867  rplogbval  16053  sgmnncl  16108  mpodvdsmulf1o  16110  mersenne  16117  perfectlem2  16120  bcmono  16124  lgsfcl2  16137  lgsval2lem  16141  lgsmod  16157  lgsdirprm  16165  lgsne0  16169  gausslemma2dlem0h  16187  gausslemma2dlem1a  16189  gausslemma2dlem1f1o  16191  gausslemma2dlem4  16195  lgseisenlem1  16201  lgseisenlem2  16202  lgsquadlem1  16208  lgsquadlem2  16209  lgsquad2lem2  16213  2sqlem8  16254  2sqlem9  16255  structiedg0val  16293  ausgrumgrien  16423  usgredgreu  16469  uspgredg2vtxeu  16471  uspgredg2v  16474  usgredg2v  16477  usgr1e  16494  subuhgr  16525  subupgr  16526  subumgr  16527  subusgr  16528  vdegp1aid  16567  trlres  16643  clwwlkbp  16648  clwwlkccatlem  16653  s2elclwwlknon2  16689  clwwlknonex2lem2  16691  clwwlknonex2e  16693  bj-charfundcALT  16847  bj-nnord  16996  bj-inf2vnlem1  17008  pwf1oexmid  17041  nnsf  17060  nninfall  17064  nninfself  17068  exmidsbthrlem  17079  qdencn  17084  alsd  17143  ralsd  17144  alseud  17179  ralseud  17180