Theorem syl3anbrc 1205

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 1201	. 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 1002

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 1004

This theorem is referenced by:  smores2  6446  smoiso  6454  iserd  6714  erinxp  6764  resixp  6888  netap  7451  2omotaplemap  7454  prarloc  7701  eluzmn  9740  eluzuzle  9742  uztrn  9751  nn0pzuz  9794  nn0ge2m1nnALT  9825  ige2m1fz  10318  0elfz  10326  uzsubfz0  10337  elfzmlbm  10339  difelfzle  10342  difelfznle  10343  elfzolt2b  10367  elfzolt3b  10368  elfzouz2  10370  fzossrbm1  10383  elfzo0  10394  eluzgtdifelfzo  10415  elfzodifsumelfzo  10419  fzonn0p1  10429  fzonn0p1p1  10431  elfzom1p1elfzo  10432  fzo0sn0fzo1  10439  ssfzo12bi  10443  ubmelm1fzo  10444  elfzonelfzo  10448  fzosplitprm1  10452  fzostep1  10455  fvinim0ffz  10459  suprzubdc  10468  zsupssdc  10470  flqword2  10521  modfzo0difsn  10629  modsumfzodifsn  10630  uzennn  10670  seq3split  10722  iseqf1olemkle  10731  iseqf1olemklt  10732  iseqf1olemqk  10741  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  bcval5  10997  1elfz0hash  11041  seq3coll  11077  ccatrn  11157  pfxn0  11235  pfxtrcfv0  11241  pfxtrcfvl  11244  swrdswrd  11252  swrdccatin1  11272  pfxccat3  11281  pfxccat3a  11285  cats1fvd  11313  seq3shft  11364  resqrexlemoverl  11547  fsum3cvg3  11922  fisumrev2  11972  isumshft  12016  cvgratnnlemseq  12052  cvgratnnlemabsle  12053  cvgratnnlemsumlt  12054  cvgratz  12058  sinbnd2  12280  cosbnd2  12281  sinltxirr  12287  cos12dec  12294  nn0o  12433  bitsfzolem  12480  bitsfzo  12481  bitsmod  12482  bitsfi  12483  bitsinv1lem  12487  bitsinv1  12488  uzwodc  12573  dvdsnprmd  12662  eulerthlema  12767  hashgcdlem  12775  prm23lt5  12801  prm23ge5  12802  zgz  12911  gznegcl  12913  gzcjcl  12914  gzaddcl  12915  gzmulcl  12916  nninfdclemcl  13034  nninfdclemp1  13036  nninfdclemlt  13037  unbendc  13040  strleund  13151  gsumfzz  13543  gsumfzcl  13547  subgid  13727  issubg2m  13741  subsubg  13749  gsumfzreidx  13889  gsumfzsubmcl  13890  gsumfzmptfidmadd  13891  gsumfzmhm  13895  isrngd  13931  ringrng  14014  isringd  14019  ringsrg  14025  subrngid  14180  subrngsubg  14183  issubrng2  14189  subsubrng  14193  subrgsubg  14206  islmodd  14272  dflidl2rng  14460  rnglidlrng  14477  rng2idlsubrng  14496  gsumfzfsum  14567  znidomb  14637  plyaddlem1  15436  sin0pilem1  15470  sin0pilem2  15471  cosq14gt0  15521  cosq23lt0  15522  coseq0q4123  15523  coseq00topi  15524  coseq0negpitopi  15525  tangtx  15527  cosordlem  15538  cosq34lt1  15539  cos02pilt1  15540  cos0pilt1  15541  rplogbval  15634  lgsdilem2  15730  gausslemma2dlem1a  15752  gausslemma2dlem2  15756  gausslemma2dlem5  15760  gausslemma2dlem6  15761  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  2lgslem1  15785  2sqlem3  15811  nnnninfen  16447  cvgcmp2nlemabs  16460  iooref1o  16462  taupi  16501