Theorem syl3anbrc 1205

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 1201	. 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 1002

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 1004

This theorem is referenced by:  smores2  6438  smoiso  6446  iserd  6704  erinxp  6754  resixp  6878  netap  7436  2omotaplemap  7439  prarloc  7686  eluzuzle  9726  uztrn  9735  nn0pzuz  9778  nn0ge2m1nnALT  9809  ige2m1fz  10302  0elfz  10310  uzsubfz0  10321  elfzmlbm  10323  difelfzle  10326  difelfznle  10327  elfzolt2b  10351  elfzolt3b  10352  elfzouz2  10354  fzossrbm1  10367  elfzo0  10378  eluzgtdifelfzo  10398  elfzodifsumelfzo  10402  fzonn0p1  10412  fzonn0p1p1  10414  elfzom1p1elfzo  10415  fzo0sn0fzo1  10422  ssfzo12bi  10426  ubmelm1fzo  10427  elfzonelfzo  10431  fzosplitprm1  10435  fzostep1  10438  fvinim0ffz  10442  suprzubdc  10451  zsupssdc  10453  flqword2  10504  modfzo0difsn  10612  modsumfzodifsn  10613  uzennn  10653  seq3split  10705  iseqf1olemkle  10714  iseqf1olemklt  10715  iseqf1olemqk  10724  seq3f1olemqsumkj  10728  seq3f1olemqsumk  10729  seq3f1olemqsum  10730  bcval5  10980  1elfz0hash  11023  seq3coll  11059  ccatrn  11139  pfxn0  11215  pfxtrcfv0  11221  pfxtrcfvl  11224  swrdswrd  11232  swrdccatin1  11252  pfxccat3  11261  pfxccat3a  11265  cats1fvd  11293  seq3shft  11344  resqrexlemoverl  11527  fsum3cvg3  11902  fisumrev2  11952  isumshft  11996  cvgratnnlemseq  12032  cvgratnnlemabsle  12033  cvgratnnlemsumlt  12034  cvgratz  12038  sinbnd2  12260  cosbnd2  12261  sinltxirr  12267  cos12dec  12274  nn0o  12413  bitsfzolem  12460  bitsfzo  12461  bitsmod  12462  bitsfi  12463  bitsinv1lem  12467  bitsinv1  12468  uzwodc  12553  dvdsnprmd  12642  eulerthlema  12747  hashgcdlem  12755  prm23lt5  12781  prm23ge5  12782  zgz  12891  gznegcl  12893  gzcjcl  12894  gzaddcl  12895  gzmulcl  12896  nninfdclemcl  13014  nninfdclemp1  13016  nninfdclemlt  13017  unbendc  13020  strleund  13131  gsumfzz  13523  gsumfzcl  13527  subgid  13707  issubg2m  13721  subsubg  13729  gsumfzreidx  13869  gsumfzsubmcl  13870  gsumfzmptfidmadd  13871  gsumfzmhm  13875  isrngd  13911  ringrng  13994  isringd  13999  ringsrg  14005  subrngid  14159  subrngsubg  14162  issubrng2  14168  subsubrng  14172  subrgsubg  14185  islmodd  14251  dflidl2rng  14439  rnglidlrng  14456  rng2idlsubrng  14475  gsumfzfsum  14546  znidomb  14616  plyaddlem1  15415  sin0pilem1  15449  sin0pilem2  15450  cosq14gt0  15500  cosq23lt0  15501  coseq0q4123  15502  coseq00topi  15503  coseq0negpitopi  15504  tangtx  15506  cosordlem  15517  cosq34lt1  15518  cos02pilt1  15519  cos0pilt1  15520  rplogbval  15613  lgsdilem2  15709  gausslemma2dlem1a  15731  gausslemma2dlem2  15735  gausslemma2dlem5  15739  gausslemma2dlem6  15740  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  2lgslem1  15764  2sqlem3  15790  nnnninfen  16346  cvgcmp2nlemabs  16359  iooref1o  16361  taupi  16400