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  6527  smoiso  6535  iserd  6795  erinxp  6845  resixp  6970  netap  7573  2omotaplemap  7576  prarloc  7823  eluzmn  9866  eluzuzle  9868  uztrn  9877  nn0pzuz  9925  nn0ge2m1nnALT  9956  ige2m1fz  10451  0elfz  10459  uzsubfz0  10470  elfzmlbm  10472  difelfzle  10475  difelfznle  10476  elfzolt2b  10500  elfzolt3b  10501  elfzouz2  10503  fzossrbm1  10516  elfzo0  10527  eluzgtdifelfzo  10549  elfzodifsumelfzo  10553  fzonn0p1  10563  fzonn0p1p1  10565  elfzom1p1elfzo  10566  fzo0sn0fzo1  10573  ssfzo12bi  10577  ubmelm1fzo  10578  elfzonelfzo  10582  fzosplitprm1  10587  fzostep1  10590  fvinim0ffz  10594  suprzubdc  10603  zsupssdc  10605  flqword2  10656  modfzo0difsn  10764  modsumfzodifsn  10765  uzennn  10805  seq3split  10857  iseqf1olemkle  10866  iseqf1olemklt  10867  iseqf1olemqk  10876  seq3f1olemqsumkj  10880  seq3f1olemqsumk  10881  seq3f1olemqsum  10882  bcval5  11133  bcm1n  11139  1elfz0hash  11179  seq3coll  11222  ccatrn  11305  ccat2s1fvwd  11343  pfxn0  11388  pfxtrcfv0  11394  pfxtrcfvl  11397  swrdswrd  11405  swrdccatin1  11425  pfxccat3  11434  pfxccat3a  11438  cats1fvd  11466  seq3shft  11531  resqrexlemoverl  11714  fsum3cvg3  12090  fisumrev2  12140  isumshft  12184  cvgratnnlemseq  12220  cvgratnnlemabsle  12221  cvgratnnlemsumlt  12222  cvgratz  12226  sinbnd2  12448  cosbnd2  12449  sinltxirr  12455  cos12dec  12462  nn0o  12601  bitsfzolem  12648  bitsfzo  12649  bitsmod  12650  bitsfi  12651  bitsinv1lem  12655  bitsinv1  12656  uzwodc  12741  dvdsnprmd  12830  eulerthlema  12935  hashgcdlem  12943  prm23lt5  12969  prm23ge5  12970  zgz  13079  gznegcl  13081  gzcjcl  13082  gzaddcl  13083  gzmulcl  13084  nninfdclemcl  13220  nninfdclemp1  13222  nninfdclemlt  13223  unbendc  13226  strleund  13337  gsumfzz  13729  gsumfzcl  13733  subgid  13913  issubg2m  13927  subsubg  13935  gsumfzreidx  14075  gsumfzsubmcl  14076  gsumfzmptfidmadd  14077  gsumfzmhm  14081  gsumsplit0  14084  isrngd  14118  ringrng  14201  isringd  14206  ringsrg  14212  subrngid  14369  subrngsubg  14372  issubrng2  14378  subsubrng  14382  subrgsubg  14395  islmodd  14490  dflidl2rng  14678  rnglidlrng  14695  rng2idlsubrng  14714  gsumfzfsum  14785  znidomb  14855  plyaddlem1  15661  sin0pilem1  15695  sin0pilem2  15696  cosq14gt0  15746  cosq23lt0  15747  coseq0q4123  15748  coseq00topi  15749  coseq0negpitopi  15750  tangtx  15752  cosordlem  15763  cosq34lt1  15764  cos02pilt1  15765  cos0pilt1  15766  rplogbval  15859  lgsdilem2  15958  gausslemma2dlem1a  15980  gausslemma2dlem2  15984  gausslemma2dlem5  15988  gausslemma2dlem6  15989  lgsquadlem1  15999  lgsquadlem2  16000  lgsquadlem3  16001  2lgslem1  16013  2sqlem3  16039  umgr2cwwkdifex  16469  trlsegvdeglem6  16509  depindlem2  16551  nnnninfen  16848  repiecelem  16858  repiecele0  16859  repiecege0  16860  cvgcmp2nlemabs  16865  iooref1o  16867  taupi  16908  gsumgfsumlem  16914  gsumgfsum  16915