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  6455  smoiso  6463  iserd  6723  erinxp  6773  resixp  6897  netap  7466  2omotaplemap  7469  prarloc  7716  eluzmn  9755  eluzuzle  9757  uztrn  9766  nn0pzuz  9814  nn0ge2m1nnALT  9845  ige2m1fz  10338  0elfz  10346  uzsubfz0  10357  elfzmlbm  10359  difelfzle  10362  difelfznle  10363  elfzolt2b  10387  elfzolt3b  10388  elfzouz2  10390  fzossrbm1  10403  elfzo0  10414  eluzgtdifelfzo  10435  elfzodifsumelfzo  10439  fzonn0p1  10449  fzonn0p1p1  10451  elfzom1p1elfzo  10452  fzo0sn0fzo1  10459  ssfzo12bi  10463  ubmelm1fzo  10464  elfzonelfzo  10468  fzosplitprm1  10473  fzostep1  10476  fvinim0ffz  10480  suprzubdc  10489  zsupssdc  10491  flqword2  10542  modfzo0difsn  10650  modsumfzodifsn  10651  uzennn  10691  seq3split  10743  iseqf1olemkle  10752  iseqf1olemklt  10753  iseqf1olemqk  10762  seq3f1olemqsumkj  10766  seq3f1olemqsumk  10767  seq3f1olemqsum  10768  bcval5  11018  1elfz0hash  11063  seq3coll  11099  ccatrn  11179  ccat2s1fvwd  11217  pfxn0  11262  pfxtrcfv0  11268  pfxtrcfvl  11271  swrdswrd  11279  swrdccatin1  11299  pfxccat3  11308  pfxccat3a  11312  cats1fvd  11340  seq3shft  11392  resqrexlemoverl  11575  fsum3cvg3  11950  fisumrev2  12000  isumshft  12044  cvgratnnlemseq  12080  cvgratnnlemabsle  12081  cvgratnnlemsumlt  12082  cvgratz  12086  sinbnd2  12308  cosbnd2  12309  sinltxirr  12315  cos12dec  12322  nn0o  12461  bitsfzolem  12508  bitsfzo  12509  bitsmod  12510  bitsfi  12511  bitsinv1lem  12515  bitsinv1  12516  uzwodc  12601  dvdsnprmd  12690  eulerthlema  12795  hashgcdlem  12803  prm23lt5  12829  prm23ge5  12830  zgz  12939  gznegcl  12941  gzcjcl  12942  gzaddcl  12943  gzmulcl  12944  nninfdclemcl  13062  nninfdclemp1  13064  nninfdclemlt  13065  unbendc  13068  strleund  13179  gsumfzz  13571  gsumfzcl  13575  subgid  13755  issubg2m  13769  subsubg  13777  gsumfzreidx  13917  gsumfzsubmcl  13918  gsumfzmptfidmadd  13919  gsumfzmhm  13923  isrngd  13959  ringrng  14042  isringd  14047  ringsrg  14053  subrngid  14208  subrngsubg  14211  issubrng2  14217  subsubrng  14221  subrgsubg  14234  islmodd  14300  dflidl2rng  14488  rnglidlrng  14505  rng2idlsubrng  14524  gsumfzfsum  14595  znidomb  14665  plyaddlem1  15464  sin0pilem1  15498  sin0pilem2  15499  cosq14gt0  15549  cosq23lt0  15550  coseq0q4123  15551  coseq00topi  15552  coseq0negpitopi  15553  tangtx  15555  cosordlem  15566  cosq34lt1  15567  cos02pilt1  15568  cos0pilt1  15569  rplogbval  15662  lgsdilem2  15758  gausslemma2dlem1a  15780  gausslemma2dlem2  15784  gausslemma2dlem5  15788  gausslemma2dlem6  15789  lgsquadlem1  15799  lgsquadlem2  15800  lgsquadlem3  15801  2lgslem1  15813  2sqlem3  15839  umgr2cwwkdifex  16234  nnnninfen  16573  cvgcmp2nlemabs  16586  iooref1o  16588  taupi  16627  gsumgfsumlem  16633  gsumgfsum  16634