Theorem sylanbrc 414

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 304	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		sylanbrc.3	. 2 ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))
5	3, 4	sylibr 133	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sb2  1754  sbequ1  1755  sbidm  1838  eqeu  2891  euind  2908  reuind  2926  eldifd  3121  eqssd  3154  ssrabdv  3216  elind  3302  dcun  3514  opm  4206  issod  4291  ordsucim  4471  onintonm  4488  ordtri2or2exmidlem  4497  en2lp  4525  ordwe  4547  sosng  4671  sotri2  4995  sotri3  4996  relssdmrn  5118  funun  5226  fnsng  5229  fnprg  5237  fntpg  5238  fntp  5239  fununi  5250  imain  5264  fnco  5290  f00  5373  f1ss  5393  f1ssr  5394  f1ssres  5396  f1f1orn  5437  foimacnv  5444  foun  5445  fun11iun  5447  sefvex  5501  dff3im  5624  fmpt  5629  ffnfv  5637  fmpt2d  5641  ffvresb  5642  fprg  5662  foco2  5716  fcof1  5745  fcofo  5746  fcof1o  5751  fliftf  5761  isoini2  5781  f1oiso  5788  moriotass  5820  fnoprabg  5934  f1ocnvd  6034  suppssfv  6040  suppssov1  6041  1stcof  6123  2ndcof  6124  1stconst  6180  2ndconst  6181  fo2ndf  6186  f1o2ndf1  6187  f1od2  6194  smores2  6253  tfrlem5  6273  tfrlemibfn  6287  tfr1onlembfn  6303  tfri1dALT  6310  tfrcllembfn  6316  nntri2  6453  eroveu  6583  elixpsn  6692  dom2lem  6729  xpf1o  6801  fidifsnen  6827  finexdc  6859  unfidisj  6878  f1finf1o  6903  fidcenumlemrks  6909  sbthlemi9  6921  supeuti  6950  infeuti  6985  casef1  7046  caseinl  7047  caseinr  7048  difinfsnlem  7055  ctmlemr  7064  ctm  7065  ctssdclemn0  7066  ctssdccl  7067  ctssdc  7069  enumctlemm  7070  nnnninf  7081  en2other2  7143  exmidfodomrlemim  7148  pw1nel3  7178  cc2lem  7198  cc4f  7201  addclpi  7259  mulclpi  7260  nnppipi  7275  recmulnqg  7323  enq0ref  7365  nqnq0pi  7370  genipv  7441  addclpr  7469  nqprxx  7478  prmuloc  7498  mulclpr  7504  distrlem1prl  7514  distrlem1pru  7515  ltexprlempr  7540  ltexprlemrl  7542  ltexprlemru  7544  lteupri  7549  recexprlempr  7564  cauappcvgprlemm  7577  cauappcvgprlemopl  7578  cauappcvgprlemlol  7579  cauappcvgprlemopu  7580  cauappcvgprlemupu  7581  cauappcvgprlemloc  7584  cauappcvgprlemcl  7585  cauappcvgprlemladdfu  7586  cauappcvgprlemladdfl  7587  cauappcvgprlem2  7592  caucvgprlemm  7600  caucvgprlemopl  7601  caucvgprlemlol  7602  caucvgprlemopu  7603  caucvgprlemupu  7604  caucvgprlemloc  7607  caucvgprlemcl  7608  caucvgprlemladdfu  7609  caucvgprlem2  7612  caucvgprprlemml  7626  caucvgprprlemmu  7627  caucvgprprlemopl  7629  caucvgprprlemlol  7630  caucvgprprlemopu  7631  caucvgprprlemupu  7632  caucvgprprlemloc  7635  caucvgprprlemcl  7636  caucvgprprlem2  7642  suplocexprlemex  7654  suplocsrlem  7740  elrealeu  7761  rereceu  7821  axpre-suploclemres  7833  negf1o  8271  receuap  8557  divvalap  8561  cju  8847  nn0ge2m1nn  9165  nnnegz  9185  elnnz  9192  elnn0z  9195  peano2z  9218  nn0n0n1ge2  9252  msqznn  9282  eluzaddi  9483  eluzsubi  9484  uzind4  9517  supinfneg  9524  infsupneg  9525  elnn1uz2  9536  uz2mulcl  9537  divfnzn  9550  nnrp  9590  rpaddcl  9604  rpmulcl  9605  rpdivcl  9606  rpgecl  9609  ge0p1rp  9612  elrpd  9620  ge0addcl  9908  ge0mulcl  9909  ge0xaddcl  9910  icoshftf1o  9918  peano2fzr  9962  uzsubsubfz  9972  fzsplit2  9975  elfznn  9979  fzss1  9988  fzss2  9989  fzp1elp1  10000  elfz1b  10015  elfz0fzfz0  10051  fz0fzelfz0  10052  difelfznle  10060  elfzofz  10087  fzosplitsnm1  10134  ubmelm1fzo  10151  fzofzp1b  10153  fzosplitsn  10158  exbtwnz  10176  flqge0nn0  10218  flqge1nn  10219  zmodcl  10269  modqmuladdnn0  10293  modsumfzodifsn  10321  frec2uzf1od  10331  frec2uzisod  10332  frecuzrdgrrn  10333  frec2uzrdg  10334  frecuzrdgrcl  10335  frecuzrdgtcl  10337  frecuzrdgsuc  10339  frecuzrdgrclt  10340  frecuzrdgfunlem  10344  frecuzrdgtclt  10346  frecuzrdgsuctlem  10348  uzennn  10361  seq3fveq2  10394  monoord  10401  iseqf1olemqcl  10411  iseqf1olemnab  10413  iseqf1olemab  10414  iseqf1olemqf1o  10418  seq3f1olemqsumkj  10423  seq3f1olemqsumk  10424  seq3id2  10434  exp3val  10447  expcl2lemap  10457  expclzaplem  10469  expge0  10481  expge1  10482  zsqcl2  10522  bcval4  10654  bcn1  10660  bccl2  10670  hashennnuni  10681  hashunlem  10706  hashdifpr  10722  zfz1isolem1  10739  seq3coll  10741  shftfn  10752  shftf  10758  recvguniq  10923  resqrexlemdecn  10940  rersqreu  10956  nn0abscl  11013  nnabscl  11028  abs2dif  11034  climuni  11220  2clim  11228  climcn2  11236  summodclem2a  11308  fsum3  11314  fsum3cvg3  11323  fsumcl2lem  11325  fsumadd  11333  fisum0diag2  11374  fsummulc2  11375  fsumge0  11386  geolim2  11439  cvgratnnlemabsle  11454  cvgratz  11459  mertenslemi1  11462  prodmodclem3  11502  prodmodclem2a  11503  fprodeq0  11544  fprodge0  11564  eff2  11607  tanvalap  11635  zdvdsdc  11738  fzo0dvdseq  11780  oexpneg  11799  oddge22np1  11803  evennn02n  11804  evennn2n  11805  nno  11828  divalglemeunn  11843  divalglemex  11844  divalglemeuneg  11845  divalg  11846  zsupcllemstep  11863  zsupcl  11865  divgcdz  11889  bezoutlemmain  11916  bezoutlemmo  11924  bezoutlemeu  11925  bezoutlemle  11926  sqgcd  11947  eucalgval2  11964  eucalglt  11968  lcmcllem  11978  lcmledvds  11981  lcmneg  11985  lcmgcdlem  11988  ncoprmgcdne1b  12000  prmind2  12031  prmdc  12041  sqnprm  12047  isprm6  12056  sqrt2irrlem  12070  pw2dvdseu  12077  sqpweven  12084  2sqpwodd  12085  sqrt2irrap  12089  qgt0numnn  12108  phicl2  12123  hashdvds  12130  crth  12133  phimullem  12134  eulerthlem1  12136  eulerthlemh  12140  eulerthlemth  12141  hashgcdlem  12147  oddprm  12168  pythagtriplem6  12179  pythagtriplem11  12183  pythagtriplem13  12185  pythagtriplem19  12191  pclem0  12195  pcpremul  12202  pceu  12204  pc2dvds  12238  difsqpwdvds  12246  pcadd  12248  oddennn  12262  evenennn  12263  ennnfoneleminc  12281  ennnfonelemf1  12288  ennnfonelemen  12291  exmidunben  12296  ctinf  12300  ctiunctlemfo  12309  nninfdclemlt  12323  nninfdclemf1  12324  tgtopon  12607  distopon  12628  epttop  12631  resttopon  12712  resttopon2  12719  cnco  12762  lmss  12787  txtopon  12803  uptx  12815  txdis1cn  12819  hmeocnv  12848  hmeof1o2  12849  hmeores  12856  hmeoco  12857  idhmeo  12858  txhmeo  12860  txswaphmeo  12862  psmetxrge0  12873  isxmet2d  12889  metres2  12922  xmetresbl  12981  comet  13040  bdxmet  13042  bdmet  13043  tgioo  13087  mulc1cncf  13117  mulcncflem  13131  cnrehmeocntop  13134  cnopnap  13135  dedekindeu  13142  dedekindicclemicc  13151  ivthinclemlm  13153  ivthinclemum  13154  ivthinclemlopn  13155  ivthinclemlr  13156  ivthinclemuopn  13157  ivthinclemur  13158  ivthinclemloc  13160  ivthinc  13162  dvfgg  13198  dvcjbr  13213  dvcj  13214  dvfre  13215  rplogbval  13404  bj-charfundcALT  13526  bj-nnord  13675  bj-inf2vnlem1  13687  pwf1oexmid  13713  nnsf  13719  nninfall  13723  nninfself  13727  exmidsbthrlem  13735  qdencn  13740