Theorem syl3anbrc 1184

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 1180	. 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 981

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 983

This theorem is referenced by:  smores2  6398  smoiso  6406  iserd  6664  erinxp  6714  resixp  6838  netap  7396  2omotaplemap  7399  prarloc  7646  eluzuzle  9686  uztrn  9695  nn0pzuz  9738  nn0ge2m1nnALT  9769  ige2m1fz  10262  0elfz  10270  uzsubfz0  10281  elfzmlbm  10283  difelfzle  10286  difelfznle  10287  elfzolt2b  10311  elfzolt3b  10312  elfzouz2  10314  fzossrbm1  10327  elfzo0  10338  eluzgtdifelfzo  10358  elfzodifsumelfzo  10362  fzonn0p1  10372  fzonn0p1p1  10374  elfzom1p1elfzo  10375  fzo0sn0fzo1  10382  ssfzo12bi  10386  ubmelm1fzo  10387  elfzonelfzo  10391  fzosplitprm1  10395  fzostep1  10398  fvinim0ffz  10402  suprzubdc  10411  zsupssdc  10413  flqword2  10464  modfzo0difsn  10572  modsumfzodifsn  10573  uzennn  10613  seq3split  10665  iseqf1olemkle  10674  iseqf1olemklt  10675  iseqf1olemqk  10684  seq3f1olemqsumkj  10688  seq3f1olemqsumk  10689  seq3f1olemqsum  10690  bcval5  10940  1elfz0hash  10983  seq3coll  11019  ccatrn  11098  pfxn0  11174  pfxtrcfv0  11180  pfxtrcfvl  11183  swrdswrd  11191  seq3shft  11234  resqrexlemoverl  11417  fsum3cvg3  11792  fisumrev2  11842  isumshft  11886  cvgratnnlemseq  11922  cvgratnnlemabsle  11923  cvgratnnlemsumlt  11924  cvgratz  11928  sinbnd2  12150  cosbnd2  12151  sinltxirr  12157  cos12dec  12164  nn0o  12303  bitsfzolem  12350  bitsfzo  12351  bitsmod  12352  bitsfi  12353  bitsinv1lem  12357  bitsinv1  12358  uzwodc  12443  dvdsnprmd  12532  eulerthlema  12637  hashgcdlem  12645  prm23lt5  12671  prm23ge5  12672  zgz  12781  gznegcl  12783  gzcjcl  12784  gzaddcl  12785  gzmulcl  12786  nninfdclemcl  12904  nninfdclemp1  12906  nninfdclemlt  12907  unbendc  12910  strleund  13020  gsumfzz  13412  gsumfzcl  13416  subgid  13596  issubg2m  13610  subsubg  13618  gsumfzreidx  13758  gsumfzsubmcl  13759  gsumfzmptfidmadd  13760  gsumfzmhm  13764  isrngd  13800  ringrng  13883  isringd  13888  ringsrg  13894  subrngid  14048  subrngsubg  14051  issubrng2  14057  subsubrng  14061  subrgsubg  14074  islmodd  14140  dflidl2rng  14328  rnglidlrng  14345  rng2idlsubrng  14364  gsumfzfsum  14435  znidomb  14505  plyaddlem1  15304  sin0pilem1  15338  sin0pilem2  15339  cosq14gt0  15389  cosq23lt0  15390  coseq0q4123  15391  coseq00topi  15392  coseq0negpitopi  15393  tangtx  15395  cosordlem  15406  cosq34lt1  15407  cos02pilt1  15408  cos0pilt1  15409  rplogbval  15502  lgsdilem2  15598  gausslemma2dlem1a  15620  gausslemma2dlem2  15624  gausslemma2dlem5  15628  gausslemma2dlem6  15629  lgsquadlem1  15639  lgsquadlem2  15640  lgsquadlem3  15641  2lgslem1  15653  2sqlem3  15679  nnnninfen  16130  cvgcmp2nlemabs  16143  iooref1o  16145  taupi  16184