Theorem syl3anbrc 1356

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  soisores  7305  limuni3  7826  onfununi  8305  smores2  8318  smoiso  8326  oelimcl  8563  iserd  8698  resixp  8908  undifixp  8909  alephval3  10059  canthwelem  10601  canthwe  10602  r1limwun  10687  wunex2  10689  tskcard  10732  gruina  10769  eluzmn  12839  eluzuzle  12841  uztrn  12850  eluzadd  12861  eluzsub  12862  subeluzsub  12865  nn0pzuz  12899  zsupss  12931  nn0ge2m1nnALT  12936  xov1plusxeqvd  13495  ige2m1fz  13615  0elfz  13622  uzsubfz0  13634  elfzmlbm  13636  difelfzle  13639  difelfznle  13640  fvffz0  13644  elfzod  13661  elfzolt2b  13669  elfzolt3b  13670  elfzouz2  13673  fzossrbm1  13687  elfzo0  13699  eluzgtdifelfzo  13726  elfzodifsumelfzo  13730  fzonn0p1  13741  fzonn0p1p1  13743  fzo0sn0fzo1  13754  ssfzo12bi  13760  fzoopth  13761  ubmelm1fzo  13762  elfzonelfzo  13768  fzosplitprm1  13777  fzostep1  13785  fvinim0ffz  13788  flword2  13816  uzsup  13866  modfzo0difsn  13949  modsumfzodifsn  13950  fsuppmapnn0fiub  13997  suppssfz  14000  1elfz0hash  14396  fzsdom2  14434  ccatdmss  14588  ccatrn  14596  ccat2s1fvw  14645  pfxn0  14693  pfxtrcfv0  14700  pfxtrcfvl  14703  swrdswrd  14711  swrdccatin1  14731  pfxccat3  14740  pfxccat3a  14744  repswswrd  14790  cshwidxmod  14809  cshw1  14828  cshwcsh2id  14834  swrds2  14946  pfx2  14953  2swrd2eqwrdeq  14959  ccat2s1fvwALT  14961  rexuzre  15370  limsupgre  15498  rlimclim1  15562  rlimclim  15563  climrlim2  15564  isercolllem1  15682  isercoll  15685  climcndslem1  15869  fallfacval4  16063  tanhbnd  16183  sinbnd2  16204  cosbnd2  16205  rpnnen2lem12  16247  nn0o  16407  bitsfzolem  16458  bitsfzo  16459  bitsmod  16460  bitsfi  16461  bitsinv1lem  16465  bitsinv1  16466  smueqlem  16514  dvdsnprmd  16714  2mulprm  16717  hashgcdlem  16813  prm23lt5  16840  zgz  16959  gznegcl  16961  gzcjcl  16962  gzaddcl  16963  gzmulcl  16964  vdwlem9  17015  prmgaplem3  17079  prmgaplem4  17080  cshwshashlem2  17122  setsstruct2  17200  ismred  17620  isfuncd  17888  homdmcoa  18090  isdrs2  18328  fpwipodrs  18562  ipodrsima  18563  chnub  18644  chnso  18646  sgrp2rid2ex  18954  subgid  19160  issubg2  19173  subsubg  19181  gaorber  19338  orbsta  19343  pmtrfconj  19496  psgnunilem2  19525  psgnunilem3  19526  psgnunilem4  19527  pgpfi1  19625  subgpgp  19627  pgpssslw  19644  subgslw  19646  sylow2alem2  19648  fislw  19655  sylow3lem3  19659  efgs1  19765  efgsp1  19767  efgsres  19768  efgredleme  19773  efgcpbllemb  19785  lt6abl  19925  telgsumfzs  20019  ablfac1eu  20105  submomnd  20162  isrngd  20209  prdsrngd  20212  ringrng  20321  isringrng  20323  isringd  20327  ringsrg  20333  ring1  20346  prdsringd  20355  subrngid  20585  subrngsubg  20588  issubrng2  20594  subsubrng  20599  subrgsubg  20613  subrgsubrng  20614  sdrgid  20828  cntzsdrg  20838  subdrgint  20839  sdrgint  20840  suborng  20912  islmodd  20920  islssd  20989  islss4  21016  dflidl2rng  21275  rnglidl0  21286  rnglidl1  21289  rnglidlrng  21304  rng2idlsubrng  21322  rhmpreimaidl  21334  gzrngunit  21472  expmhm  21475  zringunit  21505  prmirredlem  21511  znidomb  21600  isphld  21693  ocvocv  21710  ocvlss  21711  frlmlbs  21836  psdmul  22218  gsummoncoe1  22358  mp2pm2mplem4  22856  chfacfisf  22901  chfacfisfcpmat  22902  chfacfscmulfsupp  22906  chfacfpmmulfsupp  22910  chfacfpmmulgsum2  22912  2ndcctbss  23502  finlocfin  23567  dissnlocfin  23576  locfindis  23577  locfincf  23578  isfild  23905  infil  23910  neifil  23927  flimfcls  24073  istgp2  24138  oppgtmd  24144  oppgtgp  24145  distgp  24146  indistgp  24147  efmndtmd  24148  submtmd  24151  subgtgp  24152  symgtgp  24153  qustgplem  24168  prdstmdd  24171  prdstgpd  24172  tlmtgp  24243  isngp4  24659  subgngp  24682  ngptgp  24683  tngngp2  24699  nrgtrg  24737  nrgtdrg  24740  elii2  24985  icopnfcnv  24991  xrhmeo  24995  lebnumii  25015  phtpcer  25044  reparpht  25047  phtpcco2  25048  pcohtpy  25069  pcoass  25073  pcorevlem  25075  isclmi  25126  isncvsngpd  25199  cphsubrglem  25226  cphclm  25238  phclm  25281  tcphcph  25286  clsocv  25299  cphsscph  25300  cmslssbn  25421  pjthlem2  25487  ovolf  25531  iundisj2  25598  vitalilem2  25658  vitali  25662  itg2monolem3  25801  dvfsumlem1  26075  dvfsumlem3  26077  mon1puc1p  26198  uc1pmon1p  26199  mon1pid  26201  ply1remlem  26212  drnguc1p  26221  plyaddlem1  26260  coeidlem  26284  plyn0mulidp  26332  aannenlem2  26380  radcnvcl  26467  pilem2  26502  coseq00topi  26554  coseq0negpitopi  26555  tangtx  26557  tanabsge  26558  cosq14gt0  26562  cosq14ge0  26563  cosq34lt1  26579  cosordlem  26582  cos0pilt1  26584  sinord  26586  resinf1o  26588  tanord1  26589  tanord  26590  efif1olem3  26596  efsubm  26603  relogrn  26613  logimclad  26624  logrnaddcl  26626  logneg  26640  logcj  26658  argregt0  26662  argrege0  26663  argimgt0  26664  argimlt0  26665  logimul  26666  logneg2  26667  logdmnrp  26693  logcnlem4  26697  dvloglem  26700  logf1o2  26702  efopnlem2  26709  cxpsqrtlem  26754  relogbval  26824  nnlogbexp  26833  relogbcxp  26837  relogbcxpb  26839  logbgt0b  26845  asinneg  26938  asinsin  26944  acoscos  26945  acosbnd  26952  atancj  26962  atanlogaddlem  26965  atanlogsublem  26967  atanlogsub  26968  atantan  26975  atanbndlem  26977  atans2  26983  leibpi  26994  scvxcvx  27037  jensenlem2  27039  emcllem7  27053  basellem1  27132  ppisval  27155  chtdif  27209  ppidif  27214  ppiub  27255  chtublem  27262  chtub  27263  lgsdilem2  27384  gausslemma2dlem1a  27416  gausslemma2dlem2  27418  gausslemma2dlem5  27422  gausslemma2dlem6  27423  lgsquadlem1  27431  lgsquadlem2  27432  lgsquadlem3  27433  2lgslem1  27445  2sqlem3  27471  chebbnd1lem1  27520  chebbnd1lem2  27521  chebbnd1lem3  27522  dchrisumlem2  27541  dchrvmasumlem2  27549  dchrvmasumiflem1  27552  dchrisum0flblem2  27560  mulog2sumlem2  27586  logdivbnd  27607  pntpbnd2  27638  pntibndlem1  27640  pntibnd  27644  pntlemc  27646  pntlemg  27649  pntlemq  27652  pntlemf  27656  padicabvf  27682  padicabvcxp  27683  ostth2  27688  noextend  27717  noextendseq  27718  nosupno  27754  noinfno  27769  ttgcontlem1  29041  axpaschlem  29097  nbgr2vtx1edg  29507  nbuhgr2vtx1edgb  29509  cusgrexi  29600  structtocusgr  29603  pthdadjvtx  29884  pthdlem1  29922  pthd  29925  crctcshwlkn0lem3  29968  crctcshwlkn0lem4  29969  crctcshwlkn0lem5  29970  crctcshwlkn0lem7  29972  wlkiswwlks1  30023  wwlksm1edg  30037  wwlksnred  30048  wwlksnredwwlkn  30051  wwlksnextproplem3  30067  clwlkclwwlklem2fv1  30153  clwlkclwwlklem2fv2  30154  clwlkclwwlklem2a  30156  clwlkclwwlklem2  30158  clwwisshclwwslemlem  30171  clwwisshclwwslem  30172  erclwwlkref  30178  clwwlkel  30204  clwwlkf  30205  wwlksext2clwwlk  30215  wwlksubclwwlk  30216  umgr2cwwkdifex  30223  1pthd  30301  eucrctshift  30401  dlwwlknondlwlknonf1olem1  30522  numclwlk2lem2f  30535  frgrreggt1  30551  grpoinvf  30691  strlem3a  32411  hstrlem3a  32419  iundisj2f  32749  fcoinver  32763  fresf1o  32793  ssnnssfz  32949  bcm1n  32957  iundisj2fi  32959  fsumrp0cl  33159  cycpmco2lem6  33271  fxpsdrg  33315  lmodslmd  33344  fldgensdrg  33461  intlidl  33566  idlinsubrg  33577  rhmimaidl  33578  ssdifidllem  33603  ssmxidllem  33621  dflringlem2  33651  1arithidomlem1  33691  1arithidomlem2  33692  1arithidom  33693  fldextsdrg  33911  fldextrspunlem2  33934  fldextrspundgdvdslem  33937  fldextrspundgdvds  33938  minplyirred  33968  algextdeglem4  33977  algextdeglem8  33981  rtelextdg2lem  33983  constrsdrg  34032  2sqr3minply  34037  cos9thpiminply  34045  locfinreflem  34097  locfinref  34098  xrge0iifcnv  34190  xrge0iifiso  34192  xrge0iifhom  34194  esumc  34308  esumle  34315  esumlef  34319  esumpinfsum  34334  esumpcvgval  34335  fiunelros  34431  voliune  34486  volfiniune  34487  sibfinima  34596  eulerpartlemt  34628  fiblem  34655  fibp1  34658  dstrvprob  34729  ballotlemsel1i  34770  ballotlemfrceq  34786  signstfvc  34828  signstfveq0  34831  bnj944  35193  bnj998  35212  bnj1136  35252  bnj1408  35291  erdszelem4  35504  erdszelem8  35508  txsconnlem  35550  cvxsconn  35553  cvmliftpht  35628  snmlff  35639  elmrsubrn  35830  msrf  35852  mthmpps  35892  sinccvglem  35982  trer  36636  poimirlem6  38085  poimirlem7  38086  poimirlem9  38088  poimirlem17  38096  poimirlem20  38099  poimirlem28  38107  poimirlem29  38108  poimirlem30  38109  poimirlem31  38110  poimirlem32  38111  areacirc  38172  nnubfi  38209  prter1  39463  lkrlss  39679  diaf11N  41633  dibf11N  41745  lclkr  42117  lclkrs  42123  lcfrlem9  42134  lcfr  42169  mapd1o  42232  hdmapf1oN  42449  hgmapf1oN  42487  frlmvscadiccat  43088  fimgmcyc  43112  nacsfix  43253  eldioph2lem1  43301  irrapxlem1  43359  rmxypairf1o  43448  jm2.27a  43542  hbtlem2  43661  hbt  43667  mon1psubm  43736  onnoxpg  43965  pren2d  44092  binomcxplemnotnn0  44892  elixpconstg  45627  elfzfzo  45816  monoords  45836  eluzd  45943  fmul01lt1lem2  46121  sumnnodd  46166  ioodvbdlimc1lem2  46466  ioodvbdlimc2lem  46468  iblsplit  46500  iblspltprt  46507  itgspltprt  46513  stoweidlem11  46545  stoweidlem17  46551  fourierdlem12  46653  fourierdlem20  46661  fourierdlem25  46666  fourierdlem37  46678  fourierdlem41  46682  fourierdlem48  46688  fourierdlem50  46690  fourierdlem54  46694  fourierdlem64  46704  fourierdlem73  46713  fourierdlem79  46719  fourierdlem102  46742  fourierdlem111  46751  fourierdlem114  46754  etransclem23  46791  etransclem48  46816  ormkglobd  47411  chnsubseq  47416  2elfz2melfz  47872  elfzlble  47874  ceilhalfelfzo1  47888  1elfzo1ceilhalf1  47895  difltmodne  47902  modm2nep1  47926  modm1nep2  47928  modm1p1ne  47930  iccpartiltu  47988  iccpartigtl  47989  iccpartlt  47990  iccpartgt  47993  lswn0  48010  fmtnoge3  48099  fmtnodvds  48113  odz2prm2pw  48132  fmtnole4prm  48147  lighneallem4b  48178  nprmdvdsfacm1lem3  48191  nprmdvdsfacm1lem4  48192  nprmdvdsfacm1  48193  mogoldbb  48367  nnsum4primesevenALTV  48383  bgoldbtbndlem3  48389  gpgprismgriedgdmss  48634  gpgprismgrusgra  48640  gpg3nbgrvtx0  48658  gpg3nbgrvtx0ALT  48659  gpg5nbgrvtx03star  48662  gpg5nbgr3star  48663  gpg3kgrtriexlem3  48667  gpg3kgrtriexlem4  48668  gpg3kgrtriexlem6  48670  gpgprismgr4cycllem3  48679  gpgprismgr4cycllem9  48685  ssnn0ssfz  48931  lmod1  49074  elfzolborelfzop1  49101  nnolog2flm1  49172  funcf2lem2  49663  isnatd  49804