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  6379  smoiso  6387  iserd  6645  erinxp  6695  resixp  6819  netap  7365  2omotaplemap  7368  prarloc  7615  eluzuzle  9655  uztrn  9664  nn0pzuz  9707  nn0ge2m1nnALT  9738  ige2m1fz  10231  0elfz  10239  uzsubfz0  10250  elfzmlbm  10252  difelfzle  10255  difelfznle  10256  elfzolt2b  10280  elfzolt3b  10281  elfzouz2  10283  fzossrbm1  10295  elfzo0  10304  eluzgtdifelfzo  10324  elfzodifsumelfzo  10328  fzonn0p1  10338  fzonn0p1p1  10340  elfzom1p1elfzo  10341  fzo0sn0fzo1  10348  ssfzo12bi  10352  ubmelm1fzo  10353  elfzonelfzo  10357  fzosplitprm1  10361  fzostep1  10364  fvinim0ffz  10368  suprzubdc  10377  zsupssdc  10379  flqword2  10430  modfzo0difsn  10538  modsumfzodifsn  10539  uzennn  10579  seq3split  10631  iseqf1olemkle  10640  iseqf1olemklt  10641  iseqf1olemqk  10650  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seq3f1olemqsum  10656  bcval5  10906  1elfz0hash  10949  seq3coll  10985  ccatrn  11063  seq3shft  11120  resqrexlemoverl  11303  fsum3cvg3  11678  fisumrev2  11728  isumshft  11772  cvgratnnlemseq  11808  cvgratnnlemabsle  11809  cvgratnnlemsumlt  11810  cvgratz  11814  sinbnd2  12036  cosbnd2  12037  sinltxirr  12043  cos12dec  12050  nn0o  12189  bitsfzolem  12236  bitsfzo  12237  bitsmod  12238  bitsfi  12239  bitsinv1lem  12243  bitsinv1  12244  uzwodc  12329  dvdsnprmd  12418  eulerthlema  12523  hashgcdlem  12531  prm23lt5  12557  prm23ge5  12558  zgz  12667  gznegcl  12669  gzcjcl  12670  gzaddcl  12671  gzmulcl  12672  nninfdclemcl  12790  nninfdclemp1  12792  nninfdclemlt  12793  unbendc  12796  strleund  12906  gsumfzz  13298  gsumfzcl  13302  subgid  13482  issubg2m  13496  subsubg  13504  gsumfzreidx  13644  gsumfzsubmcl  13645  gsumfzmptfidmadd  13646  gsumfzmhm  13650  isrngd  13686  ringrng  13769  isringd  13774  ringsrg  13780  subrngid  13934  subrngsubg  13937  issubrng2  13943  subsubrng  13947  subrgsubg  13960  islmodd  14026  dflidl2rng  14214  rnglidlrng  14231  rng2idlsubrng  14250  gsumfzfsum  14321  znidomb  14391  plyaddlem1  15190  sin0pilem1  15224  sin0pilem2  15225  cosq14gt0  15275  cosq23lt0  15276  coseq0q4123  15277  coseq00topi  15278  coseq0negpitopi  15279  tangtx  15281  cosordlem  15292  cosq34lt1  15293  cos02pilt1  15294  cos0pilt1  15295  rplogbval  15388  lgsdilem2  15484  gausslemma2dlem1a  15506  gausslemma2dlem2  15510  gausslemma2dlem5  15514  gausslemma2dlem6  15515  lgsquadlem1  15525  lgsquadlem2  15526  lgsquadlem3  15527  2lgslem1  15539  2sqlem3  15565  nnnninfen  15920  cvgcmp2nlemabs  15933  iooref1o  15935  taupi  15974