Theorem syl3anbrc 1165

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 1161	. 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 962

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 964

This theorem is referenced by:  smores2  6191  smoiso  6199  iserd  6455  erinxp  6503  resixp  6627  prarloc  7311  eluzuzle  9334  uztrn  9342  nn0pzuz  9382  nn0ge2m1nnALT  9410  ige2m1fz  9890  0elfz  9898  uzsubfz0  9906  elfzmlbm  9908  difelfzle  9911  difelfznle  9912  elfzolt2b  9935  elfzolt3b  9936  elfzouz2  9938  fzossrbm1  9950  elfzo0  9959  eluzgtdifelfzo  9974  elfzodifsumelfzo  9978  fzonn0p1  9988  fzonn0p1p1  9990  elfzom1p1elfzo  9991  fzo0sn0fzo1  9998  ssfzo12bi  10002  ubmelm1fzo  10003  elfzonelfzo  10007  fzosplitprm1  10011  fzostep1  10014  fvinim0ffz  10018  flqword2  10062  modfzo0difsn  10168  modsumfzodifsn  10169  uzennn  10209  seq3split  10252  iseqf1olemkle  10257  iseqf1olemklt  10258  iseqf1olemqk  10267  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3f1olemqsum  10273  bcval5  10509  1elfz0hash  10552  seq3coll  10585  seq3shft  10610  resqrexlemoverl  10793  fsum3cvg3  11165  fisumrev2  11215  isumshft  11259  cvgratnnlemseq  11295  cvgratnnlemabsle  11296  cvgratnnlemsumlt  11297  cvgratz  11301  sinbnd2  11461  cosbnd2  11462  cos12dec  11474  nn0o  11604  dvdsnprmd  11806  hashgcdlem  11903  strleund  12047  sin0pilem1  12862  sin0pilem2  12863  cosq14gt0  12913  cosq23lt0  12914  coseq0q4123  12915  coseq00topi  12916  coseq0negpitopi  12917  tangtx  12919  cosordlem  12930  cosq34lt1  12931  cos02pilt1  12932  cvgcmp2nlemabs  13227  taupi  13239