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  6538  smoiso  6546  iserd  6806  erinxp  6856  resixp  6981  netap  7584  2omotaplemap  7587  prarloc  7834  eluzmn  9878  eluzuzle  9880  uztrn  9889  nn0pzuz  9937  nn0ge2m1nnALT  9968  ige2m1fz  10466  0elfz  10474  uzsubfz0  10485  elfzmlbm  10487  difelfzle  10490  difelfznle  10491  elfzolt2b  10515  elfzolt3b  10516  elfzouz2  10518  fzossrbm1  10531  elfzo0  10542  eluzgtdifelfzo  10564  elfzodifsumelfzo  10568  fzonn0p1  10578  fzonn0p1p1  10580  elfzom1p1elfzo  10581  fzo0sn0fzo1  10588  ssfzo12bi  10592  ubmelm1fzo  10593  elfzonelfzo  10597  fzosplitprm1  10602  fzostep1  10605  fvinim0ffz  10609  suprzubdc  10620  zsupssdc  10622  flqword2  10673  modfzo0difsn  10781  modsumfzodifsn  10782  uzennn  10822  seq3split  10874  iseqf1olemkle  10883  iseqf1olemklt  10884  iseqf1olemqk  10893  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  bcval5  11150  bcm1n  11156  1elfz0hash  11196  seq3coll  11239  ccatrn  11322  ccat2s1fvwd  11360  pfxn0  11405  pfxtrcfv0  11411  pfxtrcfvl  11414  swrdswrd  11422  swrdccatin1  11442  pfxccat3  11451  pfxccat3a  11455  cats1fvd  11483  seq3shft  11548  resqrexlemoverl  11731  fsum3cvg3  12107  fisumrev2  12157  isumshft  12201  cvgratnnlemseq  12237  cvgratnnlemabsle  12238  cvgratnnlemsumlt  12239  cvgratz  12243  sinbnd2  12465  cosbnd2  12466  sinltxirr  12472  cos12dec  12479  nn0o  12618  bitsfzolem  12665  bitsfzo  12666  bitsmod  12667  bitsfi  12668  bitsinv1lem  12672  bitsinv1  12673  uzwodc  12758  dvdsnprmd  12847  eulerthlema  12952  hashgcdlem  12960  prm23lt5  12986  prm23ge5  12987  zgz  13096  gznegcl  13098  gzcjcl  13099  gzaddcl  13100  gzmulcl  13101  ballotfilemsel1i  13200  ballotfilemro  13210  ballotfilemfrceq  13216  nninfdclemcl  13283  nninfdclemp1  13285  nninfdclemlt  13286  unbendc  13289  strleund  13400  gsumfzz  13750  gsumfzcl  13754  subgid  13928  issubg2m  13942  subsubg  13950  gsumfzreidx  14090  gsumfzsubmcl  14091  gsumfzmptfidmadd  14092  gsumfzmhm  14096  gsumsplit0  14099  gsumshift  14105  gsumgfsum  14106  isrngd  14192  ringrng  14279  isringd  14284  ringsrg  14290  subrngid  14447  subrngsubg  14450  issubrng2  14456  subsubrng  14460  subrgsubg  14473  islmodd  14567  dflidl2rng  14755  rnglidlrng  14772  rng2idlsubrng  14791  gsumfzfsum  14862  znidomb  14932  plyaddlem1  15738  sin0pilem1  15772  sin0pilem2  15773  cosq14gt0  15823  cosq23lt0  15824  coseq0q4123  15825  coseq00topi  15826  coseq0negpitopi  15827  tangtx  15829  cosordlem  15840  cosq34lt1  15841  cos02pilt1  15842  cos0pilt1  15843  rplogbval  15936  lgsdilem2  16035  gausslemma2dlem1a  16057  gausslemma2dlem2  16061  gausslemma2dlem5  16065  gausslemma2dlem6  16066  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  2lgslem1  16090  2sqlem3  16116  umgr2cwwkdifex  16546  trlsegvdeglem6  16586  depindlem2  16628  nnnninfen  16925  repiecelem  16935  repiecele0  16936  repiecege0  16937  cvgcmp2nlemabs  16942  iooref1o  16944  taupi  16985