Theorem syl3anbrc 1122

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

Syntax hints:   -> wi 4   <-> wb 103   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  smores2  5932  smoiso  5940  iserd  6155  xpiderm  6200  erinxp  6203  prarloc  6693  eluzuzle  8627  uztrn  8635  nn0pzuz  8675  nn0ge2m1nnALT  8703  ige2m1fz  9127  0elfz  9132  uzsubfz0  9140  elfzmlbm  9142  difelfzle  9145  difelfznle  9146  elfzolt2b  9167  elfzolt3b  9168  elfzouz2  9170  fzossrbm1  9182  elfzo0  9191  eluzgtdifelfzo  9206  elfzodifsumelfzo  9210  fzonn0p1  9220  fzonn0p1p1  9222  elfzom1p1elfzo  9223  fzo0sn0fzo1  9230  ssfzo12bi  9234  ubmelm1fzo  9235  elfzonelfzo  9239  fzosplitprm1  9243  fzostep1  9246  fvinim0ffz  9250  flqword2  9291  modfzo0difsn  9397  modsumfzodifsn  9398  ibcval5  9690  resqrexlemoverl  9907  nn0o  10307  dvdsnprmd  10507