Theorem syl3anbrc 1166

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 1162	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
5		syl3anbrc.4	. 2 |- ( ta <-> ( ps /\ ch /\ th ) )
6	4, 5	sylibr 133	1 |- ( ph -> ta )

Syntax hints:   -> wi 4   <-> wb 104   /\ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  smores2  6244  smoiso  6252  iserd  6509  erinxp  6557  resixp  6681  prarloc  7426  eluzuzle  9453  uztrn  9461  nn0pzuz  9504  nn0ge2m1nnALT  9534  ige2m1fz  10019  0elfz  10027  uzsubfz0  10038  elfzmlbm  10040  difelfzle  10043  difelfznle  10044  elfzolt2b  10067  elfzolt3b  10068  elfzouz2  10070  fzossrbm1  10082  elfzo0  10091  eluzgtdifelfzo  10106  elfzodifsumelfzo  10110  fzonn0p1  10120  fzonn0p1p1  10122  elfzom1p1elfzo  10123  fzo0sn0fzo1  10130  ssfzo12bi  10134  ubmelm1fzo  10135  elfzonelfzo  10139  fzosplitprm1  10143  fzostep1  10146  fvinim0ffz  10150  flqword2  10198  modfzo0difsn  10304  modsumfzodifsn  10305  uzennn  10345  seq3split  10388  iseqf1olemkle  10393  iseqf1olemklt  10394  iseqf1olemqk  10403  seq3f1olemqsumkj  10407  seq3f1olemqsumk  10408  seq3f1olemqsum  10409  bcval5  10649  1elfz0hash  10692  seq3coll  10725  seq3shft  10750  resqrexlemoverl  10933  fsum3cvg3  11305  fisumrev2  11355  isumshft  11399  cvgratnnlemseq  11435  cvgratnnlemabsle  11436  cvgratnnlemsumlt  11437  cvgratz  11441  sinbnd2  11663  cosbnd2  11664  cos12dec  11676  nn0o  11811  suprzubdc  11852  zsupssdc  11854  dvdsnprmd  12018  eulerthlema  12121  hashgcdlem  12129  prm23lt5  12154  prm23ge5  12155  nninfdclemcl  12275  nninfdclemp1  12277  nninfdclemlt  12278  unbendc  12281  strleund  12374  sin0pilem1  13198  sin0pilem2  13199  cosq14gt0  13249  cosq23lt0  13250  coseq0q4123  13251  coseq00topi  13252  coseq0negpitopi  13253  tangtx  13255  cosordlem  13266  cosq34lt1  13267  cos02pilt1  13268  cos0pilt1  13269  rplogbval  13359  cvgcmp2nlemabs  13700  iooref1o  13702  taupi  13738