Theorem syl3anbrc 1128

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 1124	. 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 925

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

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

This theorem is referenced by:  smores2  6073  smoiso  6081  iserd  6332  xpiderm  6377  erinxp  6380  resixp  6504  prarloc  7116  eluzuzle  9081  uztrn  9089  nn0pzuz  9129  nn0ge2m1nnALT  9157  ige2m1fz  9578  0elfz  9586  uzsubfz0  9594  elfzmlbm  9596  difelfzle  9599  difelfznle  9600  elfzolt2b  9623  elfzolt3b  9624  elfzouz2  9626  fzossrbm1  9638  elfzo0  9647  eluzgtdifelfzo  9662  elfzodifsumelfzo  9666  fzonn0p1  9676  fzonn0p1p1  9678  elfzom1p1elfzo  9679  fzo0sn0fzo1  9686  ssfzo12bi  9690  ubmelm1fzo  9691  elfzonelfzo  9695  fzosplitprm1  9699  fzostep1  9702  fvinim0ffz  9706  flqword2  9750  modfzo0difsn  9856  modsumfzodifsn  9857  seq3split  9961  iseqf1olemkle  9967  iseqf1olemklt  9968  iseqf1olemqk  9977  seq3f1olemqsumkj  9981  seq3f1olemqsumk  9982  seq3f1olemqsum  9983  ibcval5  10225  1elfz0hash  10268  iseqcoll  10301  seq3shft  10326  resqrexlemoverl  10508  fsum3cvg3  10843  fisumrev2  10894  isumshft  10938  cvgratnnlemseq  10974  cvgratnnlemabsle  10975  cvgratnnlemsumlt  10976  cvgratz  10980  sinbnd2  11099  cosbnd2  11100  nn0o  11239  dvdsnprmd  11439  hashgcdlem  11535  strleund  11636