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  6290  smoiso  6298  iserd  6556  erinxp  6604  resixp  6728  netap  7248  2omotaplemap  7251  prarloc  7497  eluzuzle  9530  uztrn  9538  nn0pzuz  9581  nn0ge2m1nnALT  9612  ige2m1fz  10103  0elfz  10111  uzsubfz0  10122  elfzmlbm  10124  difelfzle  10127  difelfznle  10128  elfzolt2b  10151  elfzolt3b  10152  elfzouz2  10154  fzossrbm1  10166  elfzo0  10175  eluzgtdifelfzo  10190  elfzodifsumelfzo  10194  fzonn0p1  10204  fzonn0p1p1  10206  elfzom1p1elfzo  10207  fzo0sn0fzo1  10214  ssfzo12bi  10218  ubmelm1fzo  10219  elfzonelfzo  10223  fzosplitprm1  10227  fzostep1  10230  fvinim0ffz  10234  flqword2  10282  modfzo0difsn  10388  modsumfzodifsn  10389  uzennn  10429  seq3split  10472  iseqf1olemkle  10477  iseqf1olemklt  10478  iseqf1olemqk  10487  seq3f1olemqsumkj  10491  seq3f1olemqsumk  10492  seq3f1olemqsum  10493  bcval5  10734  1elfz0hash  10777  seq3coll  10813  seq3shft  10838  resqrexlemoverl  11021  fsum3cvg3  11395  fisumrev2  11445  isumshft  11489  cvgratnnlemseq  11525  cvgratnnlemabsle  11526  cvgratnnlemsumlt  11527  cvgratz  11531  sinbnd2  11753  cosbnd2  11754  cos12dec  11766  nn0o  11902  suprzubdc  11943  zsupssdc  11945  uzwodc  12028  dvdsnprmd  12115  eulerthlema  12220  hashgcdlem  12228  prm23lt5  12253  prm23ge5  12254  zgz  12361  gznegcl  12363  gzcjcl  12364  gzaddcl  12365  gzmulcl  12366  nninfdclemcl  12439  nninfdclemp1  12441  nninfdclemlt  12442  unbendc  12445  strleund  12552  subgid  12962  issubg2m  12975  subsubg  12983  isringd  13120  ringsrg  13124  sin0pilem1  13984  sin0pilem2  13985  cosq14gt0  14035  cosq23lt0  14036  coseq0q4123  14037  coseq00topi  14038  coseq0negpitopi  14039  tangtx  14041  cosordlem  14052  cosq34lt1  14053  cos02pilt1  14054  cos0pilt1  14055  rplogbval  14145  lgsdilem2  14219  2sqlem3  14235  cvgcmp2nlemabs  14551  iooref1o  14553  taupi  14591