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  6451  smoiso  6459  iserd  6719  erinxp  6769  resixp  6893  netap  7456  2omotaplemap  7459  prarloc  7706  eluzmn  9745  eluzuzle  9747  uztrn  9756  nn0pzuz  9799  nn0ge2m1nnALT  9830  ige2m1fz  10323  0elfz  10331  uzsubfz0  10342  elfzmlbm  10344  difelfzle  10347  difelfznle  10348  elfzolt2b  10372  elfzolt3b  10373  elfzouz2  10375  fzossrbm1  10388  elfzo0  10399  eluzgtdifelfzo  10420  elfzodifsumelfzo  10424  fzonn0p1  10434  fzonn0p1p1  10436  elfzom1p1elfzo  10437  fzo0sn0fzo1  10444  ssfzo12bi  10448  ubmelm1fzo  10449  elfzonelfzo  10453  fzosplitprm1  10457  fzostep1  10460  fvinim0ffz  10464  suprzubdc  10473  zsupssdc  10475  flqword2  10526  modfzo0difsn  10634  modsumfzodifsn  10635  uzennn  10675  seq3split  10727  iseqf1olemkle  10736  iseqf1olemklt  10737  iseqf1olemqk  10746  seq3f1olemqsumkj  10750  seq3f1olemqsumk  10751  seq3f1olemqsum  10752  bcval5  11002  1elfz0hash  11046  seq3coll  11082  ccatrn  11162  pfxn0  11241  pfxtrcfv0  11247  pfxtrcfvl  11250  swrdswrd  11258  swrdccatin1  11278  pfxccat3  11287  pfxccat3a  11291  cats1fvd  11319  seq3shft  11370  resqrexlemoverl  11553  fsum3cvg3  11928  fisumrev2  11978  isumshft  12022  cvgratnnlemseq  12058  cvgratnnlemabsle  12059  cvgratnnlemsumlt  12060  cvgratz  12064  sinbnd2  12286  cosbnd2  12287  sinltxirr  12293  cos12dec  12300  nn0o  12439  bitsfzolem  12486  bitsfzo  12487  bitsmod  12488  bitsfi  12489  bitsinv1lem  12493  bitsinv1  12494  uzwodc  12579  dvdsnprmd  12668  eulerthlema  12773  hashgcdlem  12781  prm23lt5  12807  prm23ge5  12808  zgz  12917  gznegcl  12919  gzcjcl  12920  gzaddcl  12921  gzmulcl  12922  nninfdclemcl  13040  nninfdclemp1  13042  nninfdclemlt  13043  unbendc  13046  strleund  13157  gsumfzz  13549  gsumfzcl  13553  subgid  13733  issubg2m  13747  subsubg  13755  gsumfzreidx  13895  gsumfzsubmcl  13896  gsumfzmptfidmadd  13897  gsumfzmhm  13901  isrngd  13937  ringrng  14020  isringd  14025  ringsrg  14031  subrngid  14186  subrngsubg  14189  issubrng2  14195  subsubrng  14199  subrgsubg  14212  islmodd  14278  dflidl2rng  14466  rnglidlrng  14483  rng2idlsubrng  14502  gsumfzfsum  14573  znidomb  14643  plyaddlem1  15442  sin0pilem1  15476  sin0pilem2  15477  cosq14gt0  15527  cosq23lt0  15528  coseq0q4123  15529  coseq00topi  15530  coseq0negpitopi  15531  tangtx  15533  cosordlem  15544  cosq34lt1  15545  cos02pilt1  15546  cos0pilt1  15547  rplogbval  15640  lgsdilem2  15736  gausslemma2dlem1a  15758  gausslemma2dlem2  15762  gausslemma2dlem5  15766  gausslemma2dlem6  15767  lgsquadlem1  15777  lgsquadlem2  15778  lgsquadlem3  15779  2lgslem1  15791  2sqlem3  15817  umgr2cwwkdifex  16193  nnnninfen  16501  cvgcmp2nlemabs  16514  iooref1o  16516  taupi  16555