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  11091  resqrexlemoverl  11274  fsum3cvg3  11649  fisumrev2  11699  isumshft  11743  cvgratnnlemseq  11779  cvgratnnlemabsle  11780  cvgratnnlemsumlt  11781  cvgratz  11785  sinbnd2  12007  cosbnd2  12008  sinltxirr  12014  cos12dec  12021  nn0o  12160  bitsfzolem  12207  bitsfzo  12208  bitsmod  12209  bitsfi  12210  bitsinv1lem  12214  bitsinv1  12215  uzwodc  12300  dvdsnprmd  12389  eulerthlema  12494  hashgcdlem  12502  prm23lt5  12528  prm23ge5  12529  zgz  12638  gznegcl  12640  gzcjcl  12641  gzaddcl  12642  gzmulcl  12643  nninfdclemcl  12761  nninfdclemp1  12763  nninfdclemlt  12764  unbendc  12767  strleund  12877  gsumfzz  13269  gsumfzcl  13273  subgid  13453  issubg2m  13467  subsubg  13475  gsumfzreidx  13615  gsumfzsubmcl  13616  gsumfzmptfidmadd  13617  gsumfzmhm  13621  isrngd  13657  ringrng  13740  isringd  13745  ringsrg  13751  subrngid  13905  subrngsubg  13908  issubrng2  13914  subsubrng  13918  subrgsubg  13931  islmodd  13997  dflidl2rng  14185  rnglidlrng  14202  rng2idlsubrng  14221  gsumfzfsum  14292  znidomb  14362  plyaddlem1  15161  sin0pilem1  15195  sin0pilem2  15196  cosq14gt0  15246  cosq23lt0  15247  coseq0q4123  15248  coseq00topi  15249  coseq0negpitopi  15250  tangtx  15252  cosordlem  15263  cosq34lt1  15264  cos02pilt1  15265  cos0pilt1  15266  rplogbval  15359  lgsdilem2  15455  gausslemma2dlem1a  15477  gausslemma2dlem2  15481  gausslemma2dlem5  15485  gausslemma2dlem6  15486  lgsquadlem1  15496  lgsquadlem2  15497  lgsquadlem3  15498  2lgslem1  15510  2sqlem3  15536  nnnninfen  15891  cvgcmp2nlemabs  15904  iooref1o  15906  taupi  15945