Theorem syl3anbrc 1186

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

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

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 985

This theorem is referenced by:  smores2  6410  smoiso  6418  iserd  6676  erinxp  6726  resixp  6850  netap  7408  2omotaplemap  7411  prarloc  7658  eluzuzle  9698  uztrn  9707  nn0pzuz  9750  nn0ge2m1nnALT  9781  ige2m1fz  10274  0elfz  10282  uzsubfz0  10293  elfzmlbm  10295  difelfzle  10298  difelfznle  10299  elfzolt2b  10323  elfzolt3b  10324  elfzouz2  10326  fzossrbm1  10339  elfzo0  10350  eluzgtdifelfzo  10370  elfzodifsumelfzo  10374  fzonn0p1  10384  fzonn0p1p1  10386  elfzom1p1elfzo  10387  fzo0sn0fzo1  10394  ssfzo12bi  10398  ubmelm1fzo  10399  elfzonelfzo  10403  fzosplitprm1  10407  fzostep1  10410  fvinim0ffz  10414  suprzubdc  10423  zsupssdc  10425  flqword2  10476  modfzo0difsn  10584  modsumfzodifsn  10585  uzennn  10625  seq3split  10677  iseqf1olemkle  10686  iseqf1olemklt  10687  iseqf1olemqk  10696  seq3f1olemqsumkj  10700  seq3f1olemqsumk  10701  seq3f1olemqsum  10702  bcval5  10952  1elfz0hash  10995  seq3coll  11031  ccatrn  11110  pfxn0  11186  pfxtrcfv0  11192  pfxtrcfvl  11195  swrdswrd  11203  swrdccatin1  11223  pfxccat3  11232  pfxccat3a  11236  cats1fvd  11264  seq3shft  11315  resqrexlemoverl  11498  fsum3cvg3  11873  fisumrev2  11923  isumshft  11967  cvgratnnlemseq  12003  cvgratnnlemabsle  12004  cvgratnnlemsumlt  12005  cvgratz  12009  sinbnd2  12231  cosbnd2  12232  sinltxirr  12238  cos12dec  12245  nn0o  12384  bitsfzolem  12431  bitsfzo  12432  bitsmod  12433  bitsfi  12434  bitsinv1lem  12438  bitsinv1  12439  uzwodc  12524  dvdsnprmd  12613  eulerthlema  12718  hashgcdlem  12726  prm23lt5  12752  prm23ge5  12753  zgz  12862  gznegcl  12864  gzcjcl  12865  gzaddcl  12866  gzmulcl  12867  nninfdclemcl  12985  nninfdclemp1  12987  nninfdclemlt  12988  unbendc  12991  strleund  13102  gsumfzz  13494  gsumfzcl  13498  subgid  13678  issubg2m  13692  subsubg  13700  gsumfzreidx  13840  gsumfzsubmcl  13841  gsumfzmptfidmadd  13842  gsumfzmhm  13846  isrngd  13882  ringrng  13965  isringd  13970  ringsrg  13976  subrngid  14130  subrngsubg  14133  issubrng2  14139  subsubrng  14143  subrgsubg  14156  islmodd  14222  dflidl2rng  14410  rnglidlrng  14427  rng2idlsubrng  14446  gsumfzfsum  14517  znidomb  14587  plyaddlem1  15386  sin0pilem1  15420  sin0pilem2  15421  cosq14gt0  15471  cosq23lt0  15472  coseq0q4123  15473  coseq00topi  15474  coseq0negpitopi  15475  tangtx  15477  cosordlem  15488  cosq34lt1  15489  cos02pilt1  15490  cos0pilt1  15491  rplogbval  15584  lgsdilem2  15680  gausslemma2dlem1a  15702  gausslemma2dlem2  15706  gausslemma2dlem5  15710  gausslemma2dlem6  15711  lgsquadlem1  15721  lgsquadlem2  15722  lgsquadlem3  15723  2lgslem1  15735  2sqlem3  15761  nnnninfen  16298  cvgcmp2nlemabs  16311  iooref1o  16313  taupi  16352