Theorem syl3anbrc 1344

Description: Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)

Hypotheses

Ref	Expression
syl3anbrc.1	⊢ (𝜑 → 𝜓)
syl3anbrc.2	⊢ (𝜑 → 𝜒)
syl3anbrc.3	⊢ (𝜑 → 𝜃)
syl3anbrc.4	⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
syl3anbrc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl3anbrc

Step	Hyp	Ref	Expression
1		syl3anbrc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anbrc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anbrc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1128	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3anbrc.4	. 2 ⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
6	4, 5	sylibr 234	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  soisores  7267  limuni3  7788  onfununi  8267  smores2  8280  smoiso  8288  oelimcl  8521  iserd  8654  resixp  8863  undifixp  8864  alephval3  10008  canthwelem  10548  canthwe  10549  r1limwun  10634  wunex2  10636  tskcard  10679  gruina  10716  eluzmn  12745  eluzuzle  12747  uztrn  12756  eluzadd  12767  eluzsub  12768  subeluzsub  12771  nn0pzuz  12805  zsupss  12837  nn0ge2m1nnALT  12842  xov1plusxeqvd  13400  ige2m1fz  13519  0elfz  13526  uzsubfz0  13538  elfzmlbm  13540  difelfzle  13543  difelfznle  13544  fvffz0  13548  elfzolt2b  13572  elfzolt3b  13573  elfzouz2  13576  fzossrbm1  13590  elfzo0  13602  eluzgtdifelfzo  13629  elfzodifsumelfzo  13633  fzonn0p1  13644  fzonn0p1p1  13646  fzo0sn0fzo1  13657  ssfzo12bi  13663  fzoopth  13664  ubmelm1fzo  13665  elfzonelfzo  13671  fzosplitprm1  13680  fzostep1  13688  fvinim0ffz  13691  flword2  13719  uzsup  13769  modfzo0difsn  13852  modsumfzodifsn  13853  fsuppmapnn0fiub  13900  suppssfz  13903  1elfz0hash  14299  fzsdom2  14337  ccatdmss  14491  ccatrn  14499  ccat2s1fvw  14548  pfxn0  14596  pfxtrcfv0  14603  pfxtrcfvl  14606  swrdswrd  14614  swrdccatin1  14634  pfxccat3  14643  pfxccat3a  14647  repswswrd  14693  cshwidxmod  14712  cshw1  14731  cshwcsh2id  14737  swrds2  14849  pfx2  14856  2swrd2eqwrdeq  14862  ccat2s1fvwALT  14864  rexuzre  15262  limsupgre  15390  rlimclim1  15454  rlimclim  15455  climrlim2  15456  isercolllem1  15574  isercoll  15577  climcndslem1  15758  fallfacval4  15952  tanhbnd  16072  sinbnd2  16093  cosbnd2  16094  rpnnen2lem12  16136  nn0o  16296  bitsfzolem  16347  bitsfzo  16348  bitsmod  16349  bitsfi  16350  bitsinv1lem  16354  bitsinv1  16355  smueqlem  16403  dvdsnprmd  16603  2mulprm  16606  hashgcdlem  16701  prm23lt5  16728  zgz  16847  gznegcl  16849  gzcjcl  16850  gzaddcl  16851  gzmulcl  16852  vdwlem9  16903  prmgaplem3  16967  prmgaplem4  16968  cshwshashlem2  17010  setsstruct2  17087  ismred  17506  isfuncd  17774  homdmcoa  17976  isdrs2  18214  fpwipodrs  18448  ipodrsima  18449  chnub  18530  chnso  18532  sgrp2rid2ex  18837  subgid  19043  issubg2  19056  subsubg  19064  gaorber  19222  orbsta  19227  pmtrfconj  19380  psgnunilem2  19409  psgnunilem3  19410  psgnunilem4  19411  pgpfi1  19509  subgpgp  19511  pgpssslw  19528  subgslw  19530  sylow2alem2  19532  fislw  19539  sylow3lem3  19543  efgs1  19649  efgsp1  19651  efgsres  19652  efgredleme  19657  efgcpbllemb  19669  lt6abl  19809  telgsumfzs  19903  ablfac1eu  19989  submomnd  20046  isrngd  20093  prdsrngd  20096  ringrng  20205  isringrng  20207  isringd  20211  ringsrg  20217  ring1  20230  prdsringd  20241  subrngid  20466  subrngsubg  20469  issubrng2  20475  subsubrng  20480  subrgsubg  20494  subrgsubrng  20495  sdrgid  20709  cntzsdrg  20719  subdrgint  20720  sdrgint  20721  suborng  20793  islmodd  20801  islssd  20870  islss4  20897  dflidl2rng  21157  rnglidl0  21168  rnglidl1  21171  rnglidlrng  21186  rng2idlsubrng  21204  rhmpreimaidl  21216  gzrngunit  21372  expmhm  21375  zringunit  21405  prmirredlem  21411  znidomb  21500  isphld  21593  ocvocv  21610  ocvlss  21611  frlmlbs  21736  psdmul  22082  gsummoncoe1  22224  mp2pm2mplem4  22725  chfacfisf  22770  chfacfisfcpmat  22771  chfacfscmulfsupp  22775  chfacfpmmulfsupp  22779  chfacfpmmulgsum2  22781  2ndcctbss  23371  finlocfin  23436  dissnlocfin  23445  locfindis  23446  locfincf  23447  isfild  23774  infil  23779  neifil  23796  flimfcls  23942  istgp2  24007  oppgtmd  24013  oppgtgp  24014  distgp  24015  indistgp  24016  efmndtmd  24017  submtmd  24020  subgtgp  24021  symgtgp  24022  qustgplem  24037  prdstmdd  24040  prdstgpd  24041  tlmtgp  24112  isngp4  24528  subgngp  24551  ngptgp  24552  tngngp2  24568  nrgtrg  24606  nrgtdrg  24609  elii2  24860  icopnfcnv  24868  xrhmeo  24872  lebnumii  24893  phtpcer  24922  reparpht  24926  phtpcco2  24927  pcohtpy  24948  pcoass  24952  pcorevlem  24954  isclmi  25005  isncvsngpd  25078  cphsubrglem  25105  cphclm  25117  phclm  25160  tcphcph  25165  clsocv  25178  cphsscph  25179  cmslssbn  25300  pjthlem2  25366  ovolf  25411  iundisj2  25478  vitalilem2  25538  vitali  25542  itg2monolem3  25681  dvfsumlem1  25960  dvfsumlem3  25963  mon1puc1p  26084  uc1pmon1p  26085  mon1pid  26087  ply1remlem  26098  drnguc1p  26107  plyaddlem1  26146  coeidlem  26170  aannenlem2  26265  radcnvcl  26354  pilem2  26390  coseq00topi  26439  coseq0negpitopi  26440  tangtx  26442  tanabsge  26443  cosq14gt0  26447  cosq14ge0  26448  cosq34lt1  26464  cosordlem  26467  cos0pilt1  26469  sinord  26471  resinf1o  26473  tanord1  26474  tanord  26475  efif1olem3  26481  efsubm  26488  relogrn  26498  logimclad  26509  logrnaddcl  26511  logneg  26525  logcj  26543  argregt0  26547  argrege0  26548  argimgt0  26549  argimlt0  26550  logimul  26551  logneg2  26552  logdmnrp  26578  logcnlem4  26582  dvloglem  26585  logf1o2  26587  efopnlem2  26594  cxpsqrtlem  26639  relogbval  26710  nnlogbexp  26719  relogbcxp  26723  relogbcxpb  26725  logbgt0b  26731  asinneg  26824  asinsin  26830  acoscos  26831  acosbnd  26838  atancj  26848  atanlogaddlem  26851  atanlogsublem  26853  atanlogsub  26854  atantan  26861  atanbndlem  26863  atans2  26869  leibpi  26880  scvxcvx  26924  jensenlem2  26926  emcllem7  26940  basellem1  27019  ppisval  27042  chtdif  27096  ppidif  27101  ppiub  27143  chtublem  27150  chtub  27151  lgsdilem2  27272  gausslemma2dlem1a  27304  gausslemma2dlem2  27306  gausslemma2dlem5  27310  gausslemma2dlem6  27311  lgsquadlem1  27319  lgsquadlem2  27320  lgsquadlem3  27321  2lgslem1  27333  2sqlem3  27359  chebbnd1lem1  27408  chebbnd1lem2  27409  chebbnd1lem3  27410  dchrisumlem2  27429  dchrvmasumlem2  27437  dchrvmasumiflem1  27440  dchrisum0flblem2  27448  mulog2sumlem2  27474  logdivbnd  27495  pntpbnd2  27526  pntibndlem1  27528  pntibnd  27532  pntlemc  27534  pntlemg  27537  pntlemq  27540  pntlemf  27544  padicabvf  27570  padicabvcxp  27571  ostth2  27576  noextend  27606  noextendseq  27607  nosupno  27643  noinfno  27658  ttgcontlem1  28864  axpaschlem  28920  nbgr2vtx1edg  29330  nbuhgr2vtx1edgb  29332  cusgrexi  29423  structtocusgr  29426  pthdadjvtx  29708  pthdlem1  29746  pthd  29749  crctcshwlkn0lem3  29792  crctcshwlkn0lem4  29793  crctcshwlkn0lem5  29794  crctcshwlkn0lem7  29796  wlkiswwlks1  29847  wwlksm1edg  29861  wwlksnred  29872  wwlksnredwwlkn  29875  wwlksnextproplem3  29891  clwlkclwwlklem2fv1  29977  clwlkclwwlklem2fv2  29978  clwlkclwwlklem2a  29980  clwlkclwwlklem2  29982  clwwisshclwwslemlem  29995  clwwisshclwwslem  29996  erclwwlkref  30002  clwwlkel  30028  clwwlkf  30029  wwlksext2clwwlk  30039  wwlksubclwwlk  30040  umgr2cwwkdifex  30047  1pthd  30125  eucrctshift  30225  dlwwlknondlwlknonf1olem1  30346  numclwlk2lem2f  30359  frgrreggt1  30375  grpoinvf  30514  strlem3a  32234  hstrlem3a  32242  iundisj2f  32572  fcoinver  32586  fresf1o  32615  ssnnssfz  32774  bcm1n  32782  iundisj2fi  32784  fsumrp0cl  33009  cycpmco2lem6  33107  fxpsdrg  33151  lmodslmd  33180  fldgensdrg  33287  intlidl  33392  idlinsubrg  33403  rhmimaidl  33404  ssdifidllem  33428  ssmxidllem  33445  1arithidomlem1  33507  1arithidomlem2  33508  1arithidom  33509  fldextsdrg  33688  fldextrspunlem2  33711  fldextrspundgdvdslem  33714  fldextrspundgdvds  33715  minplyirred  33745  algextdeglem4  33754  algextdeglem8  33758  rtelextdg2lem  33760  constrsdrg  33809  2sqr3minply  33814  cos9thpiminply  33822  locfinreflem  33874  locfinref  33875  xrge0iifcnv  33967  xrge0iifiso  33969  xrge0iifhom  33971  esumc  34085  esumle  34092  esumlef  34096  esumpinfsum  34111  esumpcvgval  34112  fiunelros  34208  voliune  34263  volfiniune  34264  sibfinima  34373  eulerpartlemt  34405  fiblem  34432  fibp1  34435  dstrvprob  34506  ballotlemsel1i  34547  ballotlemfrceq  34563  plymulx0  34581  signstfvc  34608  signstfveq0  34611  bnj944  34971  bnj998  34990  bnj1136  35030  bnj1408  35069  erdszelem4  35259  erdszelem8  35263  txsconnlem  35305  cvxsconn  35308  cvmliftpht  35383  snmlff  35394  elmrsubrn  35585  msrf  35607  mthmpps  35647  sinccvglem  35737  trer  36381  poimirlem6  37686  poimirlem7  37687  poimirlem9  37689  poimirlem17  37697  poimirlem20  37700  poimirlem28  37708  poimirlem29  37709  poimirlem30  37710  poimirlem31  37711  poimirlem32  37712  areacirc  37773  nnubfi  37810  prter1  38998  lkrlss  39214  diaf11N  41168  dibf11N  41280  lclkr  41652  lclkrs  41658  lcfrlem9  41669  lcfr  41704  mapd1o  41767  hdmapf1oN  41984  hgmapf1oN  42022  frlmvscadiccat  42624  fimgmcyc  42652  nacsfix  42829  eldioph2lem1  42877  irrapxlem1  42939  rmxypairf1o  43028  jm2.27a  43122  hbtlem2  43241  hbt  43247  mon1psubm  43316  onnog  43546  pren2d  43673  binomcxplemnotnn0  44473  elixpconstg  45210  elfzfzo  45402  monoords  45422  elfzod  45522  eluzd  45531  fmul01lt1lem2  45709  sumnnodd  45754  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  iblsplit  46088  iblspltprt  46095  itgspltprt  46101  stoweidlem11  46133  stoweidlem17  46139  fourierdlem12  46241  fourierdlem20  46249  fourierdlem25  46254  fourierdlem37  46266  fourierdlem41  46270  fourierdlem48  46276  fourierdlem49  46277  fourierdlem50  46278  fourierdlem54  46282  fourierdlem64  46292  fourierdlem73  46301  fourierdlem79  46307  fourierdlem102  46330  fourierdlem111  46339  fourierdlem114  46342  etransclem23  46379  etransclem48  46404  ormkglobd  46997  chnsubseq  47002  2elfz2melfz  47442  elfzlble  47444  ceilhalfelfzo1  47454  1elfzo1ceilhalf1  47461  difltmodne  47466  modm2nep1  47490  modm1nep2  47492  modm1p1ne  47494  iccpartiltu  47546  iccpartigtl  47547  iccpartlt  47548  iccpartgt  47551  lswn0  47568  fmtnoge3  47654  fmtnodvds  47668  odz2prm2pw  47687  fmtnole4prm  47702  lighneallem4b  47733  mogoldbb  47909  nnsum4primesevenALTV  47925  bgoldbtbndlem3  47931  gpgprismgriedgdmss  48176  gpgprismgrusgra  48182  gpg3nbgrvtx0  48200  gpg3nbgrvtx0ALT  48201  gpg5nbgrvtx03star  48204  gpg5nbgr3star  48205  gpg3kgrtriexlem3  48209  gpg3kgrtriexlem4  48210  gpg3kgrtriexlem6  48212  gpgprismgr4cycllem3  48221  gpgprismgr4cycllem9  48227  ssnn0ssfz  48473  lmod1  48617  elfzolborelfzop1  48644  nnolog2flm1  48715  funcf2lem2  49207  isnatd  49348