Theorem syl3anbrc 1182

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 1178	. 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 979

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 981

This theorem is referenced by:  smores2  6312  smoiso  6320  iserd  6578  erinxp  6626  resixp  6750  netap  7270  2omotaplemap  7273  prarloc  7519  eluzuzle  9553  uztrn  9561  nn0pzuz  9604  nn0ge2m1nnALT  9635  ige2m1fz  10127  0elfz  10135  uzsubfz0  10146  elfzmlbm  10148  difelfzle  10151  difelfznle  10152  elfzolt2b  10175  elfzolt3b  10176  elfzouz2  10178  fzossrbm1  10190  elfzo0  10199  eluzgtdifelfzo  10214  elfzodifsumelfzo  10218  fzonn0p1  10228  fzonn0p1p1  10230  elfzom1p1elfzo  10231  fzo0sn0fzo1  10238  ssfzo12bi  10242  ubmelm1fzo  10243  elfzonelfzo  10247  fzosplitprm1  10251  fzostep1  10254  fvinim0ffz  10258  flqword2  10306  modfzo0difsn  10412  modsumfzodifsn  10413  uzennn  10453  seq3split  10496  iseqf1olemkle  10501  iseqf1olemklt  10502  iseqf1olemqk  10511  seq3f1olemqsumkj  10515  seq3f1olemqsumk  10516  seq3f1olemqsum  10517  bcval5  10760  1elfz0hash  10803  seq3coll  10839  seq3shft  10864  resqrexlemoverl  11047  fsum3cvg3  11421  fisumrev2  11471  isumshft  11515  cvgratnnlemseq  11551  cvgratnnlemabsle  11552  cvgratnnlemsumlt  11553  cvgratz  11557  sinbnd2  11779  cosbnd2  11780  cos12dec  11792  nn0o  11929  suprzubdc  11970  zsupssdc  11972  uzwodc  12055  dvdsnprmd  12142  eulerthlema  12247  hashgcdlem  12255  prm23lt5  12280  prm23ge5  12281  zgz  12388  gznegcl  12390  gzcjcl  12391  gzaddcl  12392  gzmulcl  12393  nninfdclemcl  12466  nninfdclemp1  12468  nninfdclemlt  12469  unbendc  12472  strleund  12580  subgid  13079  issubg2m  13093  subsubg  13101  isrngd  13267  ringrng  13350  isringd  13355  ringsrg  13359  subrngid  13508  subrngsubg  13511  issubrng2  13517  subsubrng  13521  subrgsubg  13534  islmodd  13569  dflidl2rng  13757  rnglidlrng  13774  rng2idlsubrng  13792  sin0pilem1  14585  sin0pilem2  14586  cosq14gt0  14636  cosq23lt0  14637  coseq0q4123  14638  coseq00topi  14639  coseq0negpitopi  14640  tangtx  14642  cosordlem  14653  cosq34lt1  14654  cos02pilt1  14655  cos0pilt1  14656  rplogbval  14746  lgsdilem2  14820  2sqlem3  14847  cvgcmp2nlemabs  15164  iooref1o  15166  taupi  15205