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  6295  smoiso  6303  iserd  6561  erinxp  6609  resixp  6733  netap  7253  2omotaplemap  7256  prarloc  7502  eluzuzle  9536  uztrn  9544  nn0pzuz  9587  nn0ge2m1nnALT  9618  ige2m1fz  10110  0elfz  10118  uzsubfz0  10129  elfzmlbm  10131  difelfzle  10134  difelfznle  10135  elfzolt2b  10158  elfzolt3b  10159  elfzouz2  10161  fzossrbm1  10173  elfzo0  10182  eluzgtdifelfzo  10197  elfzodifsumelfzo  10201  fzonn0p1  10211  fzonn0p1p1  10213  elfzom1p1elfzo  10214  fzo0sn0fzo1  10221  ssfzo12bi  10225  ubmelm1fzo  10226  elfzonelfzo  10230  fzosplitprm1  10234  fzostep1  10237  fvinim0ffz  10241  flqword2  10289  modfzo0difsn  10395  modsumfzodifsn  10396  uzennn  10436  seq3split  10479  iseqf1olemkle  10484  iseqf1olemklt  10485  iseqf1olemqk  10494  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  seq3f1olemqsum  10500  bcval5  10743  1elfz0hash  10786  seq3coll  10822  seq3shft  10847  resqrexlemoverl  11030  fsum3cvg3  11404  fisumrev2  11454  isumshft  11498  cvgratnnlemseq  11534  cvgratnnlemabsle  11535  cvgratnnlemsumlt  11536  cvgratz  11540  sinbnd2  11762  cosbnd2  11763  cos12dec  11775  nn0o  11912  suprzubdc  11953  zsupssdc  11955  uzwodc  12038  dvdsnprmd  12125  eulerthlema  12230  hashgcdlem  12238  prm23lt5  12263  prm23ge5  12264  zgz  12371  gznegcl  12373  gzcjcl  12374  gzaddcl  12375  gzmulcl  12376  nninfdclemcl  12449  nninfdclemp1  12451  nninfdclemlt  12452  unbendc  12455  strleund  12562  subgid  13035  issubg2m  13049  subsubg  13057  isringd  13220  ringsrg  13224  subrgsubg  13348  islmodd  13383  sin0pilem1  14205  sin0pilem2  14206  cosq14gt0  14256  cosq23lt0  14257  coseq0q4123  14258  coseq00topi  14259  coseq0negpitopi  14260  tangtx  14262  cosordlem  14273  cosq34lt1  14274  cos02pilt1  14275  cos0pilt1  14276  rplogbval  14366  lgsdilem2  14440  2sqlem3  14467  cvgcmp2nlemabs  14783  iooref1o  14785  taupi  14823