Theorem syl3anbrc 1339

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

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

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 399  df-3an 1085

This theorem is referenced by:  soisores  7079  limuni3  7566  onfununi  7977  smores2  7990  smoiso  7998  oelimcl  8225  iserd  8314  resixp  8496  undifixp  8497  alephval3  9535  canthwelem  10071  canthwe  10072  r1limwun  10157  wunex2  10159  tskcard  10202  gruina  10239  eluzmn  12249  eluzuzle  12251  uztrn  12260  subeluzsub  12274  nn0pzuz  12304  zsupss  12336  nn0ge2m1nnALT  12341  xov1plusxeqvd  12883  ssfzunsnext  12951  ige2m1fz  12996  0elfz  13003  uzsubfz0  13014  elfzmlbm  13016  difelfzle  13019  difelfznle  13020  fvffz0  13024  elfzolt2b  13048  elfzolt3b  13049  elfzouz2  13051  fzossrbm1  13065  elfzo0  13077  eluzgtdifelfzo  13098  elfzodifsumelfzo  13102  fzonn0p1  13113  fzonn0p1p1  13115  fzo0sn0fzo1  13125  ssfzo12bi  13131  ubmelm1fzo  13132  elfzonelfzo  13138  fzosplitprm1  13146  fzostep1  13152  fvinim0ffz  13155  flword2  13182  uzsup  13230  modfzo0difsn  13310  modsumfzodifsn  13311  fsuppmapnn0fiub  13358  suppssfz  13361  1elfz0hash  13750  fzsdom2  13788  ccatrn  13942  ccat2s1fvw  13997  ccat2s1fvwOLD  13998  pfxn0  14047  pfxtrcfv0  14055  pfxtrcfvl  14058  swrdswrd  14066  swrdccatin1  14086  pfxccat3  14095  pfxccat3a  14099  repswswrd  14145  cshwidxmod  14164  cshw1  14183  cshwcsh2id  14189  swrds2  14301  pfx2  14308  2swrd2eqwrdeq  14314  ccat2s1fvwALT  14317  ccat2s1fvwALTOLD  14318  rexuzre  14711  limsupgre  14837  rlimclim1  14901  rlimclim  14902  climrlim2  14903  isercolllem1  15020  isercoll  15023  climcndslem1  15203  fallfacval4  15396  tanhbnd  15513  sinbnd2  15534  cosbnd2  15535  rpnnen2lem12  15577  nn0o  15733  bitsfzolem  15782  bitsfzo  15783  bitsmod  15784  bitsfi  15785  bitsinv1lem  15789  bitsinv1  15790  smueqlem  15838  dvdsnprmd  16033  2mulprm  16036  hashgcdlem  16124  prm23lt5  16150  zgz  16268  gznegcl  16270  gzcjcl  16271  gzaddcl  16272  gzmulcl  16273  vdwlem9  16324  prmgaplem3  16388  prmgaplem4  16389  cshwshashlem2  16429  setsstruct2  16520  ismred  16872  isfuncd  17134  homdmcoa  17326  isdrs2  17548  fpwipodrs  17773  ipodrsima  17774  sgrp2rid2ex  18091  subgid  18280  issubg2  18293  subsubg  18301  gaorber  18437  orbsta  18442  pmtrfconj  18593  psgnunilem2  18622  psgnunilem3  18623  psgnunilem4  18624  pgpfi1  18719  subgpgp  18721  pgpssslw  18738  subgslw  18740  sylow2alem2  18742  fislw  18749  sylow3lem3  18753  efgs1  18860  efgsp1  18862  efgsres  18863  efgredleme  18868  efgcpbllemb  18880  lt6abl  19014  telgsumfzs  19108  ablfac1eu  19194  isringd  19334  ringsrg  19338  ring1  19351  prdsringd  19361  subrgsubg  19540  sdrgid  19574  cntzsdrg  19580  subdrgint  19581  sdrgint  19582  islmodd  19639  islssd  19706  islss4  19733  gsummoncoe1  20471  gzrngunit  20610  expmhm  20613  zringunit  20634  prmirredlem  20639  znidomb  20707  isphld  20797  ocvocv  20814  ocvlss  20815  frlmlbs  20940  mp2pm2mplem4  21416  chfacfisf  21461  chfacfisfcpmat  21462  chfacfscmulfsupp  21466  chfacfpmmulfsupp  21470  chfacfpmmulgsum2  21472  2ndcctbss  22062  finlocfin  22127  dissnlocfin  22136  locfindis  22137  locfincf  22138  isfild  22465  infil  22470  neifil  22487  flimfcls  22633  istgp2  22698  oppgtmd  22704  oppgtgp  22705  distgp  22706  indistgp  22707  efmndtmd  22708  submtmd  22711  subgtgp  22712  symgtgp  22713  qustgplem  22728  prdstmdd  22731  prdstgpd  22732  tlmtgp  22803  isngp4  23220  subgngp  23243  ngptgp  23244  tngngp2  23260  nrgtrg  23298  nrgtdrg  23301  elii2  23539  icopnfcnv  23545  xrhmeo  23549  lebnumii  23569  phtpcer  23598  reparpht  23601  phtpcco2  23602  pcohtpy  23623  pcoass  23627  pcorevlem  23629  isclmi  23680  isncvsngpd  23753  cphsubrglem  23780  cphclm  23792  phclm  23834  tcphcph  23839  clsocv  23852  cphsscph  23853  cmslssbn  23974  pjthlem2  24040  ovolf  24082  iundisj2  24149  vitalilem2  24209  vitali  24213  itg2monolem3  24352  dvfsumlem1  24622  dvfsumlem3  24624  mon1puc1p  24743  uc1pmon1p  24744  ply1remlem  24755  drnguc1p  24763  plyaddlem1  24802  coeidlem  24826  aannenlem2  24917  radcnvcl  25004  pilem2  25039  coseq00topi  25087  coseq0negpitopi  25088  tangtx  25090  tanabsge  25091  cosq14gt0  25095  cosq14ge0  25096  cosq34lt1  25111  cosordlem  25114  sinord  25117  resinf1o  25119  tanord1  25120  tanord  25121  efif1olem3  25127  efsubm  25134  relogrn  25144  logimclad  25155  logrnaddcl  25157  logneg  25170  logcj  25188  argregt0  25192  argrege0  25193  argimgt0  25194  argimlt0  25195  logimul  25196  logneg2  25197  logdmnrp  25223  logcnlem4  25227  dvloglem  25230  logf1o2  25232  efopnlem2  25239  cxpsqrtlem  25284  relogbval  25349  nnlogbexp  25358  relogbcxp  25362  relogbcxpb  25364  logbgt0b  25370  asinneg  25463  asinsin  25469  acoscos  25470  acosbnd  25477  atancj  25487  atanlogaddlem  25490  atanlogsublem  25492  atanlogsub  25493  atantan  25500  atanbndlem  25502  atans2  25508  leibpi  25519  scvxcvx  25562  jensenlem2  25564  emcllem7  25578  basellem1  25657  ppisval  25680  chtdif  25734  ppidif  25739  ppiub  25779  chtublem  25786  chtub  25787  lgsdilem2  25908  gausslemma2dlem1a  25940  gausslemma2dlem2  25942  gausslemma2dlem5  25946  gausslemma2dlem6  25947  lgsquadlem1  25955  lgsquadlem2  25956  lgsquadlem3  25957  2lgslem1  25969  2sqlem3  25995  chebbnd1lem1  26044  chebbnd1lem2  26045  chebbnd1lem3  26046  dchrisumlem2  26065  dchrvmasumlem2  26073  dchrvmasumiflem1  26076  dchrisum0flblem2  26084  mulog2sumlem2  26110  logdivbnd  26131  pntpbnd2  26162  pntibndlem1  26164  pntibnd  26168  pntlemc  26170  pntlemg  26173  pntlemq  26176  pntlemf  26180  padicabvf  26206  padicabvcxp  26207  ostth2  26212  ttgcontlem1  26670  axpaschlem  26725  nbgr2vtx1edg  27131  nbuhgr2vtx1edgb  27133  cusgrexi  27224  structtocusgr  27227  pthdadjvtx  27510  pthdlem1  27546  pthd  27549  crctcshwlkn0lem3  27589  crctcshwlkn0lem4  27590  crctcshwlkn0lem5  27591  crctcshwlkn0lem7  27593  wlkiswwlks1  27644  wwlksm1edg  27658  wwlksnred  27669  wwlksnredwwlkn  27672  wwlksnextproplem3  27689  clwlkclwwlklem2fv1  27772  clwlkclwwlklem2fv2  27773  clwlkclwwlklem2a  27775  clwlkclwwlklem2  27777  clwwisshclwwslemlem  27790  clwwisshclwwslem  27791  erclwwlkref  27797  clwwlkel  27824  clwwlkf  27825  wwlksext2clwwlk  27835  wwlksubclwwlk  27836  umgr2cwwkdifex  27843  1pthd  27921  eucrctshift  28021  dlwwlknondlwlknonf1olem1  28142  numclwlk2lem2f  28155  frgrreggt1  28171  grpoinvf  28308  strlem3a  30028  hstrlem3a  30036  iundisj2f  30339  fcoinver  30356  fresf1o  30375  ssnnssfz  30509  bcm1n  30517  iundisj2fi  30519  fsumrp0cl  30682  submomnd  30711  cycpmco2lem6  30773  lmodslmd  30832  suborng  30888  ssmxidllem  30978  locfinreflem  31104  locfinref  31105  xrge0iifcnv  31176  xrge0iifiso  31178  xrge0iifhom  31180  esumc  31310  esumle  31317  esumlef  31321  esumpinfsum  31336  esumpcvgval  31337  fiunelros  31433  voliune  31488  volfiniune  31489  sibfinima  31597  eulerpartlemt  31629  fiblem  31656  fibp1  31659  dstrvprob  31729  ballotlemsel1i  31770  ballotlemfrceq  31786  plymulx0  31817  signstfvc  31844  signstfveq0  31847  bnj944  32210  bnj998  32229  bnj1136  32269  bnj1408  32308  erdszelem4  32441  erdszelem8  32445  txsconnlem  32487  cvxsconn  32490  cvmliftpht  32565  snmlff  32576  elmrsubrn  32767  msrf  32789  mthmpps  32829  sinccvglem  32915  noextend  33173  noextendseq  33174  nosupno  33203  trer  33664  poimirlem6  34897  poimirlem7  34898  poimirlem9  34900  poimirlem17  34908  poimirlem20  34911  poimirlem28  34919  poimirlem29  34920  poimirlem30  34921  poimirlem31  34922  poimirlem32  34923  areacirc  34986  nnubfi  35024  prter1  36014  lkrlss  36230  diaf11N  38184  dibf11N  38296  lclkr  38668  lclkrs  38674  lcfrlem9  38685  lcfr  38720  mapd1o  38783  hdmapf1oN  39000  hgmapf1oN  39038  frlmvscadiccat  39143  nacsfix  39307  eldioph2lem1  39355  irrapxlem1  39417  rmxypairf1o  39506  jm2.27a  39600  hbtlem2  39722  hbt  39728  mon1pid  39803  mon1psubm  39804  pren2d  39913  binomcxplemnotnn0  40686  elixpconstg  41353  elfzfzo  41540  monoords  41562  elfzod  41671  eluzd  41680  fmul01lt1lem2  41864  sumnnodd  41909  ioodvbdlimc1lem2  42215  ioodvbdlimc2lem  42217  iblsplit  42249  iblspltprt  42256  itgspltprt  42262  stoweidlem11  42295  stoweidlem17  42301  fourierdlem12  42403  fourierdlem20  42411  fourierdlem25  42416  fourierdlem37  42428  fourierdlem41  42432  fourierdlem48  42438  fourierdlem49  42439  fourierdlem50  42440  fourierdlem54  42444  fourierdlem64  42454  fourierdlem73  42463  fourierdlem79  42469  fourierdlem102  42492  fourierdlem111  42501  fourierdlem114  42504  etransclem23  42541  etransclem48  42566  2elfz2melfz  43517  elfzlble  43519  fzoopth  43526  iccpartiltu  43581  iccpartigtl  43582  iccpartlt  43583  iccpartgt  43586  lswn0  43603  fmtnoge3  43691  fmtnodvds  43705  odz2prm2pw  43724  fmtnole4prm  43739  lighneallem4b  43773  mogoldbb  43949  nnsum4primesevenALTV  43965  bgoldbtbndlem3  43971  ringrng  44149  isringrng  44151  lidlrng  44197  ssnn0ssfz  44396  lmod1  44546  elfzolborelfzop1  44573  nnolog2flm1  44649