Theorem syl3anbrc 1362

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 1146	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3anbrc.4	. 2 ⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
6	4, 5	sylibr 237	1 ⊢ (𝜑 → 𝜏)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7361  mpt3fvotd  7716  limuni3  7890  onfununi  8380  smores2  8393  smoiso  8401  oelimcl  8640  iserd  8775  resixp  8992  undifixp  8993  alephval3  10219  canthwelem  10765  canthwe  10766  r1limwun  10851  wunex2  10853  tskcard  10896  gruina  10933  eluzmn  13002  eluzuzle  13004  uztrn  13013  eluzadd  13024  eluzsub  13025  subeluzsub  13028  nn0pzuz  13062  zsupss  13094  nn0ge2m1nnALT  13099  xov1plusxeqvd  13659  ige2m1fz  13781  0elfz  13788  uzsubfz0  13800  elfzmlbm  13802  difelfzle  13805  difelfznle  13806  fvffz0  13810  elfzod  13827  elfzolt2b  13835  elfzolt3b  13836  elfzouz2  13839  fzossrbm1  13853  elfzo0  13865  eluzgtdifelfzo  13892  elfzodifsumelfzo  13896  fzonn0p1  13907  fzonn0p1p1  13909  fzo0sn0fzo1  13920  ssfzo12bi  13926  fzoopth  13927  ubmelm1fzo  13928  elfzonelfzo  13934  fzosplitprm1  13943  fzostep1  13951  fvinim0ffz  13954  flword2  13983  uzsup  14033  modfzo0difsn  14116  modsumfzodifsn  14117  fsuppmapnn0fiub  14164  suppssfz  14167  1elfz0hash  14564  fzsdom2  14603  ccatdmss  14757  ccatrn  14765  ccat2s1fvw  14817  pfxn0  14867  pfxtrcfv0  14874  pfxtrcfvl  14877  swrdswrd  14885  swrdccatin1  14905  pfxccat3  14914  pfxccat3a  14918  repswswrd  14966  cshwidxmod  14985  cshw1  15004  cshwcsh2id  15010  swrds2  15123  pfx2  15130  2swrd2eqwrdeq  15138  ccat2s1fvwALT  15140  rexuzre  15552  limsupgre  15680  rlimclim1  15744  rlimclim  15745  climrlim2  15746  isercolllem1  15864  isercoll  15867  climcndslem1  16050  fallfacval4  16241  tanhbnd  16361  sinbnd2  16382  cosbnd2  16383  rpnnen2lem12  16425  nn0o  16585  bitsfzolem  16636  bitsfzo  16637  bitsmod  16638  bitsfi  16639  bitsinv1lem  16643  bitsinv1  16644  smueqlem  16692  dvdsnprmd  16897  2mulprm  16900  hashgcdlem  16997  prm23lt5  17024  zgz  17143  gznegcl  17145  gzcjcl  17146  gzaddcl  17147  gzmulcl  17148  vdwlem9  17199  prmgaplem3  17263  prmgaplem4  17264  cshwshashlem2  17306  setsstruct2  17384  ismred  17804  isfuncd  18072  homdmcoa  18274  isdrs2  18512  fpwipodrs  18746  ipodrsima  18747  chnub  18828  chnso  18830  sgrp2rid2ex  19158  subgid  19370  issubg2  19384  subsubg  19392  gaorber  19555  orbsta  19560  pmtrfconj  19713  psgnunilem2  19742  psgnunilem3  19743  psgnunilem4  19744  pgpfi1  19842  subgpgp  19844  pgpssslw  19861  subgslw  19863  sylow2alem2  19865  fislw  19872  sylow3lem3  19876  efgs1  19982  efgsp1  19984  efgsres  19985  efgredleme  19990  efgcpbllemb  20002  lt6abl  20142  telgsumfzs  20236  ablfac1eu  20322  submomnd  20379  isrngd  20428  prdsrngd  20431  ringrng  20547  isringrng  20549  isringd  20555  ringsrg  20561  ring1  20574  prdsringd  20583  subrngid  20834  subrngsubg  20837  issubrng2  20843  subsubrng  20848  subrgsubg  20862  subrgsubrng  20863  sdrgid  21082  cntzsdrg  21092  subdrgint  21093  sdrgint  21094  suborng  21166  islmodd  21174  islssd  21243  islss4  21270  dflidl2rng  21530  rnglidl0  21542  rnglidl1  21545  unichnlidl  21549  rnglidlrng  21568  rng2idlsubrng  21592  rhmpreimaidl  21604  ssdifidllem  21673  gzrngunit  21772  expmhm  21775  zringunit  21805  prmirredlem  21811  znidomb  21900  isphld  21993  ocvocv  22010  ocvlss  22011  frlmlbs  22136  psdmul  22520  gsummoncoe1  22659  mp2pm2mplem4  23160  chfacfisf  23205  chfacfisfcpmat  23206  chfacfscmulfsupp  23210  chfacfpmmulfsupp  23214  chfacfpmmulgsum2  23216  2ndcctbss  23807  finlocfin  23872  dissnlocfin  23881  locfindis  23882  locfincf  23883  isfild  24210  infil  24215  neifil  24232  flimfcls  24378  istgp2  24443  oppgtmd  24449  oppgtgp  24450  distgp  24451  indistgp  24452  efmndtmd  24453  submtmd  24456  subgtgp  24457  symgtgp  24458  qustgplem  24473  prdstmdd  24476  prdstgpd  24477  tlmtgp  24548  isngp4  24964  subgngp  24987  ngptgp  24988  tngngp2  25004  nrgtrg  25042  nrgtdrg  25045  elii2  25290  icopnfcnv  25296  xrhmeo  25300  lebnumii  25320  phtpcer  25349  reparpht  25352  phtpcco2  25353  pcohtpy  25374  pcoass  25378  pcorevlem  25380  isclmi  25431  isncvsngpd  25504  cphsubrglem  25531  cphclm  25543  phclm  25586  tcphcph  25591  clsocv  25604  cphsscph  25605  cmslssbn  25726  pjthlem2  25792  ovolf  25836  iundisj2  25903  vitalilem2  25963  vitali  25967  itg2monolem3  26106  dvfsumlem1  26379  dvfsumlem3  26381  mon1puc1p  26502  uc1pmon1p  26503  mon1pid  26505  ply1remlem  26516  drnguc1p  26525  plyaddlem1  26565  coeidlem  26589  plyn0mulidp  26635  aannenlem2  26689  radcnvcl  26777  pilem2  26812  coseq00topi  26864  coseq0negpitopi  26865  tangtx  26867  tanabsge  26868  cosq14gt0  26872  cosq14ge0  26873  cosq34lt1  26888  cosordlem  26891  cos0pilt1  26893  sinord  26895  resinf1o  26897  tanord1  26898  tanord  26899  efif1olem3  26905  efsubm  26912  relogrn  26922  logimclad  26933  logrnaddcl  26935  logneg  26949  logcj  26967  argregt0  26971  argrege0  26972  argimgt0  26973  argimlt0  26974  logimul  26975  logneg2  26976  logdmnrp  27002  logcnlem4  27006  dvloglem  27009  logf1o2  27011  efopnlem2  27018  cxpsqrtlem  27063  relogbval  27133  nnlogbexp  27142  relogbcxp  27146  relogbcxpb  27148  logbgt0b  27154  asinneg  27247  asinsin  27253  acoscos  27254  acosbnd  27261  atancj  27271  atanlogaddlem  27274  atanlogsublem  27276  atanlogsub  27277  atantan  27284  atanbndlem  27286  atans2  27292  leibpi  27303  scvxcvx  27346  jensenlem2  27348  emcllem7  27362  basellem1  27441  ppisval  27464  chtdif  27518  ppidif  27523  ppiub  27564  chtublem  27571  chtub  27572  lgsdilem2  27693  gausslemma2dlem1a  27725  gausslemma2dlem2  27727  gausslemma2dlem5  27731  gausslemma2dlem6  27732  lgsquadlem1  27740  lgsquadlem2  27741  lgsquadlem3  27742  2lgslem1  27754  2sqlem3  27780  chebbnd1lem1  27829  chebbnd1lem2  27830  chebbnd1lem3  27831  dchrisumlem2  27850  dchrvmasumlem2  27858  dchrvmasumiflem1  27861  dchrisum0flblem2  27869  mulog2sumlem2  27895  logdivbnd  27916  pntpbnd2  27947  pntibndlem1  27949  pntibnd  27953  pntlemc  27955  pntlemg  27958  pntlemq  27961  pntlemf  27965  padicabvf  27991  padicabvcxp  27992  ostth2  27997  fltoprmlem2  28027  noextend  28056  noextendseq  28057  nosupno  28093  noinfno  28108  ttgcontlem1  29495  axpaschlem  29551  nbgr2vtx1edg  29964  nbuhgr2vtx1edgb  29966  cusgrexi  30057  structtocusgr  30060  pthdadjvtx  30346  pthdlem1  30385  pthd  30388  crctcshwlkn0lem3  30434  crctcshwlkn0lem4  30435  crctcshwlkn0lem5  30436  crctcshwlkn0lem7  30438  wlkiswwlks1  30489  wwlksm1edg  30503  wwlksnred  30514  wwlksnredwwlkn  30517  wwlksnextproplem3  30533  clwlkclwwlklem2fv1  30619  clwlkclwwlklem2fv2  30620  clwlkclwwlklem2a  30622  clwlkclwwlklem2  30624  clwwisshclwwslemlem  30637  clwwisshclwwslem  30638  erclwwlkref  30644  clwwlkel  30670  clwwlkf  30671  wwlksext2clwwlk  30681  wwlksubclwwlk  30682  umgr2cwwkdifex  30689  1pthd  30767  eucrctshift  30877  dlwwlknondlwlknonf1olem1  30998  numclwlk2lem2f  31011  frgrreggt1  31027  grpoinvf  31167  strlem3a  32887  hstrlem3a  32895  iundisj2f  33259  fcoinver  33273  fresf1o  33300  ssnnssfz  33452  bcm1n  33460  iundisj2fi  33462  fsumrp0cl  33658  cycpmco2lem6  33768  fxpsdrg  33812  lmodslmd  33841  fldgensdrg  33960  intlidl  34054  idlinsubrg  34065  rhmimaidl  34066  ssmxidllem  34082  dflringlem2  34111  1arithidomlem1  34151  1arithidomlem2  34152  1arithidom  34153  fldextsdrg  34369  fldextrspunlem2  34392  fldextrspundgdvdslem  34395  fldextrspundgdvds  34396  minplyirred  34426  algextdeglem4  34435  algextdeglem8  34439  rtelextdg2lem  34441  constrsdrg  34490  2sqr3minply  34495  cos9thpiminply  34503  locfinreflem  34555  locfinref  34556  xrge0iifcnv  34648  xrge0iifiso  34650  xrge0iifhom  34652  esumc  34766  esumle  34773  esumlef  34777  esumpinfsum  34792  esumpcvgval  34793  fiunelros  34890  voliune  34945  volfiniune  34946  sibfinima  35054  eulerpartlemt  35086  fiblem  35113  fibp1  35116  dstrvprob  35187  ballotlemsel1i  35228  ballotlemfrceq  35244  signstfvc  35286  signstfveq0  35289  bnj944  35651  bnj998  35670  bnj1136  35710  bnj1408  35749  erdszelem4  36139  erdszelem8  36143  txsconnlem  36185  cvxsconn  36188  cvmliftpht  36263  snmlff  36274  elmrsubrn  36465  msrf  36487  mthmpps  36527  sinccvglem  36617  trer  37295  poimirlem6  38749  poimirlem7  38750  poimirlem9  38752  poimirlem17  38760  poimirlem20  38763  poimirlem28  38771  poimirlem29  38772  poimirlem30  38773  poimirlem31  38774  poimirlem32  38775  areacirc  38836  nnubfi  38887  prter1  40139  lkrlss  40355  diaf11N  42309  dibf11N  42421  lclkr  42793  lclkrs  42799  lcfrlem9  42810  lcfr  42845  mapd1o  42908  hdmapf1oN  43125  hgmapf1oN  43163  frlmvscadiccat  43777  fimgmcyc  43802  nacsfix  43927  eldioph2lem1  43975  irrapxlem1  44033  rmxypairf1o  44122  jm2.27a  44216  hbtlem2  44329  hbt  44335  mon1psubm  44404  onnoxpg  44633  pren2d  44760  binomcxplemnotnn0  45543  elixpconstg  46319  elfzfzo  46508  monoords  46528  eluzd  46634  fmul01lt1lem2  46812  sumnnodd  46857  ioodvbdlimc1lem2  47157  ioodvbdlimc2lem  47159  iblsplit  47191  iblspltprt  47198  itgspltprt  47204  stoweidlem11  47236  stoweidlem17  47242  fourierdlem12  47344  fourierdlem20  47352  fourierdlem25  47357  fourierdlem37  47369  fourierdlem41  47373  fourierdlem48  47379  fourierdlem50  47381  fourierdlem54  47385  fourierdlem64  47395  fourierdlem73  47404  fourierdlem79  47410  fourierdlem102  47433  fourierdlem111  47442  fourierdlem114  47445  etransclem23  47482  etransclem48  47507  ormkglobd  48102  chnsubseq  48105  2elfz2melfz  48603  elfzlble  48605  ceilhalfelfzo1  48619  1elfzo1ceilhalf1  48626  difltmodne  48633  modm2nep1  48657  modm1nep2  48659  modm1p1ne  48661  iccpartiltu  48719  iccpartigtl  48720  iccpartlt  48721  iccpartgt  48724  lswn0  48741  fmtnoge3  48830  fmtnodvds  48844  odz2prm2pw  48863  fmtnole4prm  48878  lighneallem4b  48909  nprmdvdsfacm1lem3  48922  nprmdvdsfacm1lem4  48923  nprmdvdsfacm1  48924  mogoldbb  49098  nnsum4primesevenALTV  49114  bgoldbtbndlem3  49120  gpgprismgriedgdmss  49365  gpgprismgrusgra  49371  gpg3nbgrvtx0  49389  gpg3nbgrvtx0ALT  49390  gpg5nbgrvtx03star  49393  gpg5nbgr3star  49394  gpg3kgrtriexlem3  49398  gpg3kgrtriexlem4  49399  gpg3kgrtriexlem6  49401  gpgprismgr4cycllem3  49410  gpgprismgr4cycllem9  49416  ssnn0ssfz  49676  lmod1  49819  elfzolborelfzop1  49846  nnolog2flm1  49917  funcf2lem2  50411  isnatd  50554