Theorem syl3anbrc 1207

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

Syntax hints:   -> wi 4   <-> wb 105   /\ w3a 1004

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

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  smores2  6459  smoiso  6467  iserd  6727  erinxp  6777  resixp  6901  netap  7472  2omotaplemap  7475  prarloc  7722  eluzmn  9761  eluzuzle  9763  uztrn  9772  nn0pzuz  9820  nn0ge2m1nnALT  9851  ige2m1fz  10344  0elfz  10352  uzsubfz0  10363  elfzmlbm  10365  difelfzle  10368  difelfznle  10369  elfzolt2b  10393  elfzolt3b  10394  elfzouz2  10396  fzossrbm1  10409  elfzo0  10420  eluzgtdifelfzo  10441  elfzodifsumelfzo  10445  fzonn0p1  10455  fzonn0p1p1  10457  elfzom1p1elfzo  10458  fzo0sn0fzo1  10465  ssfzo12bi  10469  ubmelm1fzo  10470  elfzonelfzo  10474  fzosplitprm1  10479  fzostep1  10482  fvinim0ffz  10486  suprzubdc  10495  zsupssdc  10497  flqword2  10548  modfzo0difsn  10656  modsumfzodifsn  10657  uzennn  10697  seq3split  10749  iseqf1olemkle  10758  iseqf1olemklt  10759  iseqf1olemqk  10768  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  bcval5  11024  1elfz0hash  11069  seq3coll  11105  ccatrn  11185  ccat2s1fvwd  11223  pfxn0  11268  pfxtrcfv0  11274  pfxtrcfvl  11277  swrdswrd  11285  swrdccatin1  11305  pfxccat3  11314  pfxccat3a  11318  cats1fvd  11346  seq3shft  11398  resqrexlemoverl  11581  fsum3cvg3  11956  fisumrev2  12006  isumshft  12050  cvgratnnlemseq  12086  cvgratnnlemabsle  12087  cvgratnnlemsumlt  12088  cvgratz  12092  sinbnd2  12314  cosbnd2  12315  sinltxirr  12321  cos12dec  12328  nn0o  12467  bitsfzolem  12514  bitsfzo  12515  bitsmod  12516  bitsfi  12517  bitsinv1lem  12521  bitsinv1  12522  uzwodc  12607  dvdsnprmd  12696  eulerthlema  12801  hashgcdlem  12809  prm23lt5  12835  prm23ge5  12836  zgz  12945  gznegcl  12947  gzcjcl  12948  gzaddcl  12949  gzmulcl  12950  nninfdclemcl  13068  nninfdclemp1  13070  nninfdclemlt  13071  unbendc  13074  strleund  13185  gsumfzz  13577  gsumfzcl  13581  subgid  13761  issubg2m  13775  subsubg  13783  gsumfzreidx  13923  gsumfzsubmcl  13924  gsumfzmptfidmadd  13925  gsumfzmhm  13929  isrngd  13965  ringrng  14048  isringd  14053  ringsrg  14059  subrngid  14214  subrngsubg  14217  issubrng2  14223  subsubrng  14227  subrgsubg  14240  islmodd  14306  dflidl2rng  14494  rnglidlrng  14511  rng2idlsubrng  14530  gsumfzfsum  14601  znidomb  14671  plyaddlem1  15470  sin0pilem1  15504  sin0pilem2  15505  cosq14gt0  15555  cosq23lt0  15556  coseq0q4123  15557  coseq00topi  15558  coseq0negpitopi  15559  tangtx  15561  cosordlem  15572  cosq34lt1  15573  cos02pilt1  15574  cos0pilt1  15575  rplogbval  15668  lgsdilem2  15764  gausslemma2dlem1a  15786  gausslemma2dlem2  15790  gausslemma2dlem5  15794  gausslemma2dlem6  15795  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  2lgslem1  15819  2sqlem3  15845  umgr2cwwkdifex  16275  trlsegvdeglem6  16315  nnnninfen  16623  cvgcmp2nlemabs  16636  iooref1o  16638  taupi  16677  gsumgfsumlem  16683  gsumgfsum  16684