Theorem syl3anbrc 1207

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

Syntax hints:   → wi 4   ↔ wb 105   ∧ w3a 1004

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  df-3an 1006

This theorem is referenced by:  smores2  6465  smoiso  6473  iserd  6733  erinxp  6783  resixp  6907  netap  7478  2omotaplemap  7481  prarloc  7728  eluzmn  9767  eluzuzle  9769  uztrn  9778  nn0pzuz  9826  nn0ge2m1nnALT  9857  ige2m1fz  10350  0elfz  10358  uzsubfz0  10369  elfzmlbm  10371  difelfzle  10374  difelfznle  10375  elfzolt2b  10399  elfzolt3b  10400  elfzouz2  10402  fzossrbm1  10415  elfzo0  10426  eluzgtdifelfzo  10448  elfzodifsumelfzo  10452  fzonn0p1  10462  fzonn0p1p1  10464  elfzom1p1elfzo  10465  fzo0sn0fzo1  10472  ssfzo12bi  10476  ubmelm1fzo  10477  elfzonelfzo  10481  fzosplitprm1  10486  fzostep1  10489  fvinim0ffz  10493  suprzubdc  10502  zsupssdc  10504  flqword2  10555  modfzo0difsn  10663  modsumfzodifsn  10664  uzennn  10704  seq3split  10756  iseqf1olemkle  10765  iseqf1olemklt  10766  iseqf1olemqk  10775  seq3f1olemqsumkj  10779  seq3f1olemqsumk  10780  seq3f1olemqsum  10781  bcval5  11031  1elfz0hash  11076  seq3coll  11112  ccatrn  11195  ccat2s1fvwd  11233  pfxn0  11278  pfxtrcfv0  11284  pfxtrcfvl  11287  swrdswrd  11295  swrdccatin1  11315  pfxccat3  11324  pfxccat3a  11328  cats1fvd  11356  seq3shft  11421  resqrexlemoverl  11604  fsum3cvg3  11980  fisumrev2  12030  isumshft  12074  cvgratnnlemseq  12110  cvgratnnlemabsle  12111  cvgratnnlemsumlt  12112  cvgratz  12116  sinbnd2  12338  cosbnd2  12339  sinltxirr  12345  cos12dec  12352  nn0o  12491  bitsfzolem  12538  bitsfzo  12539  bitsmod  12540  bitsfi  12541  bitsinv1lem  12545  bitsinv1  12546  uzwodc  12631  dvdsnprmd  12720  eulerthlema  12825  hashgcdlem  12833  prm23lt5  12859  prm23ge5  12860  zgz  12969  gznegcl  12971  gzcjcl  12972  gzaddcl  12973  gzmulcl  12974  nninfdclemcl  13092  nninfdclemp1  13094  nninfdclemlt  13095  unbendc  13098  strleund  13209  gsumfzz  13601  gsumfzcl  13605  subgid  13785  issubg2m  13799  subsubg  13807  gsumfzreidx  13947  gsumfzsubmcl  13948  gsumfzmptfidmadd  13949  gsumfzmhm  13953  gsumsplit0  13956  isrngd  13990  ringrng  14073  isringd  14078  ringsrg  14084  subrngid  14239  subrngsubg  14242  issubrng2  14248  subsubrng  14252  subrgsubg  14265  islmodd  14331  dflidl2rng  14519  rnglidlrng  14536  rng2idlsubrng  14555  gsumfzfsum  14626  znidomb  14696  plyaddlem1  15500  sin0pilem1  15534  sin0pilem2  15535  cosq14gt0  15585  cosq23lt0  15586  coseq0q4123  15587  coseq00topi  15588  coseq0negpitopi  15589  tangtx  15591  cosordlem  15602  cosq34lt1  15603  cos02pilt1  15604  cos0pilt1  15605  rplogbval  15698  lgsdilem2  15794  gausslemma2dlem1a  15816  gausslemma2dlem2  15820  gausslemma2dlem5  15824  gausslemma2dlem6  15825  lgsquadlem1  15835  lgsquadlem2  15836  lgsquadlem3  15837  2lgslem1  15849  2sqlem3  15875  umgr2cwwkdifex  16305  trlsegvdeglem6  16345  depindlem2  16387  nnnninfen  16686  repiecelem  16696  repiecele0  16697  repiecege0  16698  cvgcmp2nlemabs  16703  iooref1o  16705  taupi  16745  gsumgfsumlem  16751  gsumgfsum  16752