Theorem syl3anbrc 1208

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

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

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 1007

This theorem is referenced by:  smores2  6524  smoiso  6532  iserd  6792  erinxp  6842  resixp  6967  netap  7564  2omotaplemap  7567  prarloc  7814  eluzmn  9856  eluzuzle  9858  uztrn  9867  nn0pzuz  9915  nn0ge2m1nnALT  9946  ige2m1fz  10440  0elfz  10448  uzsubfz0  10459  elfzmlbm  10461  difelfzle  10464  difelfznle  10465  elfzolt2b  10489  elfzolt3b  10490  elfzouz2  10492  fzossrbm1  10505  elfzo0  10516  eluzgtdifelfzo  10538  elfzodifsumelfzo  10542  fzonn0p1  10552  fzonn0p1p1  10554  elfzom1p1elfzo  10555  fzo0sn0fzo1  10562  ssfzo12bi  10566  ubmelm1fzo  10567  elfzonelfzo  10571  fzosplitprm1  10576  fzostep1  10579  fvinim0ffz  10583  suprzubdc  10592  zsupssdc  10594  flqword2  10645  modfzo0difsn  10753  modsumfzodifsn  10754  uzennn  10794  seq3split  10846  iseqf1olemkle  10855  iseqf1olemklt  10856  iseqf1olemqk  10865  seq3f1olemqsumkj  10869  seq3f1olemqsumk  10870  seq3f1olemqsum  10871  bcval5  11121  1elfz0hash  11166  seq3coll  11207  ccatrn  11290  ccat2s1fvwd  11328  pfxn0  11373  pfxtrcfv0  11379  pfxtrcfvl  11382  swrdswrd  11390  swrdccatin1  11410  pfxccat3  11419  pfxccat3a  11423  cats1fvd  11451  seq3shft  11516  resqrexlemoverl  11699  fsum3cvg3  12075  fisumrev2  12125  isumshft  12169  cvgratnnlemseq  12205  cvgratnnlemabsle  12206  cvgratnnlemsumlt  12207  cvgratz  12211  sinbnd2  12433  cosbnd2  12434  sinltxirr  12440  cos12dec  12447  nn0o  12586  bitsfzolem  12633  bitsfzo  12634  bitsmod  12635  bitsfi  12636  bitsinv1lem  12640  bitsinv1  12641  uzwodc  12726  dvdsnprmd  12815  eulerthlema  12920  hashgcdlem  12928  prm23lt5  12954  prm23ge5  12955  zgz  13064  gznegcl  13066  gzcjcl  13067  gzaddcl  13068  gzmulcl  13069  nninfdclemcl  13188  nninfdclemp1  13190  nninfdclemlt  13191  unbendc  13194  strleund  13305  gsumfzz  13697  gsumfzcl  13701  subgid  13881  issubg2m  13895  subsubg  13903  gsumfzreidx  14043  gsumfzsubmcl  14044  gsumfzmptfidmadd  14045  gsumfzmhm  14049  gsumsplit0  14052  isrngd  14086  ringrng  14169  isringd  14174  ringsrg  14180  subrngid  14335  subrngsubg  14338  issubrng2  14344  subsubrng  14348  subrgsubg  14361  islmodd  14428  dflidl2rng  14616  rnglidlrng  14633  rng2idlsubrng  14652  gsumfzfsum  14723  znidomb  14793  plyaddlem1  15599  sin0pilem1  15633  sin0pilem2  15634  cosq14gt0  15684  cosq23lt0  15685  coseq0q4123  15686  coseq00topi  15687  coseq0negpitopi  15688  tangtx  15690  cosordlem  15701  cosq34lt1  15702  cos02pilt1  15703  cos0pilt1  15704  rplogbval  15797  lgsdilem2  15896  gausslemma2dlem1a  15918  gausslemma2dlem2  15922  gausslemma2dlem5  15926  gausslemma2dlem6  15927  lgsquadlem1  15937  lgsquadlem2  15938  lgsquadlem3  15939  2lgslem1  15951  2sqlem3  15977  umgr2cwwkdifex  16407  trlsegvdeglem6  16447  depindlem2  16489  nnnninfen  16786  repiecelem  16796  repiecele0  16797  repiecege0  16798  cvgcmp2nlemabs  16803  iooref1o  16805  taupi  16845  gsumgfsumlem  16851  gsumgfsum  16852