Theorem syl3anbrc 1183

Description: Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)

Hypotheses

Ref	Expression
syl3anbrc.1	|- ( ph -> ps )
syl3anbrc.2	|- ( ph -> ch )
syl3anbrc.3	|- ( ph -> th )
syl3anbrc.4	|- ( ta <-> ( ps /\ ch /\ th ) )

Assertion

Ref	Expression
syl3anbrc	|- ( ph -> ta )

Proof of Theorem syl3anbrc

Step	Hyp	Ref	Expression
1		syl3anbrc.1	. . 3 |- ( ph -> ps )
2		syl3anbrc.2	. . 3 |- ( ph -> ch )
3		syl3anbrc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	3jca 1179	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
5		syl3anbrc.4	. 2 |- ( ta <-> ( ps /\ ch /\ th ) )
6	4, 5	sylibr 134	1 |- ( ph -> ta )

Syntax hints:   -> wi 4   <-> wb 105   /\ w3a 980

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 982

This theorem is referenced by:  smores2  6352  smoiso  6360  iserd  6618  erinxp  6668  resixp  6792  netap  7321  2omotaplemap  7324  prarloc  7570  eluzuzle  9609  uztrn  9618  nn0pzuz  9661  nn0ge2m1nnALT  9692  ige2m1fz  10185  0elfz  10193  uzsubfz0  10204  elfzmlbm  10206  difelfzle  10209  difelfznle  10210  elfzolt2b  10234  elfzolt3b  10235  elfzouz2  10237  fzossrbm1  10249  elfzo0  10258  eluzgtdifelfzo  10273  elfzodifsumelfzo  10277  fzonn0p1  10287  fzonn0p1p1  10289  elfzom1p1elfzo  10290  fzo0sn0fzo1  10297  ssfzo12bi  10301  ubmelm1fzo  10302  elfzonelfzo  10306  fzosplitprm1  10310  fzostep1  10313  fvinim0ffz  10317  suprzubdc  10326  zsupssdc  10328  flqword2  10379  modfzo0difsn  10487  modsumfzodifsn  10488  uzennn  10528  seq3split  10580  iseqf1olemkle  10589  iseqf1olemklt  10590  iseqf1olemqk  10599  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  bcval5  10855  1elfz0hash  10898  seq3coll  10934  seq3shft  11003  resqrexlemoverl  11186  fsum3cvg3  11561  fisumrev2  11611  isumshft  11655  cvgratnnlemseq  11691  cvgratnnlemabsle  11692  cvgratnnlemsumlt  11693  cvgratz  11697  sinbnd2  11919  cosbnd2  11920  sinltxirr  11926  cos12dec  11933  nn0o  12072  bitsfzolem  12118  bitsfzo  12119  uzwodc  12204  dvdsnprmd  12293  eulerthlema  12398  hashgcdlem  12406  prm23lt5  12432  prm23ge5  12433  zgz  12542  gznegcl  12544  gzcjcl  12545  gzaddcl  12546  gzmulcl  12547  nninfdclemcl  12665  nninfdclemp1  12667  nninfdclemlt  12668  unbendc  12671  strleund  12781  gsumfzz  13127  gsumfzcl  13131  subgid  13305  issubg2m  13319  subsubg  13327  gsumfzreidx  13467  gsumfzsubmcl  13468  gsumfzmptfidmadd  13469  gsumfzmhm  13473  isrngd  13509  ringrng  13592  isringd  13597  ringsrg  13603  subrngid  13757  subrngsubg  13760  issubrng2  13766  subsubrng  13770  subrgsubg  13783  islmodd  13849  dflidl2rng  14037  rnglidlrng  14054  rng2idlsubrng  14073  gsumfzfsum  14144  znidomb  14214  plyaddlem1  14983  sin0pilem1  15017  sin0pilem2  15018  cosq14gt0  15068  cosq23lt0  15069  coseq0q4123  15070  coseq00topi  15071  coseq0negpitopi  15072  tangtx  15074  cosordlem  15085  cosq34lt1  15086  cos02pilt1  15087  cos0pilt1  15088  rplogbval  15181  lgsdilem2  15277  gausslemma2dlem1a  15299  gausslemma2dlem2  15303  gausslemma2dlem5  15307  gausslemma2dlem6  15308  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  2lgslem1  15332  2sqlem3  15358  nnnninfen  15665  cvgcmp2nlemabs  15676  iooref1o  15678  taupi  15717