Theorem syl3anbrc 1208

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 1204	. 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 1005

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 1007

This theorem is referenced by:  smores2  6525  smoiso  6533  iserd  6793  erinxp  6843  resixp  6968  netap  7568  2omotaplemap  7571  prarloc  7818  eluzmn  9860  eluzuzle  9862  uztrn  9871  nn0pzuz  9919  nn0ge2m1nnALT  9950  ige2m1fz  10444  0elfz  10452  uzsubfz0  10463  elfzmlbm  10465  difelfzle  10468  difelfznle  10469  elfzolt2b  10493  elfzolt3b  10494  elfzouz2  10496  fzossrbm1  10509  elfzo0  10520  eluzgtdifelfzo  10542  elfzodifsumelfzo  10546  fzonn0p1  10556  fzonn0p1p1  10558  elfzom1p1elfzo  10559  fzo0sn0fzo1  10566  ssfzo12bi  10570  ubmelm1fzo  10571  elfzonelfzo  10575  fzosplitprm1  10580  fzostep1  10583  fvinim0ffz  10587  suprzubdc  10596  zsupssdc  10598  flqword2  10649  modfzo0difsn  10757  modsumfzodifsn  10758  uzennn  10798  seq3split  10850  iseqf1olemkle  10859  iseqf1olemklt  10860  iseqf1olemqk  10869  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3f1olemqsum  10875  bcval5  11125  bcm1n  11131  1elfz0hash  11171  seq3coll  11214  ccatrn  11297  ccat2s1fvwd  11335  pfxn0  11380  pfxtrcfv0  11386  pfxtrcfvl  11389  swrdswrd  11397  swrdccatin1  11417  pfxccat3  11426  pfxccat3a  11430  cats1fvd  11458  seq3shft  11523  resqrexlemoverl  11706  fsum3cvg3  12082  fisumrev2  12132  isumshft  12176  cvgratnnlemseq  12212  cvgratnnlemabsle  12213  cvgratnnlemsumlt  12214  cvgratz  12218  sinbnd2  12440  cosbnd2  12441  sinltxirr  12447  cos12dec  12454  nn0o  12593  bitsfzolem  12640  bitsfzo  12641  bitsmod  12642  bitsfi  12643  bitsinv1lem  12647  bitsinv1  12648  uzwodc  12733  dvdsnprmd  12822  eulerthlema  12927  hashgcdlem  12935  prm23lt5  12961  prm23ge5  12962  zgz  13071  gznegcl  13073  gzcjcl  13074  gzaddcl  13075  gzmulcl  13076  nninfdclemcl  13199  nninfdclemp1  13201  nninfdclemlt  13202  unbendc  13205  strleund  13316  gsumfzz  13708  gsumfzcl  13712  subgid  13892  issubg2m  13906  subsubg  13914  gsumfzreidx  14054  gsumfzsubmcl  14055  gsumfzmptfidmadd  14056  gsumfzmhm  14060  gsumsplit0  14063  isrngd  14097  ringrng  14180  isringd  14185  ringsrg  14191  subrngid  14346  subrngsubg  14349  issubrng2  14355  subsubrng  14359  subrgsubg  14372  islmodd  14441  dflidl2rng  14629  rnglidlrng  14646  rng2idlsubrng  14665  gsumfzfsum  14736  znidomb  14806  plyaddlem1  15612  sin0pilem1  15646  sin0pilem2  15647  cosq14gt0  15697  cosq23lt0  15698  coseq0q4123  15699  coseq00topi  15700  coseq0negpitopi  15701  tangtx  15703  cosordlem  15714  cosq34lt1  15715  cos02pilt1  15716  cos0pilt1  15717  rplogbval  15810  lgsdilem2  15909  gausslemma2dlem1a  15931  gausslemma2dlem2  15935  gausslemma2dlem5  15939  gausslemma2dlem6  15940  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  2lgslem1  15964  2sqlem3  15990  umgr2cwwkdifex  16420  trlsegvdeglem6  16460  depindlem2  16502  nnnninfen  16799  repiecelem  16809  repiecele0  16810  repiecege0  16811  cvgcmp2nlemabs  16816  iooref1o  16818  taupi  16859  gsumgfsumlem  16865  gsumgfsum  16866