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  7620  2omotaplemap  7623  prarloc  7870  eluzmn  9930  eluzuzle  9932  uztrn  9941  nn0pzuz  9989  nn0ge2m1nnALT  10020  ige2m1fz  10519  0elfz  10527  uzsubfz0  10538  elfzmlbm  10540  difelfzle  10543  difelfznle  10544  elfzolt2b  10568  elfzolt3b  10569  elfzouz2  10571  fzossrbm1  10584  elfzo0  10595  eluzgtdifelfzo  10617  elfzodifsumelfzo  10621  fzonn0p1  10631  fzonn0p1p1  10633  elfzom1p1elfzo  10634  fzo0sn0fzo1  10641  ssfzo12bi  10645  ubmelm1fzo  10646  elfzonelfzo  10650  fzosplitprm1  10655  fzostep1  10658  fvinim0ffz  10662  suprzubdc  10673  zsupssdc  10675  flqword2  10726  modfzo0difsn  10834  modsumfzodifsn  10835  uzennn  10875  seq3split  10927  iseqf1olemkle  10936  iseqf1olemklt  10937  iseqf1olemqk  10946  seq3f1olemqsumkj  10950  seq3f1olemqsumk  10951  seq3f1olemqsum  10952  bcval5  11203  bcm1n  11209  1elfz0hash  11249  seq3coll  11296  ccatrn  11379  ccat2s1fvwd  11417  pfxn0  11462  pfxtrcfv0  11468  pfxtrcfvl  11471  swrdswrd  11479  swrdccatin1  11499  pfxccat3  11508  pfxccat3a  11512  cats1fvd  11540  seq3shft  11605  resqrexlemoverl  11789  fsum3cvg3  12165  fisumrev2  12215  isumshft  12259  cvgratnnlemseq  12295  cvgratnnlemabsle  12296  cvgratnnlemsumlt  12297  cvgratz  12301  sinbnd2  12523  cosbnd2  12524  sinltxirr  12530  cos12dec  12537  nn0o  12676  bitsfzolem  12723  bitsfzo  12724  bitsmod  12725  bitsfi  12726  bitsinv1lem  12730  bitsinv1  12731  uzwodc  12816  dvdsnprmd  12905  eulerthlema  13010  hashgcdlem  13018  prm23lt5  13044  prm23ge5  13045  zgz  13154  gznegcl  13156  gzcjcl  13157  gzaddcl  13158  gzmulcl  13159  ballotfilemsel1i  13258  ballotfilemro  13268  ballotfilemfrceq  13274  nninfdclemcl  13341  nninfdclemp1  13343  nninfdclemlt  13344  unbendc  13347  strleund  13459  gzsumcl  13806  subgid  13980  issubg2m  13994  subsubg  14002  gzsumreidx  14143  gzsumsubmcl  14144  gzsummhm  14147  gzsumsplit0  14150  gzsumshift  14151  gzsumgsum  14157  isrngd  14254  ringrng  14343  isringd  14348  ringsrg  14354  subrngid  14511  subrngsubg  14514  issubrng2  14520  subsubrng  14524  subrgsubg  14537  islmodd  14631  dflidl2rng  14820  rnglidlrng  14837  rng2idlsubrng  14856  znidomb  14995  plyaddlem1  15850  sin0pilem1  15885  sin0pilem2  15886  cosq14gt0  15936  cosq23lt0  15937  coseq0q4123  15938  coseq00topi  15939  coseq0negpitopi  15940  tangtx  15942  cosordlem  15953  cosq34lt1  15954  cos02pilt1  15955  cos0pilt1  15956  rplogbval  16053  lgsdilem2  16167  gausslemma2dlem1a  16189  gausslemma2dlem2  16193  gausslemma2dlem5  16197  gausslemma2dlem6  16198  lgsquadlem1  16208  lgsquadlem2  16209  lgsquadlem3  16210  2lgslem1  16222  2sqlem3  16248  umgr2cwwkdifex  16678  trlsegvdeglem6  16718  depindlem2  16760  nnnninfen  17076  repiecelem  17086  repiecele0  17087  repiecege0  17088  cvgcmp2nlemabs  17093  iooref1o  17095  taupi  17135