Theorem sylanbrc 415

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  1760  sbequ1  1761  sbidm  1844  eqeu  2900  euind  2917  reuind  2935  eldifd  3131  eqssd  3164  ssrabdv  3226  elind  3312  dcun  3524  opm  4217  issod  4302  ordsucim  4482  onintonm  4499  ordtri2or2exmidlem  4508  en2lp  4536  ordwe  4558  sosng  4682  sotri2  5006  sotri3  5007  relssdmrn  5129  funun  5240  fnsng  5243  fnprg  5251  fntpg  5252  fntp  5253  fununi  5264  imain  5278  fnco  5304  f00  5387  f1ss  5407  f1ssr  5408  f1ssres  5410  f1f1orn  5451  foimacnv  5458  foun  5459  fun11iun  5461  sefvex  5515  dff3im  5638  fmpt  5643  ffnfv  5651  fmpt2d  5655  ffvresb  5656  fprg  5676  foco2  5730  fcof1  5759  fcofo  5760  fcof1o  5765  fliftf  5775  isoini2  5795  f1oiso  5802  moriotass  5834  fnoprabg  5951  f1ocnvd  6048  suppssfv  6054  suppssov1  6055  1stcof  6139  2ndcof  6140  1stconst  6197  2ndconst  6198  fo2ndf  6203  f1o2ndf1  6204  f1od2  6211  smores2  6270  tfrlem5  6290  tfrlemibfn  6304  tfr1onlembfn  6320  tfri1dALT  6327  tfrcllembfn  6333  nntri2  6470  eroveu  6600  elixpsn  6709  dom2lem  6746  xpf1o  6818  fidifsnen  6844  finexdc  6876  unfidisj  6895  f1finf1o  6920  fidcenumlemrks  6926  sbthlemi9  6938  supeuti  6967  infeuti  7002  casef1  7063  caseinl  7064  caseinr  7065  difinfsnlem  7072  ctmlemr  7081  ctm  7082  ctssdclemn0  7083  ctssdccl  7084  ctssdc  7086  enumctlemm  7087  nnnninf  7098  en2other2  7160  exmidfodomrlemim  7165  pw1nel3  7195  cc2lem  7215  cc4f  7218  addclpi  7276  mulclpi  7277  nnppipi  7292  recmulnqg  7340  enq0ref  7382  nqnq0pi  7387  genipv  7458  addclpr  7486  nqprxx  7495  prmuloc  7515  mulclpr  7521  distrlem1prl  7531  distrlem1pru  7532  ltexprlempr  7557  ltexprlemrl  7559  ltexprlemru  7561  lteupri  7566  recexprlempr  7581  cauappcvgprlemm  7594  cauappcvgprlemopl  7595  cauappcvgprlemlol  7596  cauappcvgprlemopu  7597  cauappcvgprlemupu  7598  cauappcvgprlemloc  7601  cauappcvgprlemcl  7602  cauappcvgprlemladdfu  7603  cauappcvgprlemladdfl  7604  cauappcvgprlem2  7609  caucvgprlemm  7617  caucvgprlemopl  7618  caucvgprlemlol  7619  caucvgprlemopu  7620  caucvgprlemupu  7621  caucvgprlemloc  7624  caucvgprlemcl  7625  caucvgprlemladdfu  7626  caucvgprlem2  7629  caucvgprprlemml  7643  caucvgprprlemmu  7644  caucvgprprlemopl  7646  caucvgprprlemlol  7647  caucvgprprlemopu  7648  caucvgprprlemupu  7649  caucvgprprlemloc  7652  caucvgprprlemcl  7653  caucvgprprlem2  7659  suplocexprlemex  7671  suplocsrlem  7757  elrealeu  7778  rereceu  7838  axpre-suploclemres  7850  negf1o  8288  receuap  8574  divvalap  8578  cju  8864  nn0ge2m1nn  9182  nnnegz  9202  elnnz  9209  elnn0z  9212  peano2z  9235  nn0n0n1ge2  9269  msqznn  9299  eluzaddi  9500  eluzsubi  9501  uzind4  9534  supinfneg  9541  infsupneg  9542  elnn1uz2  9553  uz2mulcl  9554  divfnzn  9567  nnrp  9607  rpaddcl  9621  rpmulcl  9622  rpdivcl  9623  rpgecl  9626  ge0p1rp  9629  elrpd  9637  ge0addcl  9925  ge0mulcl  9926  ge0xaddcl  9927  icoshftf1o  9935  peano2fzr  9980  uzsubsubfz  9990  fzsplit2  9993  elfznn  9997  fzss1  10006  fzss2  10007  fzp1elp1  10018  elfz1b  10033  elfz0fzfz0  10069  fz0fzelfz0  10070  difelfznle  10078  elfzofz  10105  fzosplitsnm1  10152  ubmelm1fzo  10169  fzofzp1b  10171  fzosplitsn  10176  exbtwnz  10194  flqge0nn0  10236  flqge1nn  10237  zmodcl  10287  modqmuladdnn0  10311  modsumfzodifsn  10339  frec2uzf1od  10349  frec2uzisod  10350  frecuzrdgrrn  10351  frec2uzrdg  10352  frecuzrdgrcl  10353  frecuzrdgtcl  10355  frecuzrdgsuc  10357  frecuzrdgrclt  10358  frecuzrdgfunlem  10362  frecuzrdgtclt  10364  frecuzrdgsuctlem  10366  uzennn  10379  seq3fveq2  10412  monoord  10419  iseqf1olemqcl  10429  iseqf1olemnab  10431  iseqf1olemab  10432  iseqf1olemqf1o  10436  seq3f1olemqsumkj  10441  seq3f1olemqsumk  10442  seq3id2  10452  exp3val  10465  expcl2lemap  10475  expclzaplem  10487  expge0  10499  expge1  10500  zsqcl2  10540  bcval4  10673  bcn1  10679  bccl2  10689  hashennnuni  10700  hashunlem  10726  hashdifpr  10742  zfz1isolem1  10762  seq3coll  10764  shftfn  10775  shftf  10781  recvguniq  10946  resqrexlemdecn  10963  rersqreu  10979  nn0abscl  11036  nnabscl  11051  abs2dif  11057  climuni  11243  2clim  11251  climcn2  11259  summodclem2a  11331  fsum3  11337  fsum3cvg3  11346  fsumcl2lem  11348  fsumadd  11356  fisum0diag2  11397  fsummulc2  11398  fsumge0  11409  geolim2  11462  cvgratnnlemabsle  11477  cvgratz  11482  mertenslemi1  11485  prodmodclem3  11525  prodmodclem2a  11526  fprodeq0  11567  fprodge0  11587  eff2  11630  tanvalap  11658  zdvdsdc  11761  fzo0dvdseq  11804  oexpneg  11823  oddge22np1  11827  evennn02n  11828  evennn2n  11829  nno  11852  divalglemeunn  11867  divalglemex  11868  divalglemeuneg  11869  divalg  11870  zsupcllemstep  11887  zsupcl  11889  divgcdz  11913  bezoutlemmain  11940  bezoutlemmo  11948  bezoutlemeu  11949  bezoutlemle  11950  sqgcd  11971  uzwodc  11979  eucalgval2  11994  eucalglt  11998  lcmcllem  12008  lcmledvds  12011  lcmneg  12015  lcmgcdlem  12018  ncoprmgcdne1b  12030  prmind2  12061  prmdc  12071  sqnprm  12077  isprm5lem  12082  isprm5  12083  isprm6  12088  sqrt2irrlem  12102  pw2dvdseu  12109  sqpweven  12116  2sqpwodd  12117  sqrt2irrap  12121  qgt0numnn  12140  phicl2  12155  hashdvds  12162  crth  12165  phimullem  12166  eulerthlem1  12168  eulerthlemh  12172  eulerthlemth  12173  hashgcdlem  12179  oddprm  12200  pythagtriplem6  12211  pythagtriplem11  12215  pythagtriplem13  12217  pythagtriplem19  12223  pclem0  12227  pcpremul  12234  pceu  12236  pc2dvds  12270  difsqpwdvds  12278  pcadd  12280  pockthlem  12295  pockthg  12296  1arith  12306  oddennn  12334  evenennn  12335  ennnfoneleminc  12353  ennnfonelemf1  12360  ennnfonelemen  12363  exmidunben  12368  ctinf  12372  ctiunctlemfo  12381  nninfdclemlt  12393  nninfdclemf1  12394  mgmsscl  12601  sgrp0  12636  sgrp1  12637  hashfinmndnn  12654  ismndd  12659  mndpfo  12660  mhmf1o  12679  0mhm  12690  mhmco  12691  tgtopon  12781  distopon  12802  epttop  12805  resttopon  12886  resttopon2  12893  cnco  12936  lmss  12961  txtopon  12977  uptx  12989  txdis1cn  12993  hmeocnv  13022  hmeof1o2  13023  hmeores  13030  hmeoco  13031  idhmeo  13032  txhmeo  13034  txswaphmeo  13036  psmetxrge0  13047  isxmet2d  13063  metres2  13096  xmetresbl  13155  comet  13214  bdxmet  13216  bdmet  13217  tgioo  13261  mulc1cncf  13291  mulcncflem  13305  cnrehmeocntop  13308  cnopnap  13309  dedekindeu  13316  dedekindicclemicc  13325  ivthinclemlm  13327  ivthinclemum  13328  ivthinclemlopn  13329  ivthinclemlr  13330  ivthinclemuopn  13331  ivthinclemur  13332  ivthinclemloc  13334  ivthinc  13336  dvfgg  13372  dvcjbr  13387  dvcj  13388  dvfre  13389  rplogbval  13578  lgsfcl2  13622  lgsval2lem  13626  lgsmod  13642  lgsdirprm  13650  lgsne0  13654  2sqlem8  13674  2sqlem9  13675  bj-charfundcALT  13766  bj-nnord  13915  bj-inf2vnlem1  13927  pwf1oexmid  13954  nnsf  13960  nninfall  13964  nninfself  13968  exmidsbthrlem  13976  qdencn  13981