Theorem syl3anbrc 1181

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 1177	. 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 978

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 980

This theorem is referenced by:  smores2  6294  smoiso  6302  iserd  6560  erinxp  6608  resixp  6732  netap  7252  2omotaplemap  7255  prarloc  7501  eluzuzle  9535  uztrn  9543  nn0pzuz  9586  nn0ge2m1nnALT  9617  ige2m1fz  10109  0elfz  10117  uzsubfz0  10128  elfzmlbm  10130  difelfzle  10133  difelfznle  10134  elfzolt2b  10157  elfzolt3b  10158  elfzouz2  10160  fzossrbm1  10172  elfzo0  10181  eluzgtdifelfzo  10196  elfzodifsumelfzo  10200  fzonn0p1  10210  fzonn0p1p1  10212  elfzom1p1elfzo  10213  fzo0sn0fzo1  10220  ssfzo12bi  10224  ubmelm1fzo  10225  elfzonelfzo  10229  fzosplitprm1  10233  fzostep1  10236  fvinim0ffz  10240  flqword2  10288  modfzo0difsn  10394  modsumfzodifsn  10395  uzennn  10435  seq3split  10478  iseqf1olemkle  10483  iseqf1olemklt  10484  iseqf1olemqk  10493  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  bcval5  10742  1elfz0hash  10785  seq3coll  10821  seq3shft  10846  resqrexlemoverl  11029  fsum3cvg3  11403  fisumrev2  11453  isumshft  11497  cvgratnnlemseq  11533  cvgratnnlemabsle  11534  cvgratnnlemsumlt  11535  cvgratz  11539  sinbnd2  11761  cosbnd2  11762  cos12dec  11774  nn0o  11911  suprzubdc  11952  zsupssdc  11954  uzwodc  12037  dvdsnprmd  12124  eulerthlema  12229  hashgcdlem  12237  prm23lt5  12262  prm23ge5  12263  zgz  12370  gznegcl  12372  gzcjcl  12373  gzaddcl  12374  gzmulcl  12375  nninfdclemcl  12448  nninfdclemp1  12450  nninfdclemlt  12451  unbendc  12454  strleund  12561  subgid  13033  issubg2m  13047  subsubg  13055  isringd  13218  ringsrg  13222  subrgsubg  13346  islmodd  13381  sin0pilem1  14172  sin0pilem2  14173  cosq14gt0  14223  cosq23lt0  14224  coseq0q4123  14225  coseq00topi  14226  coseq0negpitopi  14227  tangtx  14229  cosordlem  14240  cosq34lt1  14241  cos02pilt1  14242  cos0pilt1  14243  rplogbval  14333  lgsdilem2  14407  2sqlem3  14434  cvgcmp2nlemabs  14750  iooref1o  14752  taupi  14790