Theorem syl3anbrc 1212

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  smores2  6565  smoiso  6573  iserd  6833  erinxp  6883  resixp  7015  netap  7621  2omotaplemap  7624  prarloc  7871  eluzmn  9938  eluzuzle  9940  uztrn  9949  nn0pzuz  9997  nn0ge2m1nnALT  10028  ige2m1fz  10528  0elfz  10536  uzsubfz0  10547  elfzmlbm  10549  difelfzle  10552  difelfznle  10553  elfzolt2b  10577  elfzolt3b  10578  elfzouz2  10580  fzossrbm1  10593  elfzo0  10604  eluzgtdifelfzo  10626  elfzodifsumelfzo  10630  fzonn0p1  10640  fzonn0p1p1  10642  elfzom1p1elfzo  10643  fzo0sn0fzo1  10650  ssfzo12bi  10654  ubmelm1fzo  10655  elfzonelfzo  10659  fzosplitprm1  10664  fzostep1  10667  fvinim0ffz  10671  suprzubdc  10682  zsupssdc  10684  flqword2  10739  modfzo0difsn  10847  modsumfzodifsn  10848  uzennn  10888  seq3split  10940  iseqf1olemkle  10949  iseqf1olemklt  10950  iseqf1olemqk  10959  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  bcval5  11217  bcm1n  11223  1elfz0hash  11263  seq3coll  11310  ccatrn  11393  ccat2s1fvwd  11431  pfxn0  11476  pfxtrcfv0  11482  pfxtrcfvl  11485  swrdswrd  11493  swrdccatin1  11513  pfxccat3  11522  pfxccat3a  11526  cats1fvd  11554  seq3shft  11619  resqrexlemoverl  11803  fsum3cvg3  12182  fisumrev2  12232  isumshft  12276  cvgratnnlemseq  12312  cvgratnnlemabsle  12313  cvgratnnlemsumlt  12314  cvgratz  12318  sinbnd2  12540  cosbnd2  12541  sinltxirr  12547  cos12dec  12554  nn0o  12693  bitsfzolem  12740  bitsfzo  12741  bitsmod  12742  bitsfi  12743  bitsinv1lem  12747  bitsinv1  12748  uzwodc  12833  dvdsnprmd  12922  eulerthlema  13031  hashgcdlem  13039  prm23lt5  13065  prm23ge5  13066  zgz  13175  gznegcl  13177  gzcjcl  13178  gzaddcl  13179  gzmulcl  13180  ballotfilemsel1i  13308  ballotfilemro  13318  ballotfilemfrceq  13324  nninfdclemcl  13391  nninfdclemp1  13393  nninfdclemlt  13394  unbendc  13397  strleund  13510  gzsumcl  13857  subgid  14031  issubg2m  14045  subsubg  14053  gzsumreidx  14225  gzsumsubmcl  14226  gzsummhm  14229  gzsumsplit0  14232  gzsumshift  14233  gzsumgsum  14239  isrngd  14343  ringrng  14432  isringd  14437  ringsrg  14443  subrngid  14600  subrngsubg  14603  issubrng2  14609  subsubrng  14613  subrgsubg  14626  islmodd  14720  dflidl2rng  14909  rnglidlrng  14926  rng2idlsubrng  14945  znidomb  15084  plyaddlem1  15947  sin0pilem1  15982  sin0pilem2  15983  cosq14gt0  16033  cosq23lt0  16034  coseq0q4123  16035  coseq00topi  16036  coseq0negpitopi  16037  tangtx  16039  cosordlem  16051  cosq34lt1  16052  cos02pilt1  16053  cos0pilt1  16054  rplogbval  16155  ppiqsval  16214  chtdif  16238  ppidif  16243  ppiqub  16267  chtublem  16269  chtqub  16270  bposlem4  16288  lgsdilem2  16334  gausslemma2dlem1a  16356  gausslemma2dlem2  16360  gausslemma2dlem5  16364  gausslemma2dlem6  16365  lgsquadlem1  16375  lgsquadlem2  16376  lgsquadlem3  16377  2lgslem1  16389  2sqlem3  16415  umgr2cwwkdifex  16845  trlsegvdeglem6  16885  depindlem2  16927  nnnninfen  17243  repiecelem  17253  repiecele0  17254  repiecege0  17255  cvgcmp2nlemabs  17260  iooref1o  17262  taupi  17303