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  6199  smoiso  6207  iserd  6463  erinxp  6511  resixp  6635  prarloc  7335  eluzuzle  9358  uztrn  9366  nn0pzuz  9409  nn0ge2m1nnALT  9437  ige2m1fz  9921  0elfz  9929  uzsubfz0  9937  elfzmlbm  9939  difelfzle  9942  difelfznle  9943  elfzolt2b  9966  elfzolt3b  9967  elfzouz2  9969  fzossrbm1  9981  elfzo0  9990  eluzgtdifelfzo  10005  elfzodifsumelfzo  10009  fzonn0p1  10019  fzonn0p1p1  10021  elfzom1p1elfzo  10022  fzo0sn0fzo1  10029  ssfzo12bi  10033  ubmelm1fzo  10034  elfzonelfzo  10038  fzosplitprm1  10042  fzostep1  10045  fvinim0ffz  10049  flqword2  10093  modfzo0difsn  10199  modsumfzodifsn  10200  uzennn  10240  seq3split  10283  iseqf1olemkle  10288  iseqf1olemklt  10289  iseqf1olemqk  10298  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  bcval5  10541  1elfz0hash  10584  seq3coll  10617  seq3shft  10642  resqrexlemoverl  10825  fsum3cvg3  11197  fisumrev2  11247  isumshft  11291  cvgratnnlemseq  11327  cvgratnnlemabsle  11328  cvgratnnlemsumlt  11329  cvgratz  11333  sinbnd2  11497  cosbnd2  11498  cos12dec  11510  nn0o  11640  dvdsnprmd  11842  hashgcdlem  11939  strleund  12086  sin0pilem1  12910  sin0pilem2  12911  cosq14gt0  12961  cosq23lt0  12962  coseq0q4123  12963  coseq00topi  12964  coseq0negpitopi  12965  tangtx  12967  cosordlem  12978  cosq34lt1  12979  cos02pilt1  12980  cos0pilt1  12981  rplogbval  13070  cvgcmp2nlemabs  13402  iooref1o  13426  taupi  13430