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  6565  smoiso  6573  iserd  6833  erinxp  6883  resixp  7015  netap  7621  2omotaplemap  7624  prarloc  7871  eluzmn  9938  eluzuzle  9940  uztrn  9949  nn0pzuz  9997  nn0ge2m1nnALT  10028  ige2m1fz  10528  0elfz  10536  uzsubfz0  10547  elfzmlbm  10549  difelfzle  10552  difelfznle  10553  elfzolt2b  10577  elfzolt3b  10578  elfzouz2  10580  fzossrbm1  10593  elfzo0  10604  eluzgtdifelfzo  10626  elfzodifsumelfzo  10630  fzonn0p1  10640  fzonn0p1p1  10642  elfzom1p1elfzo  10643  fzo0sn0fzo1  10650  ssfzo12bi  10654  ubmelm1fzo  10655  elfzonelfzo  10659  fzosplitprm1  10664  fzostep1  10667  fvinim0ffz  10671  suprzubdc  10682  zsupssdc  10684  flqword2  10739  modfzo0difsn  10847  modsumfzodifsn  10848  uzennn  10888  seq3split  10940  iseqf1olemkle  10949  iseqf1olemklt  10950  iseqf1olemqk  10959  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  bcval5  11217  bcm1n  11223  1elfz0hash  11263  seq3coll  11310  ccatrn  11393  ccat2s1fvwd  11431  pfxn0  11476  pfxtrcfv0  11482  pfxtrcfvl  11485  swrdswrd  11493  swrdccatin1  11513  pfxccat3  11522  pfxccat3a  11526  cats1fvd  11554  seq3shft  11619  resqrexlemoverl  11803  fsum3cvg3  12182  fisumrev2  12232  isumshft  12276  cvgratnnlemseq  12312  cvgratnnlemabsle  12313  cvgratnnlemsumlt  12314  cvgratz  12318  sinbnd2  12540  cosbnd2  12541  sinltxirr  12547  cos12dec  12554  nn0o  12693  bitsfzolem  12740  bitsfzo  12741  bitsmod  12742  bitsfi  12743  bitsinv1lem  12747  bitsinv1  12748  uzwodc  12833  dvdsnprmd  12922  eulerthlema  13031  hashgcdlem  13039  prm23lt5  13065  prm23ge5  13066  zgz  13175  gznegcl  13177  gzcjcl  13178  gzaddcl  13179  gzmulcl  13180  ballotfilemsel1i  13308  ballotfilemro  13318  ballotfilemfrceq  13324  nninfdclemcl  13391  nninfdclemp1  13393  nninfdclemlt  13394  unbendc  13397  strleund  13510  gzsumcl  13857  subgid  14031  issubg2m  14045  subsubg  14053  gzsumreidx  14225  gzsumsubmcl  14226  gzsummhm  14229  gzsumsplit0  14232  gzsumshift  14233  gzsumgsum  14239  isrngd  14336  ringrng  14425  isringd  14430  ringsrg  14436  subrngid  14593  subrngsubg  14596  issubrng2  14602  subsubrng  14606  subrgsubg  14619  islmodd  14713  dflidl2rng  14902  rnglidlrng  14919  rng2idlsubrng  14938  znidomb  15077  plyaddlem1  15939  sin0pilem1  15974  sin0pilem2  15975  cosq14gt0  16025  cosq23lt0  16026  coseq0q4123  16027  coseq00topi  16028  coseq0negpitopi  16029  tangtx  16031  cosordlem  16042  cosq34lt1  16043  cos02pilt1  16044  cos0pilt1  16045  rplogbval  16142  ppiqsval  16201  chtdif  16225  ppidif  16230  ppiqub  16254  chtublem  16256  chtqub  16257  bposlem4  16275  lgsdilem2  16321  gausslemma2dlem1a  16343  gausslemma2dlem2  16347  gausslemma2dlem5  16351  gausslemma2dlem6  16352  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  2lgslem1  16376  2sqlem3  16402  umgr2cwwkdifex  16832  trlsegvdeglem6  16872  depindlem2  16914  nnnninfen  17230  repiecelem  17240  repiecele0  17241  repiecege0  17242  cvgcmp2nlemabs  17247  iooref1o  17249  taupi  17290