Theorem syl3anbrc 1212

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

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

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 1011

This theorem is referenced by:  smores2  6559  smoiso  6567  iserd  6827  erinxp  6877  resixp  7009  netap  7614  2omotaplemap  7617  prarloc  7864  eluzmn  9911  eluzuzle  9913  uztrn  9922  nn0pzuz  9970  nn0ge2m1nnALT  10001  ige2m1fz  10500  0elfz  10508  uzsubfz0  10519  elfzmlbm  10521  difelfzle  10524  difelfznle  10525  elfzolt2b  10549  elfzolt3b  10550  elfzouz2  10552  fzossrbm1  10565  elfzo0  10576  eluzgtdifelfzo  10598  elfzodifsumelfzo  10602  fzonn0p1  10612  fzonn0p1p1  10614  elfzom1p1elfzo  10615  fzo0sn0fzo1  10622  ssfzo12bi  10626  ubmelm1fzo  10627  elfzonelfzo  10631  fzosplitprm1  10636  fzostep1  10639  fvinim0ffz  10643  suprzubdc  10654  zsupssdc  10656  flqword2  10707  modfzo0difsn  10815  modsumfzodifsn  10816  uzennn  10856  seq3split  10908  iseqf1olemkle  10917  iseqf1olemklt  10918  iseqf1olemqk  10927  seq3f1olemqsumkj  10931  seq3f1olemqsumk  10932  seq3f1olemqsum  10933  bcval5  11184  bcm1n  11190  1elfz0hash  11230  seq3coll  11277  ccatrn  11360  ccat2s1fvwd  11398  pfxn0  11443  pfxtrcfv0  11449  pfxtrcfvl  11452  swrdswrd  11460  swrdccatin1  11480  pfxccat3  11489  pfxccat3a  11493  cats1fvd  11521  seq3shft  11586  resqrexlemoverl  11770  fsum3cvg3  12146  fisumrev2  12196  isumshft  12240  cvgratnnlemseq  12276  cvgratnnlemabsle  12277  cvgratnnlemsumlt  12278  cvgratz  12282  sinbnd2  12504  cosbnd2  12505  sinltxirr  12511  cos12dec  12518  nn0o  12657  bitsfzolem  12704  bitsfzo  12705  bitsmod  12706  bitsfi  12707  bitsinv1lem  12711  bitsinv1  12712  uzwodc  12797  dvdsnprmd  12886  eulerthlema  12991  hashgcdlem  12999  prm23lt5  13025  prm23ge5  13026  zgz  13135  gznegcl  13137  gzcjcl  13138  gzaddcl  13139  gzmulcl  13140  ballotfilemsel1i  13239  ballotfilemro  13249  ballotfilemfrceq  13255  nninfdclemcl  13322  nninfdclemp1  13324  nninfdclemlt  13325  unbendc  13328  strleund  13440  gzsumcl  13787  subgid  13961  issubg2m  13975  subsubg  13983  gzsumreidx  14124  gzsumsubmcl  14125  gzsummhm  14128  gzsumsplit0  14131  gzsumshift  14132  gzsumgsum  14138  isrngd  14235  ringrng  14324  isringd  14329  ringsrg  14335  subrngid  14492  subrngsubg  14495  issubrng2  14501  subsubrng  14505  subrgsubg  14518  islmodd  14612  dflidl2rng  14801  rnglidlrng  14818  rng2idlsubrng  14837  znidomb  14976  plyaddlem1  15831  sin0pilem1  15865  sin0pilem2  15866  cosq14gt0  15916  cosq23lt0  15917  coseq0q4123  15918  coseq00topi  15919  coseq0negpitopi  15920  tangtx  15922  cosordlem  15933  cosq34lt1  15934  cos02pilt1  15935  cos0pilt1  15936  rplogbval  16030  lgsdilem2  16138  gausslemma2dlem1a  16160  gausslemma2dlem2  16164  gausslemma2dlem5  16168  gausslemma2dlem6  16169  lgsquadlem1  16179  lgsquadlem2  16180  lgsquadlem3  16181  2lgslem1  16193  2sqlem3  16219  umgr2cwwkdifex  16649  trlsegvdeglem6  16689  depindlem2  16731  nnnninfen  17038  repiecelem  17048  repiecele0  17049  repiecege0  17050  cvgcmp2nlemabs  17055  iooref1o  17057  taupi  17097