Theorem syl3anbrc 1184

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

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

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 983

This theorem is referenced by:  smores2  6387  smoiso  6395  iserd  6653  erinxp  6703  resixp  6827  netap  7373  2omotaplemap  7376  prarloc  7623  eluzuzle  9663  uztrn  9672  nn0pzuz  9715  nn0ge2m1nnALT  9746  ige2m1fz  10239  0elfz  10247  uzsubfz0  10258  elfzmlbm  10260  difelfzle  10263  difelfznle  10264  elfzolt2b  10288  elfzolt3b  10289  elfzouz2  10291  fzossrbm1  10304  elfzo0  10313  eluzgtdifelfzo  10333  elfzodifsumelfzo  10337  fzonn0p1  10347  fzonn0p1p1  10349  elfzom1p1elfzo  10350  fzo0sn0fzo1  10357  ssfzo12bi  10361  ubmelm1fzo  10362  elfzonelfzo  10366  fzosplitprm1  10370  fzostep1  10373  fvinim0ffz  10377  suprzubdc  10386  zsupssdc  10388  flqword2  10439  modfzo0difsn  10547  modsumfzodifsn  10548  uzennn  10588  seq3split  10640  iseqf1olemkle  10649  iseqf1olemklt  10650  iseqf1olemqk  10659  seq3f1olemqsumkj  10663  seq3f1olemqsumk  10664  seq3f1olemqsum  10665  bcval5  10915  1elfz0hash  10958  seq3coll  10994  ccatrn  11073  pfxn0  11147  pfxtrcfv0  11153  pfxtrcfvl  11156  swrdswrd  11164  seq3shft  11193  resqrexlemoverl  11376  fsum3cvg3  11751  fisumrev2  11801  isumshft  11845  cvgratnnlemseq  11881  cvgratnnlemabsle  11882  cvgratnnlemsumlt  11883  cvgratz  11887  sinbnd2  12109  cosbnd2  12110  sinltxirr  12116  cos12dec  12123  nn0o  12262  bitsfzolem  12309  bitsfzo  12310  bitsmod  12311  bitsfi  12312  bitsinv1lem  12316  bitsinv1  12317  uzwodc  12402  dvdsnprmd  12491  eulerthlema  12596  hashgcdlem  12604  prm23lt5  12630  prm23ge5  12631  zgz  12740  gznegcl  12742  gzcjcl  12743  gzaddcl  12744  gzmulcl  12745  nninfdclemcl  12863  nninfdclemp1  12865  nninfdclemlt  12866  unbendc  12869  strleund  12979  gsumfzz  13371  gsumfzcl  13375  subgid  13555  issubg2m  13569  subsubg  13577  gsumfzreidx  13717  gsumfzsubmcl  13718  gsumfzmptfidmadd  13719  gsumfzmhm  13723  isrngd  13759  ringrng  13842  isringd  13847  ringsrg  13853  subrngid  14007  subrngsubg  14010  issubrng2  14016  subsubrng  14020  subrgsubg  14033  islmodd  14099  dflidl2rng  14287  rnglidlrng  14304  rng2idlsubrng  14323  gsumfzfsum  14394  znidomb  14464  plyaddlem1  15263  sin0pilem1  15297  sin0pilem2  15298  cosq14gt0  15348  cosq23lt0  15349  coseq0q4123  15350  coseq00topi  15351  coseq0negpitopi  15352  tangtx  15354  cosordlem  15365  cosq34lt1  15366  cos02pilt1  15367  cos0pilt1  15368  rplogbval  15461  lgsdilem2  15557  gausslemma2dlem1a  15579  gausslemma2dlem2  15583  gausslemma2dlem5  15587  gausslemma2dlem6  15588  lgsquadlem1  15598  lgsquadlem2  15599  lgsquadlem3  15600  2lgslem1  15612  2sqlem3  15638  nnnninfen  16032  cvgcmp2nlemabs  16045  iooref1o  16047  taupi  16086