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  6569  smoiso  6577  iserd  6837  erinxp  6887  resixp  7019  netap  7626  2omotaplemap  7629  prarloc  7876  eluzmn  9944  eluzuzle  9946  uztrn  9955  nn0pzuz  10003  nn0ge2m1nnALT  10034  ige2m1fz  10534  0elfz  10542  uzsubfz0  10553  elfzmlbm  10555  difelfzle  10558  difelfznle  10559  elfzolt2b  10583  elfzolt3b  10584  elfzouz2  10586  fzossrbm1  10599  elfzo0  10610  eluzgtdifelfzo  10632  elfzodifsumelfzo  10636  fzonn0p1  10646  fzonn0p1p1  10648  elfzom1p1elfzo  10649  fzo0sn0fzo1  10656  ssfzo12bi  10660  ubmelm1fzo  10661  elfzonelfzo  10665  fzosplitprm1  10670  fzostep1  10673  fvinim0ffz  10677  suprzubdc  10688  zsupssdc  10690  flqword2  10745  modfzo0difsn  10853  modsumfzodifsn  10854  uzennn  10894  seq3split  10946  iseqf1olemkle  10955  iseqf1olemklt  10956  iseqf1olemqk  10965  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  bcval5  11223  bcm1n  11229  1elfz0hash  11269  seq3coll  11316  ccatrn  11399  ccat2s1fvwd  11437  pfxn0  11482  pfxtrcfv0  11488  pfxtrcfvl  11491  swrdswrd  11499  swrdccatin1  11519  pfxccat3  11528  pfxccat3a  11532  cats1fvd  11560  seq3shft  11625  resqrexlemoverl  11809  fsum3cvg3  12188  fisumrev2  12238  isumshft  12282  cvgratnnlemseq  12318  cvgratnnlemabsle  12319  cvgratnnlemsumlt  12320  cvgratz  12324  sinbnd2  12546  cosbnd2  12547  sinltxirr  12553  cos12dec  12560  nn0o  12699  bitsfzolem  12746  bitsfzo  12747  bitsmod  12748  bitsfi  12749  bitsinv1lem  12753  bitsinv1  12754  uzwodc  12839  dvdsnprmd  12928  eulerthlema  13037  hashgcdlem  13045  prm23lt5  13071  prm23ge5  13072  zgz  13181  gznegcl  13183  gzcjcl  13184  gzaddcl  13185  gzmulcl  13186  ballotfilemsel1i  13314  ballotfilemro  13324  ballotfilemfrceq  13330  nninfdclemcl  13397  nninfdclemp1  13399  nninfdclemlt  13400  unbendc  13403  strleund  13516  gzsumcl  13863  subgid  14037  issubg2m  14051  subsubg  14059  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  gzsumsplit0  14238  gzsumshift  14239  gzsumgsum  14245  isrngd  14359  ringrng  14448  isringd  14453  ringsrg  14459  subrngid  14618  subrngsubg  14621  issubrng2  14627  subsubrng  14631  subrgsubg  14644  islmodd  14738  dflidl2rng  14927  rnglidlrng  14944  rng2idlsubrng  14963  znidomb  15102  plyaddlem1  15973  sin0pilem1  16008  sin0pilem2  16009  cosq14gt0  16059  cosq23lt0  16060  coseq0q4123  16061  coseq00topi  16062  coseq0negpitopi  16063  tangtx  16065  cosordlem  16077  cosq34lt1  16078  cos02pilt1  16079  cos0pilt1  16080  rplogbval  16181  ppiqsval  16240  chtdif  16264  ppidif  16269  ppiqub  16293  chtublem  16295  chtqub  16296  bposlem4  16314  lgsdilem2  16360  gausslemma2dlem1a  16382  gausslemma2dlem2  16386  gausslemma2dlem5  16390  gausslemma2dlem6  16391  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  2lgslem1  16415  2sqlem3  16441  umgr2cwwkdifex  16871  trlsegvdeglem6  16911  depindlem2  16953  nnnninfen  17270  repiecelem  17280  repiecele0  17281  repiecege0  17282  cvgcmp2nlemabs  17287  iooref1o  17289  taupi  17330