Theorem syl3anbrc 1207

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 1203	. 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 1004

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 1006

This theorem is referenced by:  smores2  6460  smoiso  6468  iserd  6728  erinxp  6778  resixp  6902  netap  7473  2omotaplemap  7476  prarloc  7723  eluzmn  9762  eluzuzle  9764  uztrn  9773  nn0pzuz  9821  nn0ge2m1nnALT  9852  ige2m1fz  10345  0elfz  10353  uzsubfz0  10364  elfzmlbm  10366  difelfzle  10369  difelfznle  10370  elfzolt2b  10394  elfzolt3b  10395  elfzouz2  10397  fzossrbm1  10410  elfzo0  10421  eluzgtdifelfzo  10443  elfzodifsumelfzo  10447  fzonn0p1  10457  fzonn0p1p1  10459  elfzom1p1elfzo  10460  fzo0sn0fzo1  10467  ssfzo12bi  10471  ubmelm1fzo  10472  elfzonelfzo  10476  fzosplitprm1  10481  fzostep1  10484  fvinim0ffz  10488  suprzubdc  10497  zsupssdc  10499  flqword2  10550  modfzo0difsn  10658  modsumfzodifsn  10659  uzennn  10699  seq3split  10751  iseqf1olemkle  10760  iseqf1olemklt  10761  iseqf1olemqk  10770  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  bcval5  11026  1elfz0hash  11071  seq3coll  11107  ccatrn  11190  ccat2s1fvwd  11228  pfxn0  11273  pfxtrcfv0  11279  pfxtrcfvl  11282  swrdswrd  11290  swrdccatin1  11310  pfxccat3  11319  pfxccat3a  11323  cats1fvd  11351  seq3shft  11416  resqrexlemoverl  11599  fsum3cvg3  11975  fisumrev2  12025  isumshft  12069  cvgratnnlemseq  12105  cvgratnnlemabsle  12106  cvgratnnlemsumlt  12107  cvgratz  12111  sinbnd2  12333  cosbnd2  12334  sinltxirr  12340  cos12dec  12347  nn0o  12486  bitsfzolem  12533  bitsfzo  12534  bitsmod  12535  bitsfi  12536  bitsinv1lem  12540  bitsinv1  12541  uzwodc  12626  dvdsnprmd  12715  eulerthlema  12820  hashgcdlem  12828  prm23lt5  12854  prm23ge5  12855  zgz  12964  gznegcl  12966  gzcjcl  12967  gzaddcl  12968  gzmulcl  12969  nninfdclemcl  13087  nninfdclemp1  13089  nninfdclemlt  13090  unbendc  13093  strleund  13204  gsumfzz  13596  gsumfzcl  13600  subgid  13780  issubg2m  13794  subsubg  13802  gsumfzreidx  13942  gsumfzsubmcl  13943  gsumfzmptfidmadd  13944  gsumfzmhm  13948  gsumsplit0  13951  isrngd  13985  ringrng  14068  isringd  14073  ringsrg  14079  subrngid  14234  subrngsubg  14237  issubrng2  14243  subsubrng  14247  subrgsubg  14260  islmodd  14326  dflidl2rng  14514  rnglidlrng  14531  rng2idlsubrng  14550  gsumfzfsum  14621  znidomb  14691  plyaddlem1  15490  sin0pilem1  15524  sin0pilem2  15525  cosq14gt0  15575  cosq23lt0  15576  coseq0q4123  15577  coseq00topi  15578  coseq0negpitopi  15579  tangtx  15581  cosordlem  15592  cosq34lt1  15593  cos02pilt1  15594  cos0pilt1  15595  rplogbval  15688  lgsdilem2  15784  gausslemma2dlem1a  15806  gausslemma2dlem2  15810  gausslemma2dlem5  15814  gausslemma2dlem6  15815  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  2lgslem1  15839  2sqlem3  15865  umgr2cwwkdifex  16295  trlsegvdeglem6  16335  depindlem2  16377  nnnninfen  16674  cvgcmp2nlemabs  16687  iooref1o  16689  taupi  16729  gsumgfsumlem  16735  gsumgfsum  16736