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  6320  smoiso  6328  iserd  6586  erinxp  6636  resixp  6760  netap  7284  2omotaplemap  7287  prarloc  7533  eluzuzle  9567  uztrn  9576  nn0pzuz  9619  nn0ge2m1nnALT  9650  ige2m1fz  10142  0elfz  10150  uzsubfz0  10161  elfzmlbm  10163  difelfzle  10166  difelfznle  10167  elfzolt2b  10190  elfzolt3b  10191  elfzouz2  10193  fzossrbm1  10205  elfzo0  10214  eluzgtdifelfzo  10229  elfzodifsumelfzo  10233  fzonn0p1  10243  fzonn0p1p1  10245  elfzom1p1elfzo  10246  fzo0sn0fzo1  10253  ssfzo12bi  10257  ubmelm1fzo  10258  elfzonelfzo  10262  fzosplitprm1  10266  fzostep1  10269  fvinim0ffz  10273  flqword2  10322  modfzo0difsn  10428  modsumfzodifsn  10429  uzennn  10469  seq3split  10512  iseqf1olemkle  10517  iseqf1olemklt  10518  iseqf1olemqk  10527  seq3f1olemqsumkj  10531  seq3f1olemqsumk  10532  seq3f1olemqsum  10533  bcval5  10778  1elfz0hash  10821  seq3coll  10857  seq3shft  10882  resqrexlemoverl  11065  fsum3cvg3  11439  fisumrev2  11489  isumshft  11533  cvgratnnlemseq  11569  cvgratnnlemabsle  11570  cvgratnnlemsumlt  11571  cvgratz  11575  sinbnd2  11797  cosbnd2  11798  cos12dec  11810  nn0o  11947  suprzubdc  11988  zsupssdc  11990  uzwodc  12073  dvdsnprmd  12160  eulerthlema  12265  hashgcdlem  12273  prm23lt5  12298  prm23ge5  12299  zgz  12408  gznegcl  12410  gzcjcl  12411  gzaddcl  12412  gzmulcl  12413  nninfdclemcl  12502  nninfdclemp1  12504  nninfdclemlt  12505  unbendc  12508  strleund  12618  subgid  13131  issubg2m  13145  subsubg  13153  isrngd  13324  ringrng  13407  isringd  13412  ringsrg  13416  subrngid  13565  subrngsubg  13568  issubrng2  13574  subsubrng  13578  subrgsubg  13591  islmodd  13626  dflidl2rng  13814  rnglidlrng  13831  rng2idlsubrng  13849  sin0pilem1  14679  sin0pilem2  14680  cosq14gt0  14730  cosq23lt0  14731  coseq0q4123  14732  coseq00topi  14733  coseq0negpitopi  14734  tangtx  14736  cosordlem  14747  cosq34lt1  14748  cos02pilt1  14749  cos0pilt1  14750  rplogbval  14840  lgsdilem2  14915  2sqlem3  14942  cvgcmp2nlemabs  15259  iooref1o  15261  taupi  15300