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  6361  smoiso  6369  iserd  6627  erinxp  6677  resixp  6801  netap  7339  2omotaplemap  7342  prarloc  7589  eluzuzle  9628  uztrn  9637  nn0pzuz  9680  nn0ge2m1nnALT  9711  ige2m1fz  10204  0elfz  10212  uzsubfz0  10223  elfzmlbm  10225  difelfzle  10228  difelfznle  10229  elfzolt2b  10253  elfzolt3b  10254  elfzouz2  10256  fzossrbm1  10268  elfzo0  10277  eluzgtdifelfzo  10292  elfzodifsumelfzo  10296  fzonn0p1  10306  fzonn0p1p1  10308  elfzom1p1elfzo  10309  fzo0sn0fzo1  10316  ssfzo12bi  10320  ubmelm1fzo  10321  elfzonelfzo  10325  fzosplitprm1  10329  fzostep1  10332  fvinim0ffz  10336  suprzubdc  10345  zsupssdc  10347  flqword2  10398  modfzo0difsn  10506  modsumfzodifsn  10507  uzennn  10547  seq3split  10599  iseqf1olemkle  10608  iseqf1olemklt  10609  iseqf1olemqk  10618  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seq3f1olemqsum  10624  bcval5  10874  1elfz0hash  10917  seq3coll  10953  seq3shft  11022  resqrexlemoverl  11205  fsum3cvg3  11580  fisumrev2  11630  isumshft  11674  cvgratnnlemseq  11710  cvgratnnlemabsle  11711  cvgratnnlemsumlt  11712  cvgratz  11716  sinbnd2  11938  cosbnd2  11939  sinltxirr  11945  cos12dec  11952  nn0o  12091  bitsfzolem  12138  bitsfzo  12139  bitsmod  12140  bitsfi  12141  bitsinv1lem  12145  bitsinv1  12146  uzwodc  12231  dvdsnprmd  12320  eulerthlema  12425  hashgcdlem  12433  prm23lt5  12459  prm23ge5  12460  zgz  12569  gznegcl  12571  gzcjcl  12572  gzaddcl  12573  gzmulcl  12574  nninfdclemcl  12692  nninfdclemp1  12694  nninfdclemlt  12695  unbendc  12698  strleund  12808  gsumfzz  13199  gsumfzcl  13203  subgid  13383  issubg2m  13397  subsubg  13405  gsumfzreidx  13545  gsumfzsubmcl  13546  gsumfzmptfidmadd  13547  gsumfzmhm  13551  isrngd  13587  ringrng  13670  isringd  13675  ringsrg  13681  subrngid  13835  subrngsubg  13838  issubrng2  13844  subsubrng  13848  subrgsubg  13861  islmodd  13927  dflidl2rng  14115  rnglidlrng  14132  rng2idlsubrng  14151  gsumfzfsum  14222  znidomb  14292  plyaddlem1  15091  sin0pilem1  15125  sin0pilem2  15126  cosq14gt0  15176  cosq23lt0  15177  coseq0q4123  15178  coseq00topi  15179  coseq0negpitopi  15180  tangtx  15182  cosordlem  15193  cosq34lt1  15194  cos02pilt1  15195  cos0pilt1  15196  rplogbval  15289  lgsdilem2  15385  gausslemma2dlem1a  15407  gausslemma2dlem2  15411  gausslemma2dlem5  15415  gausslemma2dlem6  15416  lgsquadlem1  15426  lgsquadlem2  15427  lgsquadlem3  15428  2lgslem1  15440  2sqlem3  15466  nnnninfen  15776  cvgcmp2nlemabs  15789  iooref1o  15791  taupi  15830