Theorem syl3anbrc 1183

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 1179	. 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 980

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 982

This theorem is referenced by:  smores2  6349  smoiso  6357  iserd  6615  erinxp  6665  resixp  6789  netap  7316  2omotaplemap  7319  prarloc  7565  eluzuzle  9603  uztrn  9612  nn0pzuz  9655  nn0ge2m1nnALT  9686  ige2m1fz  10179  0elfz  10187  uzsubfz0  10198  elfzmlbm  10200  difelfzle  10203  difelfznle  10204  elfzolt2b  10228  elfzolt3b  10229  elfzouz2  10231  fzossrbm1  10243  elfzo0  10252  eluzgtdifelfzo  10267  elfzodifsumelfzo  10271  fzonn0p1  10281  fzonn0p1p1  10283  elfzom1p1elfzo  10284  fzo0sn0fzo1  10291  ssfzo12bi  10295  ubmelm1fzo  10296  elfzonelfzo  10300  fzosplitprm1  10304  fzostep1  10307  fvinim0ffz  10311  flqword2  10361  modfzo0difsn  10469  modsumfzodifsn  10470  uzennn  10510  seq3split  10562  iseqf1olemkle  10571  iseqf1olemklt  10572  iseqf1olemqk  10581  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  bcval5  10837  1elfz0hash  10880  seq3coll  10916  seq3shft  10985  resqrexlemoverl  11168  fsum3cvg3  11542  fisumrev2  11592  isumshft  11636  cvgratnnlemseq  11672  cvgratnnlemabsle  11673  cvgratnnlemsumlt  11674  cvgratz  11678  sinbnd2  11900  cosbnd2  11901  sinltxirr  11907  cos12dec  11914  nn0o  12051  suprzubdc  12092  zsupssdc  12094  uzwodc  12177  dvdsnprmd  12266  eulerthlema  12371  hashgcdlem  12379  prm23lt5  12404  prm23ge5  12405  zgz  12514  gznegcl  12516  gzcjcl  12517  gzaddcl  12518  gzmulcl  12519  nninfdclemcl  12608  nninfdclemp1  12610  nninfdclemlt  12611  unbendc  12614  strleund  12724  gsumfzz  13070  gsumfzcl  13074  subgid  13248  issubg2m  13262  subsubg  13270  gsumfzreidx  13410  gsumfzsubmcl  13411  gsumfzmptfidmadd  13412  gsumfzmhm  13416  isrngd  13452  ringrng  13535  isringd  13540  ringsrg  13546  subrngid  13700  subrngsubg  13703  issubrng2  13709  subsubrng  13713  subrgsubg  13726  islmodd  13792  dflidl2rng  13980  rnglidlrng  13997  rng2idlsubrng  14016  gsumfzfsum  14087  znidomb  14157  plyaddlem1  14926  sin0pilem1  14957  sin0pilem2  14958  cosq14gt0  15008  cosq23lt0  15009  coseq0q4123  15010  coseq00topi  15011  coseq0negpitopi  15012  tangtx  15014  cosordlem  15025  cosq34lt1  15026  cos02pilt1  15027  cos0pilt1  15028  rplogbval  15118  lgsdilem2  15193  gausslemma2dlem1a  15215  gausslemma2dlem2  15219  gausslemma2dlem5  15223  gausslemma2dlem6  15224  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  2lgslem1  15248  2sqlem3  15274  nnnninfen  15581  cvgcmp2nlemabs  15592  iooref1o  15594  taupi  15633