Theorem syl3anbrc 1205

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

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

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 1004

This theorem is referenced by:  smores2  6446  smoiso  6454  iserd  6714  erinxp  6764  resixp  6888  netap  7448  2omotaplemap  7451  prarloc  7698  eluzuzle  9738  uztrn  9747  nn0pzuz  9790  nn0ge2m1nnALT  9821  ige2m1fz  10314  0elfz  10322  uzsubfz0  10333  elfzmlbm  10335  difelfzle  10338  difelfznle  10339  elfzolt2b  10363  elfzolt3b  10364  elfzouz2  10366  fzossrbm1  10379  elfzo0  10390  eluzgtdifelfzo  10411  elfzodifsumelfzo  10415  fzonn0p1  10425  fzonn0p1p1  10427  elfzom1p1elfzo  10428  fzo0sn0fzo1  10435  ssfzo12bi  10439  ubmelm1fzo  10440  elfzonelfzo  10444  fzosplitprm1  10448  fzostep1  10451  fvinim0ffz  10455  suprzubdc  10464  zsupssdc  10466  flqword2  10517  modfzo0difsn  10625  modsumfzodifsn  10626  uzennn  10666  seq3split  10718  iseqf1olemkle  10727  iseqf1olemklt  10728  iseqf1olemqk  10737  seq3f1olemqsumkj  10741  seq3f1olemqsumk  10742  seq3f1olemqsum  10743  bcval5  10993  1elfz0hash  11036  seq3coll  11072  ccatrn  11152  pfxn0  11228  pfxtrcfv0  11234  pfxtrcfvl  11237  swrdswrd  11245  swrdccatin1  11265  pfxccat3  11274  pfxccat3a  11278  cats1fvd  11306  seq3shft  11357  resqrexlemoverl  11540  fsum3cvg3  11915  fisumrev2  11965  isumshft  12009  cvgratnnlemseq  12045  cvgratnnlemabsle  12046  cvgratnnlemsumlt  12047  cvgratz  12051  sinbnd2  12273  cosbnd2  12274  sinltxirr  12280  cos12dec  12287  nn0o  12426  bitsfzolem  12473  bitsfzo  12474  bitsmod  12475  bitsfi  12476  bitsinv1lem  12480  bitsinv1  12481  uzwodc  12566  dvdsnprmd  12655  eulerthlema  12760  hashgcdlem  12768  prm23lt5  12794  prm23ge5  12795  zgz  12904  gznegcl  12906  gzcjcl  12907  gzaddcl  12908  gzmulcl  12909  nninfdclemcl  13027  nninfdclemp1  13029  nninfdclemlt  13030  unbendc  13033  strleund  13144  gsumfzz  13536  gsumfzcl  13540  subgid  13720  issubg2m  13734  subsubg  13742  gsumfzreidx  13882  gsumfzsubmcl  13883  gsumfzmptfidmadd  13884  gsumfzmhm  13888  isrngd  13924  ringrng  14007  isringd  14012  ringsrg  14018  subrngid  14173  subrngsubg  14176  issubrng2  14182  subsubrng  14186  subrgsubg  14199  islmodd  14265  dflidl2rng  14453  rnglidlrng  14470  rng2idlsubrng  14489  gsumfzfsum  14560  znidomb  14630  plyaddlem1  15429  sin0pilem1  15463  sin0pilem2  15464  cosq14gt0  15514  cosq23lt0  15515  coseq0q4123  15516  coseq00topi  15517  coseq0negpitopi  15518  tangtx  15520  cosordlem  15531  cosq34lt1  15532  cos02pilt1  15533  cos0pilt1  15534  rplogbval  15627  lgsdilem2  15723  gausslemma2dlem1a  15745  gausslemma2dlem2  15749  gausslemma2dlem5  15753  gausslemma2dlem6  15754  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  2lgslem1  15778  2sqlem3  15804  nnnninfen  16417  cvgcmp2nlemabs  16430  iooref1o  16432  taupi  16471