Theorem syl3anbrc 1181

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

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

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 980

This theorem is referenced by:  smores2  6297  smoiso  6305  iserd  6563  erinxp  6611  resixp  6735  netap  7255  2omotaplemap  7258  prarloc  7504  eluzuzle  9538  uztrn  9546  nn0pzuz  9589  nn0ge2m1nnALT  9620  ige2m1fz  10112  0elfz  10120  uzsubfz0  10131  elfzmlbm  10133  difelfzle  10136  difelfznle  10137  elfzolt2b  10160  elfzolt3b  10161  elfzouz2  10163  fzossrbm1  10175  elfzo0  10184  eluzgtdifelfzo  10199  elfzodifsumelfzo  10203  fzonn0p1  10213  fzonn0p1p1  10215  elfzom1p1elfzo  10216  fzo0sn0fzo1  10223  ssfzo12bi  10227  ubmelm1fzo  10228  elfzonelfzo  10232  fzosplitprm1  10236  fzostep1  10239  fvinim0ffz  10243  flqword2  10291  modfzo0difsn  10397  modsumfzodifsn  10398  uzennn  10438  seq3split  10481  iseqf1olemkle  10486  iseqf1olemklt  10487  iseqf1olemqk  10496  seq3f1olemqsumkj  10500  seq3f1olemqsumk  10501  seq3f1olemqsum  10502  bcval5  10745  1elfz0hash  10788  seq3coll  10824  seq3shft  10849  resqrexlemoverl  11032  fsum3cvg3  11406  fisumrev2  11456  isumshft  11500  cvgratnnlemseq  11536  cvgratnnlemabsle  11537  cvgratnnlemsumlt  11538  cvgratz  11542  sinbnd2  11764  cosbnd2  11765  cos12dec  11777  nn0o  11914  suprzubdc  11955  zsupssdc  11957  uzwodc  12040  dvdsnprmd  12127  eulerthlema  12232  hashgcdlem  12240  prm23lt5  12265  prm23ge5  12266  zgz  12373  gznegcl  12375  gzcjcl  12376  gzaddcl  12377  gzmulcl  12378  nninfdclemcl  12451  nninfdclemp1  12453  nninfdclemlt  12454  unbendc  12457  strleund  12564  subgid  13040  issubg2m  13054  subsubg  13062  isringd  13225  ringsrg  13229  subrgsubg  13353  islmodd  13388  sin0pilem1  14287  sin0pilem2  14288  cosq14gt0  14338  cosq23lt0  14339  coseq0q4123  14340  coseq00topi  14341  coseq0negpitopi  14342  tangtx  14344  cosordlem  14355  cosq34lt1  14356  cos02pilt1  14357  cos0pilt1  14358  rplogbval  14448  lgsdilem2  14522  2sqlem3  14549  cvgcmp2nlemabs  14865  iooref1o  14867  taupi  14906