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  6569  smoiso  6577  iserd  6837  erinxp  6887  resixp  7020  netap  7627  2omotaplemap  7630  prarloc  7877  eluzmn  9945  eluzuzle  9947  uztrn  9956  nn0pzuz  10004  nn0ge2m1nnALT  10035  ige2m1fz  10535  0elfz  10543  uzsubfz0  10554  elfzmlbm  10556  difelfzle  10559  difelfznle  10560  elfzolt2b  10584  elfzolt3b  10585  elfzouz2  10587  fzossrbm1  10600  elfzo0  10611  eluzgtdifelfzo  10633  elfzodifsumelfzo  10637  fzonn0p1  10647  fzonn0p1p1  10649  elfzom1p1elfzo  10650  fzo0sn0fzo1  10657  ssfzo12bi  10661  ubmelm1fzo  10662  elfzonelfzo  10666  fzosplitprm1  10671  fzostep1  10674  fvinim0ffz  10678  suprzubdc  10689  zsupssdc  10691  flqword2  10746  modfzo0difsn  10854  modsumfzodifsn  10855  uzennn  10895  seq3split  10947  iseqf1olemkle  10956  iseqf1olemklt  10957  iseqf1olemqk  10966  seq3f1olemqsumkj  10970  seq3f1olemqsumk  10971  seq3f1olemqsum  10972  bcval5  11224  bcm1n  11230  1elfz0hash  11270  seq3coll  11317  ccatrn  11400  ccat2s1fvwd  11438  pfxn0  11483  pfxtrcfv0  11489  pfxtrcfvl  11492  swrdswrd  11500  swrdccatin1  11520  pfxccat3  11529  pfxccat3a  11533  cats1fvd  11561  seq3shft  11626  resqrexlemoverl  11810  fsum3cvg3  12189  fisumrev2  12239  isumshft  12283  cvgratnnlemseq  12319  cvgratnnlemabsle  12320  cvgratnnlemsumlt  12321  cvgratz  12325  sinbnd2  12547  cosbnd2  12548  sinltxirr  12554  cos12dec  12561  nn0o  12700  bitsfzolem  12747  bitsfzo  12748  bitsmod  12749  bitsfi  12750  bitsinv1lem  12754  bitsinv1  12755  uzwodc  12840  dvdsnprmd  12929  eulerthlema  13038  hashgcdlem  13046  prm23lt5  13072  prm23ge5  13073  zgz  13182  gznegcl  13184  gzcjcl  13185  gzaddcl  13186  gzmulcl  13187  ballotfilemsel1i  13315  ballotfilemro  13325  ballotfilemfrceq  13331  nninfdclemcl  13398  nninfdclemp1  13400  nninfdclemlt  13401  unbendc  13404  strleund  13517  gzsumcl  13864  subgid  14038  issubg2m  14052  subsubg  14060  gzsumreidx  14232  gzsumsubmcl  14233  gzsummhm  14236  gzsumsplit0  14239  gzsumshift  14240  gzsumgsum  14246  isrngd  14360  ringrng  14449  isringd  14454  ringsrg  14460  subrngid  14619  subrngsubg  14622  issubrng2  14628  subsubrng  14632  subrgsubg  14645  islmodd  14739  dflidl2rng  14928  rnglidlrng  14945  rng2idlsubrng  14964  znidomb  15103  plyaddlem1  15985  sin0pilem1  16020  sin0pilem2  16021  cosq14gt0  16071  cosq23lt0  16072  coseq0q4123  16073  coseq00topi  16074  coseq0negpitopi  16075  tangtx  16077  cosordlem  16089  cosq34lt1  16090  cos02pilt1  16091  cos0pilt1  16092  rplogbval  16193  ppiqsval  16252  chtdif  16276  ppidif  16281  ppiqub  16305  chtublem  16307  chtqub  16308  bposlem4  16326  lgsdilem2  16372  gausslemma2dlem1a  16394  gausslemma2dlem2  16398  gausslemma2dlem5  16402  gausslemma2dlem6  16403  lgsquadlem1  16413  lgsquadlem2  16414  lgsquadlem3  16415  2lgslem1  16427  2sqlem3  16453  umgr2cwwkdifex  16883  trlsegvdeglem6  16923  depindlem2  16965  nnnninfen  17282  repiecelem  17292  repiecele0  17293  repiecege0  17294  cvgcmp2nlemabs  17299  iooref1o  17301  taupi  17342