Theorem syl3anbrc 1208

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

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

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 1007

This theorem is referenced by:  smores2  6538  smoiso  6546  iserd  6806  erinxp  6856  resixp  6981  netap  7584  2omotaplemap  7587  prarloc  7834  eluzmn  9881  eluzuzle  9883  uztrn  9892  nn0pzuz  9940  nn0ge2m1nnALT  9971  ige2m1fz  10469  0elfz  10477  uzsubfz0  10488  elfzmlbm  10490  difelfzle  10493  difelfznle  10494  elfzolt2b  10518  elfzolt3b  10519  elfzouz2  10521  fzossrbm1  10534  elfzo0  10545  eluzgtdifelfzo  10567  elfzodifsumelfzo  10571  fzonn0p1  10581  fzonn0p1p1  10583  elfzom1p1elfzo  10584  fzo0sn0fzo1  10591  ssfzo12bi  10595  ubmelm1fzo  10596  elfzonelfzo  10600  fzosplitprm1  10605  fzostep1  10608  fvinim0ffz  10612  suprzubdc  10623  zsupssdc  10625  flqword2  10676  modfzo0difsn  10784  modsumfzodifsn  10785  uzennn  10825  seq3split  10877  iseqf1olemkle  10886  iseqf1olemklt  10887  iseqf1olemqk  10896  seq3f1olemqsumkj  10900  seq3f1olemqsumk  10901  seq3f1olemqsum  10902  bcval5  11153  bcm1n  11159  1elfz0hash  11199  seq3coll  11242  ccatrn  11325  ccat2s1fvwd  11363  pfxn0  11408  pfxtrcfv0  11414  pfxtrcfvl  11417  swrdswrd  11425  swrdccatin1  11445  pfxccat3  11454  pfxccat3a  11458  cats1fvd  11486  seq3shft  11551  resqrexlemoverl  11734  fsum3cvg3  12110  fisumrev2  12160  isumshft  12204  cvgratnnlemseq  12240  cvgratnnlemabsle  12241  cvgratnnlemsumlt  12242  cvgratz  12246  sinbnd2  12468  cosbnd2  12469  sinltxirr  12475  cos12dec  12482  nn0o  12621  bitsfzolem  12668  bitsfzo  12669  bitsmod  12670  bitsfi  12671  bitsinv1lem  12675  bitsinv1  12676  uzwodc  12761  dvdsnprmd  12850  eulerthlema  12955  hashgcdlem  12963  prm23lt5  12989  prm23ge5  12990  zgz  13099  gznegcl  13101  gzcjcl  13102  gzaddcl  13103  gzmulcl  13104  ballotfilemsel1i  13203  ballotfilemro  13213  ballotfilemfrceq  13219  nninfdclemcl  13286  nninfdclemp1  13288  nninfdclemlt  13289  unbendc  13292  strleund  13403  gsumfzz  13753  gsumfzcl  13757  subgid  13931  issubg2m  13945  subsubg  13953  gsumfzreidx  14093  gsumfzsubmcl  14094  gsumfzmptfidmadd  14095  gsumfzmhm  14099  gsumsplit0  14102  gsumshift  14108  gsumgfsum  14109  isrngd  14195  ringrng  14282  isringd  14287  ringsrg  14293  subrngid  14450  subrngsubg  14453  issubrng2  14459  subsubrng  14463  subrgsubg  14476  islmodd  14570  dflidl2rng  14758  rnglidlrng  14775  rng2idlsubrng  14794  gsumfzfsum  14865  znidomb  14935  plyaddlem1  15741  sin0pilem1  15775  sin0pilem2  15776  cosq14gt0  15826  cosq23lt0  15827  coseq0q4123  15828  coseq00topi  15829  coseq0negpitopi  15830  tangtx  15832  cosordlem  15843  cosq34lt1  15844  cos02pilt1  15845  cos0pilt1  15846  rplogbval  15939  lgsdilem2  16038  gausslemma2dlem1a  16060  gausslemma2dlem2  16064  gausslemma2dlem5  16068  gausslemma2dlem6  16069  lgsquadlem1  16079  lgsquadlem2  16080  lgsquadlem3  16081  2lgslem1  16093  2sqlem3  16119  umgr2cwwkdifex  16549  trlsegvdeglem6  16589  depindlem2  16631  nnnninfen  16938  repiecelem  16948  repiecele0  16949  repiecege0  16950  cvgcmp2nlemabs  16955  iooref1o  16957  taupi  16998