Theorem syl3anbrc 1166

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

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

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 965

This theorem is referenced by:  smores2  6231  smoiso  6239  iserd  6495  erinxp  6543  resixp  6667  prarloc  7402  eluzuzle  9426  uztrn  9434  nn0pzuz  9477  nn0ge2m1nnALT  9505  ige2m1fz  9990  0elfz  9998  uzsubfz0  10006  elfzmlbm  10008  difelfzle  10011  difelfznle  10012  elfzolt2b  10035  elfzolt3b  10036  elfzouz2  10038  fzossrbm1  10050  elfzo0  10059  eluzgtdifelfzo  10074  elfzodifsumelfzo  10078  fzonn0p1  10088  fzonn0p1p1  10090  elfzom1p1elfzo  10091  fzo0sn0fzo1  10098  ssfzo12bi  10102  ubmelm1fzo  10103  elfzonelfzo  10107  fzosplitprm1  10111  fzostep1  10114  fvinim0ffz  10118  flqword2  10166  modfzo0difsn  10272  modsumfzodifsn  10273  uzennn  10313  seq3split  10356  iseqf1olemkle  10361  iseqf1olemklt  10362  iseqf1olemqk  10371  seq3f1olemqsumkj  10375  seq3f1olemqsumk  10376  seq3f1olemqsum  10377  bcval5  10614  1elfz0hash  10657  seq3coll  10690  seq3shft  10715  resqrexlemoverl  10898  fsum3cvg3  11270  fisumrev2  11320  isumshft  11364  cvgratnnlemseq  11400  cvgratnnlemabsle  11401  cvgratnnlemsumlt  11402  cvgratz  11406  sinbnd2  11628  cosbnd2  11629  cos12dec  11641  nn0o  11771  dvdsnprmd  11974  eulerthlema  12074  hashgcdlem  12078  strleund  12225  sin0pilem1  13049  sin0pilem2  13050  cosq14gt0  13100  cosq23lt0  13101  coseq0q4123  13102  coseq00topi  13103  coseq0negpitopi  13104  tangtx  13106  cosordlem  13117  cosq34lt1  13118  cos02pilt1  13119  cos0pilt1  13120  rplogbval  13209  cvgcmp2nlemabs  13552  iooref1o  13554  taupi  13590