Theorem syl3anbrc 1183

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

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

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 982

This theorem is referenced by:  smores2  6347  smoiso  6355  iserd  6613  erinxp  6663  resixp  6787  netap  7314  2omotaplemap  7317  prarloc  7563  eluzuzle  9600  uztrn  9609  nn0pzuz  9652  nn0ge2m1nnALT  9683  ige2m1fz  10176  0elfz  10184  uzsubfz0  10195  elfzmlbm  10197  difelfzle  10200  difelfznle  10201  elfzolt2b  10225  elfzolt3b  10226  elfzouz2  10228  fzossrbm1  10240  elfzo0  10249  eluzgtdifelfzo  10264  elfzodifsumelfzo  10268  fzonn0p1  10278  fzonn0p1p1  10280  elfzom1p1elfzo  10281  fzo0sn0fzo1  10288  ssfzo12bi  10292  ubmelm1fzo  10293  elfzonelfzo  10297  fzosplitprm1  10301  fzostep1  10304  fvinim0ffz  10308  flqword2  10358  modfzo0difsn  10466  modsumfzodifsn  10467  uzennn  10507  seq3split  10559  iseqf1olemkle  10568  iseqf1olemklt  10569  iseqf1olemqk  10578  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  bcval5  10834  1elfz0hash  10877  seq3coll  10913  seq3shft  10982  resqrexlemoverl  11165  fsum3cvg3  11539  fisumrev2  11589  isumshft  11633  cvgratnnlemseq  11669  cvgratnnlemabsle  11670  cvgratnnlemsumlt  11671  cvgratz  11675  sinbnd2  11897  cosbnd2  11898  sinltxirr  11904  cos12dec  11911  nn0o  12048  suprzubdc  12089  zsupssdc  12091  uzwodc  12174  dvdsnprmd  12263  eulerthlema  12368  hashgcdlem  12376  prm23lt5  12401  prm23ge5  12402  zgz  12511  gznegcl  12513  gzcjcl  12514  gzaddcl  12515  gzmulcl  12516  nninfdclemcl  12605  nninfdclemp1  12607  nninfdclemlt  12608  unbendc  12611  strleund  12721  gsumfzz  13067  gsumfzcl  13071  subgid  13245  issubg2m  13259  subsubg  13267  gsumfzreidx  13407  gsumfzsubmcl  13408  gsumfzmptfidmadd  13409  gsumfzmhm  13413  isrngd  13449  ringrng  13532  isringd  13537  ringsrg  13543  subrngid  13697  subrngsubg  13700  issubrng2  13706  subsubrng  13710  subrgsubg  13723  islmodd  13789  dflidl2rng  13977  rnglidlrng  13994  rng2idlsubrng  14013  gsumfzfsum  14076  znidomb  14146  plyaddlem1  14893  sin0pilem1  14916  sin0pilem2  14917  cosq14gt0  14967  cosq23lt0  14968  coseq0q4123  14969  coseq00topi  14970  coseq0negpitopi  14971  tangtx  14973  cosordlem  14984  cosq34lt1  14985  cos02pilt1  14986  cos0pilt1  14987  rplogbval  15077  lgsdilem2  15152  gausslemma2dlem1a  15174  gausslemma2dlem2  15178  gausslemma2dlem5  15182  gausslemma2dlem6  15183  lgsquadlem1  15191  2sqlem3  15204  nnnninfen  15511  cvgcmp2nlemabs  15522  iooref1o  15524  taupi  15563