Theorem syl3anbrc 1176

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 1172	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
5		syl3anbrc.4	. 2 |- ( ta <-> ( ps /\ ch /\ th ) )
6	4, 5	sylibr 133	1 |- ( ph -> ta )

Syntax hints:   -> wi 4   <-> wb 104   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  smores2  6273  smoiso  6281  iserd  6539  erinxp  6587  resixp  6711  prarloc  7465  eluzuzle  9495  uztrn  9503  nn0pzuz  9546  nn0ge2m1nnALT  9577  ige2m1fz  10066  0elfz  10074  uzsubfz0  10085  elfzmlbm  10087  difelfzle  10090  difelfznle  10091  elfzolt2b  10114  elfzolt3b  10115  elfzouz2  10117  fzossrbm1  10129  elfzo0  10138  eluzgtdifelfzo  10153  elfzodifsumelfzo  10157  fzonn0p1  10167  fzonn0p1p1  10169  elfzom1p1elfzo  10170  fzo0sn0fzo1  10177  ssfzo12bi  10181  ubmelm1fzo  10182  elfzonelfzo  10186  fzosplitprm1  10190  fzostep1  10193  fvinim0ffz  10197  flqword2  10245  modfzo0difsn  10351  modsumfzodifsn  10352  uzennn  10392  seq3split  10435  iseqf1olemkle  10440  iseqf1olemklt  10441  iseqf1olemqk  10450  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  bcval5  10697  1elfz0hash  10741  seq3coll  10777  seq3shft  10802  resqrexlemoverl  10985  fsum3cvg3  11359  fisumrev2  11409  isumshft  11453  cvgratnnlemseq  11489  cvgratnnlemabsle  11490  cvgratnnlemsumlt  11491  cvgratz  11495  sinbnd2  11717  cosbnd2  11718  cos12dec  11730  nn0o  11866  suprzubdc  11907  zsupssdc  11909  uzwodc  11992  dvdsnprmd  12079  eulerthlema  12184  hashgcdlem  12192  prm23lt5  12217  prm23ge5  12218  zgz  12325  gznegcl  12327  gzcjcl  12328  gzaddcl  12329  gzmulcl  12330  nninfdclemcl  12403  nninfdclemp1  12405  nninfdclemlt  12406  unbendc  12409  strleund  12506  sin0pilem1  13496  sin0pilem2  13497  cosq14gt0  13547  cosq23lt0  13548  coseq0q4123  13549  coseq00topi  13550  coseq0negpitopi  13551  tangtx  13553  cosordlem  13564  cosq34lt1  13565  cos02pilt1  13566  cos0pilt1  13567  rplogbval  13657  lgsdilem2  13731  2sqlem3  13747  cvgcmp2nlemabs  14064  iooref1o  14066  taupi  14102