Theorem syl3anbrc 1212

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  smores2  6570  smoiso  6578  iserd  6838  erinxp  6888  resixp  7021  netap  7626  2omotaplemap  7629  prarloc  7876  eluzmn  9943  eluzuzle  9945  uztrn  9954  nn0pzuz  10002  nn0ge2m1nnALT  10033  ige2m1fz  10533  0elfz  10541  uzsubfz0  10552  elfzmlbm  10554  difelfzle  10557  difelfznle  10558  elfzolt2b  10582  elfzolt3b  10583  elfzouz2  10585  fzossrbm1  10598  elfzo0  10609  eluzgtdifelfzo  10631  elfzodifsumelfzo  10635  fzonn0p1  10645  fzonn0p1p1  10647  elfzom1p1elfzo  10648  fzo0sn0fzo1  10655  ssfzo12bi  10659  ubmelm1fzo  10660  elfzonelfzo  10664  fzosplitprm1  10669  fzostep1  10672  fvinim0ffz  10676  suprzubdc  10687  zsupssdc  10689  flqword2  10744  modfzo0difsn  10852  modsumfzodifsn  10853  uzennn  10893  seq3split  10945  iseqf1olemkle  10954  iseqf1olemklt  10955  iseqf1olemqk  10964  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  bcval5  11222  bcm1n  11228  1elfz0hash  11268  seq3coll  11315  ccatrn  11398  ccat2s1fvwd  11436  pfxn0  11481  pfxtrcfv0  11487  pfxtrcfvl  11490  swrdswrd  11498  swrdccatin1  11518  pfxccat3  11527  pfxccat3a  11531  cats1fvd  11559  seq3shft  11624  resqrexlemoverl  11808  fsum3cvg3  12187  fisumrev2  12237  isumshft  12281  cvgratnnlemseq  12317  cvgratnnlemabsle  12318  cvgratnnlemsumlt  12319  cvgratz  12323  sinbnd2  12545  cosbnd2  12546  sinltxirr  12552  cos12dec  12559  nn0o  12698  bitsfzolem  12745  bitsfzo  12746  bitsmod  12747  bitsfi  12748  bitsinv1lem  12752  bitsinv1  12753  uzwodc  12838  dvdsnprmd  12927  eulerthlema  13036  hashgcdlem  13044  prm23lt5  13070  prm23ge5  13071  zgz  13180  gznegcl  13182  gzcjcl  13183  gzaddcl  13184  gzmulcl  13185  ballotfilemsel1i  13313  ballotfilemro  13323  ballotfilemfrceq  13329  nninfdclemcl  13396  nninfdclemp1  13398  nninfdclemlt  13399  unbendc  13402  strleund  13515  gzsumcl  13862  subgid  14036  issubg2m  14050  subsubg  14058  gzsumreidx  14230  gzsumsubmcl  14231  gzsummhm  14234  gzsumsplit0  14237  gzsumshift  14238  gzsumgsum  14244  isrngd  14358  ringrng  14447  isringd  14452  ringsrg  14458  subrngid  14617  subrngsubg  14620  issubrng2  14626  subsubrng  14630  subrgsubg  14643  islmodd  14737  dflidl2rng  14926  rnglidlrng  14943  rng2idlsubrng  14962  znidomb  15101  plyaddlem1  15990  sin0pilem1  16025  sin0pilem2  16026  cosq14gt0  16076  cosq23lt0  16077  coseq0q4123  16078  coseq00topi  16079  coseq0negpitopi  16080  tangtx  16082  cosordlem  16094  cosq34lt1  16095  cos02pilt1  16096  cos0pilt1  16097  rplogbval  16198  ppiqsval  16257  chtdif  16281  ppidif  16286  ppiqub  16310  chtublem  16312  chtqub  16313  bposlem4  16331  lgsdilem2  16377  gausslemma2dlem1a  16399  gausslemma2dlem2  16403  gausslemma2dlem5  16407  gausslemma2dlem6  16408  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  2lgslem1  16432  2sqlem3  16458  umgr2cwwkdifex  16888  trlsegvdeglem6  16928  depindlem2  16970  nnnninfen  17287  repiecelem  17297  repiecele0  17298  repiecege0  17299  cvgcmp2nlemabs  17304  iooref1o  17306  taupi  17347