Theorem syl3anbrc 1184

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

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

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 983

This theorem is referenced by:  smores2  6405  smoiso  6413  iserd  6671  erinxp  6721  resixp  6845  netap  7403  2omotaplemap  7406  prarloc  7653  eluzuzle  9693  uztrn  9702  nn0pzuz  9745  nn0ge2m1nnALT  9776  ige2m1fz  10269  0elfz  10277  uzsubfz0  10288  elfzmlbm  10290  difelfzle  10293  difelfznle  10294  elfzolt2b  10318  elfzolt3b  10319  elfzouz2  10321  fzossrbm1  10334  elfzo0  10345  eluzgtdifelfzo  10365  elfzodifsumelfzo  10369  fzonn0p1  10379  fzonn0p1p1  10381  elfzom1p1elfzo  10382  fzo0sn0fzo1  10389  ssfzo12bi  10393  ubmelm1fzo  10394  elfzonelfzo  10398  fzosplitprm1  10402  fzostep1  10405  fvinim0ffz  10409  suprzubdc  10418  zsupssdc  10420  flqword2  10471  modfzo0difsn  10579  modsumfzodifsn  10580  uzennn  10620  seq3split  10672  iseqf1olemkle  10681  iseqf1olemklt  10682  iseqf1olemqk  10691  seq3f1olemqsumkj  10695  seq3f1olemqsumk  10696  seq3f1olemqsum  10697  bcval5  10947  1elfz0hash  10990  seq3coll  11026  ccatrn  11105  pfxn0  11181  pfxtrcfv0  11187  pfxtrcfvl  11190  swrdswrd  11198  swrdccatin1  11218  pfxccat3  11227  pfxccat3a  11231  cats1fvd  11259  seq3shft  11310  resqrexlemoverl  11493  fsum3cvg3  11868  fisumrev2  11918  isumshft  11962  cvgratnnlemseq  11998  cvgratnnlemabsle  11999  cvgratnnlemsumlt  12000  cvgratz  12004  sinbnd2  12226  cosbnd2  12227  sinltxirr  12233  cos12dec  12240  nn0o  12379  bitsfzolem  12426  bitsfzo  12427  bitsmod  12428  bitsfi  12429  bitsinv1lem  12433  bitsinv1  12434  uzwodc  12519  dvdsnprmd  12608  eulerthlema  12713  hashgcdlem  12721  prm23lt5  12747  prm23ge5  12748  zgz  12857  gznegcl  12859  gzcjcl  12860  gzaddcl  12861  gzmulcl  12862  nninfdclemcl  12980  nninfdclemp1  12982  nninfdclemlt  12983  unbendc  12986  strleund  13096  gsumfzz  13488  gsumfzcl  13492  subgid  13672  issubg2m  13686  subsubg  13694  gsumfzreidx  13834  gsumfzsubmcl  13835  gsumfzmptfidmadd  13836  gsumfzmhm  13840  isrngd  13876  ringrng  13959  isringd  13964  ringsrg  13970  subrngid  14124  subrngsubg  14127  issubrng2  14133  subsubrng  14137  subrgsubg  14150  islmodd  14216  dflidl2rng  14404  rnglidlrng  14421  rng2idlsubrng  14440  gsumfzfsum  14511  znidomb  14581  plyaddlem1  15380  sin0pilem1  15414  sin0pilem2  15415  cosq14gt0  15465  cosq23lt0  15466  coseq0q4123  15467  coseq00topi  15468  coseq0negpitopi  15469  tangtx  15471  cosordlem  15482  cosq34lt1  15483  cos02pilt1  15484  cos0pilt1  15485  rplogbval  15578  lgsdilem2  15674  gausslemma2dlem1a  15696  gausslemma2dlem2  15700  gausslemma2dlem5  15704  gausslemma2dlem6  15705  lgsquadlem1  15715  lgsquadlem2  15716  lgsquadlem3  15717  2lgslem1  15729  2sqlem3  15755  nnnninfen  16268  cvgcmp2nlemabs  16281  iooref1o  16283  taupi  16322