Theorem syl3anbrc 1171

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

Syntax hints:   → wi 4   ↔ wb 104   ∧ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  smores2  6258  smoiso  6266  iserd  6523  erinxp  6571  resixp  6695  prarloc  7440  eluzuzle  9470  uztrn  9478  nn0pzuz  9521  nn0ge2m1nnALT  9552  ige2m1fz  10041  0elfz  10049  uzsubfz0  10060  elfzmlbm  10062  difelfzle  10065  difelfznle  10066  elfzolt2b  10089  elfzolt3b  10090  elfzouz2  10092  fzossrbm1  10104  elfzo0  10113  eluzgtdifelfzo  10128  elfzodifsumelfzo  10132  fzonn0p1  10142  fzonn0p1p1  10144  elfzom1p1elfzo  10145  fzo0sn0fzo1  10152  ssfzo12bi  10156  ubmelm1fzo  10157  elfzonelfzo  10161  fzosplitprm1  10165  fzostep1  10168  fvinim0ffz  10172  flqword2  10220  modfzo0difsn  10326  modsumfzodifsn  10327  uzennn  10367  seq3split  10410  iseqf1olemkle  10415  iseqf1olemklt  10416  iseqf1olemqk  10425  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  bcval5  10672  1elfz0hash  10715  seq3coll  10751  seq3shft  10776  resqrexlemoverl  10959  fsum3cvg3  11333  fisumrev2  11383  isumshft  11427  cvgratnnlemseq  11463  cvgratnnlemabsle  11464  cvgratnnlemsumlt  11465  cvgratz  11469  sinbnd2  11691  cosbnd2  11692  cos12dec  11704  nn0o  11840  suprzubdc  11881  zsupssdc  11883  uzwodc  11966  dvdsnprmd  12053  eulerthlema  12158  hashgcdlem  12166  prm23lt5  12191  prm23ge5  12192  zgz  12299  gznegcl  12301  gzcjcl  12302  gzaddcl  12303  gzmulcl  12304  nninfdclemcl  12377  nninfdclemp1  12379  nninfdclemlt  12380  unbendc  12383  strleund  12478  sin0pilem1  13302  sin0pilem2  13303  cosq14gt0  13353  cosq23lt0  13354  coseq0q4123  13355  coseq00topi  13356  coseq0negpitopi  13357  tangtx  13359  cosordlem  13370  cosq34lt1  13371  cos02pilt1  13372  cos0pilt1  13373  rplogbval  13463  lgsdilem2  13537  2sqlem3  13553  cvgcmp2nlemabs  13871  iooref1o  13873  taupi  13909