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  938  ecase2d  1385  sb2  1813  sbequ1  1814  sbidm  1897  eqeu  2973  euind  2990  reuind  3008  eldifd  3207  eqssd  3241  ssrabdv  3303  elind  3389  dcun  3601  opm  4319  issod  4407  ordsucim  4589  onintonm  4606  ordtri2or2exmidlem  4615  en2lp  4643  ordwe  4665  sosng  4789  sotri2  5122  sotri3  5123  relssdmrn  5245  funun  5358  fnsng  5364  fnprg  5372  fntpg  5373  fntp  5374  fununi  5385  imain  5399  fnco  5427  f00  5513  f1ss  5533  f1ssr  5534  f1ssres  5536  f1f1orn  5579  foimacnv  5586  foun  5587  fun11iun  5589  sefvex  5644  dff3im  5773  fmpt  5778  ffnfv  5786  fmpt2d  5790  ffvresb  5791  fprg  5815  foco2  5870  fcof1  5900  fcofo  5901  fcof1o  5906  fliftf  5916  isoini2  5936  f1oiso  5943  moriotass  5978  fnoprabg  6096  f1ocnvd  6198  suppssfv  6204  suppssov1  6205  1stcof  6299  2ndcof  6300  1stconst  6357  2ndconst  6358  fo2ndf  6363  f1o2ndf1  6364  f1od2  6371  smores2  6430  tfrlem5  6450  tfrlemibfn  6464  tfr1onlembfn  6480  tfri1dALT  6487  tfrcllembfn  6493  nntri2  6630  eroveu  6763  elixpsn  6872  dom2lem  6913  xpf1o  6993  fidifsnen  7020  finexdc  7052  unfidisj  7072  f1finf1o  7102  fidcenumlemrks  7108  sbthlemi9  7120  supeuti  7149  infeuti  7184  casef1  7245  caseinl  7246  caseinr  7247  difinfsnlem  7254  ctmlemr  7263  ctm  7264  ctssdclemn0  7265  ctssdccl  7266  ctssdc  7268  enumctlemm  7269  nnnninf  7281  nninfwlpoimlemg  7330  en2other2  7362  exmidfodomrlemim  7367  pw1if  7398  pw1nel3  7404  dftap2  7425  cc2lem  7440  cc4f  7443  addclpi  7502  mulclpi  7503  nnppipi  7518  recmulnqg  7566  enq0ref  7608  nqnq0pi  7613  genipv  7684  addclpr  7712  nqprxx  7721  prmuloc  7741  mulclpr  7747  distrlem1prl  7757  distrlem1pru  7758  ltexprlempr  7783  ltexprlemrl  7785  ltexprlemru  7787  lteupri  7792  recexprlempr  7807  cauappcvgprlemm  7820  cauappcvgprlemopl  7821  cauappcvgprlemlol  7822  cauappcvgprlemopu  7823  cauappcvgprlemupu  7824  cauappcvgprlemloc  7827  cauappcvgprlemcl  7828  cauappcvgprlemladdfu  7829  cauappcvgprlemladdfl  7830  cauappcvgprlem2  7835  caucvgprlemm  7843  caucvgprlemopl  7844  caucvgprlemlol  7845  caucvgprlemopu  7846  caucvgprlemupu  7847  caucvgprlemloc  7850  caucvgprlemcl  7851  caucvgprlemladdfu  7852  caucvgprlem2  7855  caucvgprprlemml  7869  caucvgprprlemmu  7870  caucvgprprlemopl  7872  caucvgprprlemlol  7873  caucvgprprlemopu  7874  caucvgprprlemupu  7875  caucvgprprlemloc  7878  caucvgprprlemcl  7879  caucvgprprlem2  7885  suplocexprlemex  7897  suplocsrlem  7983  elrealeu  8004  rereceu  8064  axpre-suploclemres  8076  negf1o  8516  aptap  8785  receuap  8804  divvalap  8809  cju  9096  nn0ge2m1nn  9417  nnnegz  9437  elnnz  9444  elnn0z  9447  peano2z  9470  nn0n0n1ge2  9505  msqznn  9535  eluzaddi  9737  eluzsubi  9738  uzind4  9771  supinfneg  9778  infsupneg  9779  elnn1uz2  9790  uz2mulcl  9791  divfnzn  9804  nnrp  9847  rpaddcl  9861  rpmulcl  9862  rpdivcl  9863  rpgecl  9866  ge0p1rp  9869  elrpd  9877  ge0addcl  10165  ge0mulcl  10166  ge0xaddcl  10167  icoshftf1o  10175  peano2fzr  10221  uzsubsubfz  10231  fzsplit2  10234  elfznn  10238  fzss1  10247  fzss2  10248  fzp1elp1  10259  elfz1b  10274  elfz0fzfz0  10310  fz0fzelfz0  10311  difelfznle  10319  elfzofz  10347  fzosplitsnm1  10402  ubmelm1fzo  10419  fzofzp1b  10421  fzosplitsn  10426  zsupcllemstep  10436  zsupcl  10438  exbtwnz  10457  flqge0nn0  10500  flqge1nn  10501  zmodcl  10553  modqmuladdnn0  10577  modsumfzodifsn  10605  frec2uzf1od  10615  frec2uzisod  10616  frecuzrdgrrn  10617  frec2uzrdg  10618  frecuzrdgrcl  10619  frecuzrdgtcl  10621  frecuzrdgsuc  10623  frecuzrdgrclt  10624  frecuzrdgfunlem  10628  frecuzrdgtclt  10630  frecuzrdgsuctlem  10632  uzennn  10645  seq3fveq2  10684  seqfveq2g  10686  monoord  10694  iseqf1olemqcl  10708  iseqf1olemnab  10710  iseqf1olemab  10711  iseqf1olemqf1o  10715  seq3f1olemqsumkj  10720  seq3f1olemqsumk  10721  seq3id2  10735  exp3val  10750  expcl2lemap  10760  expclzaplem  10772  expge0  10784  expge1  10785  zsqcl2  10826  bcval4  10961  bcn1  10967  bccl2  10977  hashennnuni  10988  hashunlem  11013  hashdifpr  11029  zfz1isolem1  11049  seq3coll  11051  iswrdiz  11065  ccatsymb  11123  ccatrn  11130  swrds1  11186  swrdccat2  11189  swrdccatin2  11247  pfxccatin12lem2  11249  pfxccatin12lem3  11250  pfxccatin12  11251  pfxccat3  11252  pfxccat3a  11256  shftfn  11321  shftf  11327  recvguniq  11492  resqrexlemdecn  11509  rersqreu  11525  nn0abscl  11582  nnabscl  11597  abs2dif  11603  nn0maxcl  11722  climuni  11790  2clim  11798  climcn2  11806  summodclem2a  11878  fsum3  11884  fsum3cvg3  11893  fsumcl2lem  11895  fsumadd  11903  fisum0diag2  11944  fsummulc2  11945  fsumge0  11956  geolim2  12009  cvgratnnlemabsle  12024  cvgratz  12029  mertenslemi1  12032  prodmodclem3  12072  prodmodclem2a  12073  fprodeq0  12114  fprodge0  12134  eff2  12177  tanvalap  12205  zdvdsdc  12309  fzo0dvdseq  12354  oexpneg  12374  oddge22np1  12378  evennn02n  12379  evennn2n  12380  nno  12403  divalglemeunn  12418  divalglemex  12419  divalglemeuneg  12420  divalg  12421  bitsfzolem  12451  bitsinv1lem  12458  divgcdz  12478  bezoutlemmain  12505  bezoutlemmo  12513  bezoutlemeu  12514  bezoutlemle  12515  sqgcd  12536  uzwodc  12544  nninfctlemfo  12547  eucalgval2  12561  eucalglt  12565  lcmneg  12582  lcmgcdlem  12585  ncoprmgcdne1b  12597  prmind2  12628  prmdc  12638  sqnprm  12644  isprm5lem  12649  isprm5  12650  isprm6  12655  sqrt2irrlem  12669  pw2dvdseu  12676  sqpweven  12683  2sqpwodd  12684  sqrt2irrap  12688  qgt0numnn  12707  phicl2  12722  hashdvds  12729  crth  12732  phimullem  12733  eulerthlem1  12735  eulerthlemh  12739  eulerthlemth  12740  hashgcdlem  12746  oddprm  12768  pythagtriplem6  12779  pythagtriplem11  12783  pythagtriplem13  12785  pythagtriplem19  12791  pclem0  12795  pcpremul  12802  pceu  12804  pc2dvds  12839  difsqpwdvds  12847  pcadd  12849  pockthlem  12865  pockthg  12866  1arith  12876  4sqlemffi  12905  4sqlem11  12910  4sqlem12  12911  4sqlem13m  12912  4sqlem14  12913  4sqlem17  12916  oddennn  12949  evenennn  12950  ennnfoneleminc  12968  ennnfonelemf1  12975  ennnfonelemen  12978  exmidunben  12983  ctinf  12987  ctiunctlemfo  12996  nninfdclemlt  13008  nninfdclemf1  13009  ptex  13283  imasaddfnlemg  13333  imasaddflemg  13335  mgmsscl  13380  sgrp0  13429  sgrp1  13430  hashfinmndnn  13451  ismndd  13456  mndpfo  13457  mhmf1o  13489  0mhm  13505  resmhm  13506  resmhm2  13507  resmhm2b  13508  mhmco  13509  gsumvallem2  13512  isgrpd2e  13539  grpinvf1o  13589  grpinvnzcl  13591  dfgrp3m  13618  mhmmnd  13639  ghmgrp  13641  mulgval  13645  mulgfng  13647  subgmulg  13711  issubg4m  13716  isnsg3  13730  nmzsubg  13733  ssnmz  13734  0nsg  13737  nsgid  13738  ghmnsgima  13791  ghmnsgpreima  13792  ghmf1  13796  kerf1ghm  13797  ghmf1o  13798  conjnmzb  13803  isabld  13822  ghmcmn  13850  ghmabl  13851  invghm  13852  srgfcl  13922  srglmhm  13942  srgrmhm  13943  iscrngd  13991  ringsrg  13996  unitabl  14066  rhmf1o  14117  rhmco  14123  ringelnzr  14136  subrngringnsg  14154  subrgcrng  14174  subrgnzr  14191  resrhm  14197  unitrrg  14216  lssneln0  14323  rnglidlmsgrp  14446  quscrng  14482  expghmap  14556  mulgghm2  14557  znf1o  14600  znidom  14606  znidomb  14607  psrbaglesuppg  14621  tgtopon  14725  distopon  14746  epttop  14749  resttopon  14830  resttopon2  14837  cnco  14880  lmss  14905  txtopon  14921  uptx  14933  txdis1cn  14937  hmeocnv  14966  hmeof1o2  14967  hmeores  14974  hmeoco  14975  idhmeo  14976  txhmeo  14978  txswaphmeo  14980  psmetxrge0  14991  isxmet2d  15007  metres2  15040  xmetresbl  15099  comet  15158  bdxmet  15160  bdmet  15161  tgioo  15213  mulc1cncf  15248  mulcncflem  15266  cnrehmeocntop  15269  cnopnap  15270  dedekindeu  15282  dedekindicclemicc  15291  ivthinclemlm  15293  ivthinclemum  15294  ivthinclemlopn  15295  ivthinclemlr  15296  ivthinclemuopn  15297  ivthinclemur  15298  ivthinclemloc  15300  ivthinc  15302  ivthreinc  15304  dvfgg  15347  dvcjbr  15367  dvcj  15368  dvfre  15369  elplyr  15399  plyreres  15423  rplogbval  15604  sgmnncl  15647  mpodvdsmulf1o  15649  mersenne  15656  perfectlem2  15659  lgsfcl2  15670  lgsval2lem  15674  lgsmod  15690  lgsdirprm  15698  lgsne0  15702  gausslemma2dlem0h  15720  gausslemma2dlem1a  15722  gausslemma2dlem1f1o  15724  gausslemma2dlem4  15728  lgseisenlem1  15734  lgseisenlem2  15735  lgsquadlem1  15741  lgsquadlem2  15742  lgsquad2lem2  15746  2sqlem8  15787  2sqlem9  15788  structiedg0val  15826  ausgrumgrien  15953  usgredgreu  15999  uspgredg2vtxeu  16001  uspgredg2v  16004  usgredg2v  16007  bj-charfundcALT  16102  bj-nnord  16251  bj-inf2vnlem1  16263  pwf1oexmid  16296  nnsf  16302  nninfall  16306  nninfself  16310  exmidsbthrlem  16321  qdencn  16326