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:  sb2  1767  sbequ1  1768  sbidm  1851  eqeu  2909  euind  2926  reuind  2944  eldifd  3141  eqssd  3174  ssrabdv  3236  elind  3322  dcun  3535  opm  4236  issod  4321  ordsucim  4501  onintonm  4518  ordtri2or2exmidlem  4527  en2lp  4555  ordwe  4577  sosng  4701  sotri2  5028  sotri3  5029  relssdmrn  5151  funun  5262  fnsng  5265  fnprg  5273  fntpg  5274  fntp  5275  fununi  5286  imain  5300  fnco  5326  f00  5409  f1ss  5429  f1ssr  5430  f1ssres  5432  f1f1orn  5474  foimacnv  5481  foun  5482  fun11iun  5484  sefvex  5538  dff3im  5663  fmpt  5668  ffnfv  5676  fmpt2d  5680  ffvresb  5681  fprg  5701  foco2  5756  fcof1  5786  fcofo  5787  fcof1o  5792  fliftf  5802  isoini2  5822  f1oiso  5829  moriotass  5861  fnoprabg  5978  f1ocnvd  6075  suppssfv  6081  suppssov1  6082  1stcof  6166  2ndcof  6167  1stconst  6224  2ndconst  6225  fo2ndf  6230  f1o2ndf1  6231  f1od2  6238  smores2  6297  tfrlem5  6317  tfrlemibfn  6331  tfr1onlembfn  6347  tfri1dALT  6354  tfrcllembfn  6360  nntri2  6497  eroveu  6628  elixpsn  6737  dom2lem  6774  xpf1o  6846  fidifsnen  6872  finexdc  6904  unfidisj  6923  f1finf1o  6948  fidcenumlemrks  6954  sbthlemi9  6966  supeuti  6995  infeuti  7030  casef1  7091  caseinl  7092  caseinr  7093  difinfsnlem  7100  ctmlemr  7109  ctm  7110  ctssdclemn0  7111  ctssdccl  7112  ctssdc  7114  enumctlemm  7115  nnnninf  7126  nninfwlpoimlemg  7175  en2other2  7197  exmidfodomrlemim  7202  pw1nel3  7232  dftap2  7252  cc2lem  7267  cc4f  7270  addclpi  7328  mulclpi  7329  nnppipi  7344  recmulnqg  7392  enq0ref  7434  nqnq0pi  7439  genipv  7510  addclpr  7538  nqprxx  7547  prmuloc  7567  mulclpr  7573  distrlem1prl  7583  distrlem1pru  7584  ltexprlempr  7609  ltexprlemrl  7611  ltexprlemru  7613  lteupri  7618  recexprlempr  7633  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemopu  7649  cauappcvgprlemupu  7650  cauappcvgprlemloc  7653  cauappcvgprlemcl  7654  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  cauappcvgprlem2  7661  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemopu  7672  caucvgprlemupu  7673  caucvgprlemloc  7676  caucvgprlemcl  7677  caucvgprlemladdfu  7678  caucvgprlem2  7681  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemopu  7700  caucvgprprlemupu  7701  caucvgprprlemloc  7704  caucvgprprlemcl  7705  caucvgprprlem2  7711  suplocexprlemex  7723  suplocsrlem  7809  elrealeu  7830  rereceu  7890  axpre-suploclemres  7902  negf1o  8341  aptap  8609  receuap  8628  divvalap  8633  cju  8920  nn0ge2m1nn  9238  nnnegz  9258  elnnz  9265  elnn0z  9268  peano2z  9291  nn0n0n1ge2  9325  msqznn  9355  eluzaddi  9556  eluzsubi  9557  uzind4  9590  supinfneg  9597  infsupneg  9598  elnn1uz2  9609  uz2mulcl  9610  divfnzn  9623  nnrp  9665  rpaddcl  9679  rpmulcl  9680  rpdivcl  9681  rpgecl  9684  ge0p1rp  9687  elrpd  9695  ge0addcl  9983  ge0mulcl  9984  ge0xaddcl  9985  icoshftf1o  9993  peano2fzr  10039  uzsubsubfz  10049  fzsplit2  10052  elfznn  10056  fzss1  10065  fzss2  10066  fzp1elp1  10077  elfz1b  10092  elfz0fzfz0  10128  fz0fzelfz0  10129  difelfznle  10137  elfzofz  10164  fzosplitsnm1  10211  ubmelm1fzo  10228  fzofzp1b  10230  fzosplitsn  10235  exbtwnz  10253  flqge0nn0  10295  flqge1nn  10296  zmodcl  10346  modqmuladdnn0  10370  modsumfzodifsn  10398  frec2uzf1od  10408  frec2uzisod  10409  frecuzrdgrrn  10410  frec2uzrdg  10411  frecuzrdgrcl  10412  frecuzrdgtcl  10414  frecuzrdgsuc  10416  frecuzrdgrclt  10417  frecuzrdgfunlem  10421  frecuzrdgtclt  10423  frecuzrdgsuctlem  10425  uzennn  10438  seq3fveq2  10471  monoord  10478  iseqf1olemqcl  10488  iseqf1olemnab  10490  iseqf1olemab  10491  iseqf1olemqf1o  10495  seq3f1olemqsumkj  10500  seq3f1olemqsumk  10501  seq3id2  10511  exp3val  10524  expcl2lemap  10534  expclzaplem  10546  expge0  10558  expge1  10559  zsqcl2  10600  bcval4  10734  bcn1  10740  bccl2  10750  hashennnuni  10761  hashunlem  10786  hashdifpr  10802  zfz1isolem1  10822  seq3coll  10824  shftfn  10835  shftf  10841  recvguniq  11006  resqrexlemdecn  11023  rersqreu  11039  nn0abscl  11096  nnabscl  11111  abs2dif  11117  climuni  11303  2clim  11311  climcn2  11319  summodclem2a  11391  fsum3  11397  fsum3cvg3  11406  fsumcl2lem  11408  fsumadd  11416  fisum0diag2  11457  fsummulc2  11458  fsumge0  11469  geolim2  11522  cvgratnnlemabsle  11537  cvgratz  11542  mertenslemi1  11545  prodmodclem3  11585  prodmodclem2a  11586  fprodeq0  11627  fprodge0  11647  eff2  11690  tanvalap  11718  zdvdsdc  11821  fzo0dvdseq  11865  oexpneg  11884  oddge22np1  11888  evennn02n  11889  evennn2n  11890  nno  11913  divalglemeunn  11928  divalglemex  11929  divalglemeuneg  11930  divalg  11931  zsupcllemstep  11948  zsupcl  11950  divgcdz  11974  bezoutlemmain  12001  bezoutlemmo  12009  bezoutlemeu  12010  bezoutlemle  12011  sqgcd  12032  uzwodc  12040  eucalgval2  12055  eucalglt  12059  lcmcllem  12069  lcmledvds  12072  lcmneg  12076  lcmgcdlem  12079  ncoprmgcdne1b  12091  prmind2  12122  prmdc  12132  sqnprm  12138  isprm5lem  12143  isprm5  12144  isprm6  12149  sqrt2irrlem  12163  pw2dvdseu  12170  sqpweven  12177  2sqpwodd  12178  sqrt2irrap  12182  qgt0numnn  12201  phicl2  12216  hashdvds  12223  crth  12226  phimullem  12227  eulerthlem1  12229  eulerthlemh  12233  eulerthlemth  12234  hashgcdlem  12240  oddprm  12261  pythagtriplem6  12272  pythagtriplem11  12276  pythagtriplem13  12278  pythagtriplem19  12284  pclem0  12288  pcpremul  12295  pceu  12297  pc2dvds  12331  difsqpwdvds  12339  pcadd  12341  pockthlem  12356  pockthg  12357  1arith  12367  oddennn  12395  evenennn  12396  ennnfoneleminc  12414  ennnfonelemf1  12421  ennnfonelemen  12424  exmidunben  12429  ctinf  12433  ctiunctlemfo  12442  nninfdclemlt  12454  nninfdclemf1  12455  ptex  12718  imasaddfnlemg  12740  imasaddflemg  12742  mgmsscl  12785  sgrp0  12820  sgrp1  12821  hashfinmndnn  12838  ismndd  12843  mndpfo  12844  mhmf1o  12866  0mhm  12878  mhmco  12879  isgrpd2e  12901  grpinvf1o  12945  grpinvnzcl  12947  dfgrp3m  12974  mhmmnd  12985  ghmgrp  12987  mulgval  12991  mulgfng  12992  subgmulg  13053  issubg4m  13058  isnsg3  13072  nmzsubg  13075  ssnmz  13076  0nsg  13079  nsgid  13080  isabld  13107  srgfcl  13161  srglmhm  13181  srgrmhm  13182  iscrngd  13226  ringsrg  13229  unitabl  13291  ringelnzr  13333  subrgcrng  13351  subrgnzr  13368  lssneln0  13465  tgtopon  13605  distopon  13626  epttop  13629  resttopon  13710  resttopon2  13717  cnco  13760  lmss  13785  txtopon  13801  uptx  13813  txdis1cn  13817  hmeocnv  13846  hmeof1o2  13847  hmeores  13854  hmeoco  13855  idhmeo  13856  txhmeo  13858  txswaphmeo  13860  psmetxrge0  13871  isxmet2d  13887  metres2  13920  xmetresbl  13979  comet  14038  bdxmet  14040  bdmet  14041  tgioo  14085  mulc1cncf  14115  mulcncflem  14129  cnrehmeocntop  14132  cnopnap  14133  dedekindeu  14140  dedekindicclemicc  14149  ivthinclemlm  14151  ivthinclemum  14152  ivthinclemlopn  14153  ivthinclemlr  14154  ivthinclemuopn  14155  ivthinclemur  14156  ivthinclemloc  14158  ivthinc  14160  dvfgg  14196  dvcjbr  14211  dvcj  14212  dvfre  14213  rplogbval  14402  lgsfcl2  14446  lgsval2lem  14450  lgsmod  14466  lgsdirprm  14474  lgsne0  14478  lgseisenlem1  14489  lgseisenlem2  14490  2sqlem8  14509  2sqlem9  14510  bj-charfundcALT  14600  bj-nnord  14749  bj-inf2vnlem1  14761  pwf1oexmid  14788  nnsf  14793  nninfall  14797  nninfself  14801  exmidsbthrlem  14809  qdencn  14814