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  6460  smoiso  6468  iserd  6728  erinxp  6778  resixp  6902  netap  7473  2omotaplemap  7476  prarloc  7723  eluzmn  9762  eluzuzle  9764  uztrn  9773  nn0pzuz  9821  nn0ge2m1nnALT  9852  ige2m1fz  10345  0elfz  10353  uzsubfz0  10364  elfzmlbm  10366  difelfzle  10369  difelfznle  10370  elfzolt2b  10394  elfzolt3b  10395  elfzouz2  10397  fzossrbm1  10410  elfzo0  10421  eluzgtdifelfzo  10443  elfzodifsumelfzo  10447  fzonn0p1  10457  fzonn0p1p1  10459  elfzom1p1elfzo  10460  fzo0sn0fzo1  10467  ssfzo12bi  10471  ubmelm1fzo  10472  elfzonelfzo  10476  fzosplitprm1  10481  fzostep1  10484  fvinim0ffz  10488  suprzubdc  10497  zsupssdc  10499  flqword2  10550  modfzo0difsn  10658  modsumfzodifsn  10659  uzennn  10699  seq3split  10751  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemqk  10770  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  bcval5  11026  1elfz0hash  11071  seq3coll  11107  ccatrn  11187  ccat2s1fvwd  11225  pfxn0  11270  pfxtrcfv0  11276  pfxtrcfvl  11279  swrdswrd  11287  swrdccatin1  11307  pfxccat3  11316  pfxccat3a  11320  cats1fvd  11348  seq3shft  11400  resqrexlemoverl  11583  fsum3cvg3  11959  fisumrev2  12009  isumshft  12053  cvgratnnlemseq  12089  cvgratnnlemabsle  12090  cvgratnnlemsumlt  12091  cvgratz  12095  sinbnd2  12317  cosbnd2  12318  sinltxirr  12324  cos12dec  12331  nn0o  12470  bitsfzolem  12517  bitsfzo  12518  bitsmod  12519  bitsfi  12520  bitsinv1lem  12524  bitsinv1  12525  uzwodc  12610  dvdsnprmd  12699  eulerthlema  12804  hashgcdlem  12812  prm23lt5  12838  prm23ge5  12839  zgz  12948  gznegcl  12950  gzcjcl  12951  gzaddcl  12952  gzmulcl  12953  nninfdclemcl  13071  nninfdclemp1  13073  nninfdclemlt  13074  unbendc  13077  strleund  13188  gsumfzz  13580  gsumfzcl  13584  subgid  13764  issubg2m  13778  subsubg  13786  gsumfzreidx  13926  gsumfzsubmcl  13927  gsumfzmptfidmadd  13928  gsumfzmhm  13932  gsumsplit0  13935  isrngd  13969  ringrng  14052  isringd  14057  ringsrg  14063  subrngid  14218  subrngsubg  14221  issubrng2  14227  subsubrng  14231  subrgsubg  14244  islmodd  14310  dflidl2rng  14498  rnglidlrng  14515  rng2idlsubrng  14534  gsumfzfsum  14605  znidomb  14675  plyaddlem1  15474  sin0pilem1  15508  sin0pilem2  15509  cosq14gt0  15559  cosq23lt0  15560  coseq0q4123  15561  coseq00topi  15562  coseq0negpitopi  15563  tangtx  15565  cosordlem  15576  cosq34lt1  15577  cos02pilt1  15578  cos0pilt1  15579  rplogbval  15672  lgsdilem2  15768  gausslemma2dlem1a  15790  gausslemma2dlem2  15794  gausslemma2dlem5  15798  gausslemma2dlem6  15799  lgsquadlem1  15809  lgsquadlem2  15810  lgsquadlem3  15811  2lgslem1  15823  2sqlem3  15849  umgr2cwwkdifex  16279  trlsegvdeglem6  16319  depindlem2  16347  nnnninfen  16644  cvgcmp2nlemabs  16657  iooref1o  16659  taupi  16698  gsumgfsumlem  16704  gsumgfsum  16705