Theorem syl3anbrc 1212

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  smores2  6565  smoiso  6573  iserd  6833  erinxp  6883  resixp  7015  netap  7620  2omotaplemap  7623  prarloc  7870  eluzmn  9928  eluzuzle  9930  uztrn  9939  nn0pzuz  9987  nn0ge2m1nnALT  10018  ige2m1fz  10517  0elfz  10525  uzsubfz0  10536  elfzmlbm  10538  difelfzle  10541  difelfznle  10542  elfzolt2b  10566  elfzolt3b  10567  elfzouz2  10569  fzossrbm1  10582  elfzo0  10593  eluzgtdifelfzo  10615  elfzodifsumelfzo  10619  fzonn0p1  10629  fzonn0p1p1  10631  elfzom1p1elfzo  10632  fzo0sn0fzo1  10639  ssfzo12bi  10643  ubmelm1fzo  10644  elfzonelfzo  10648  fzosplitprm1  10653  fzostep1  10656  fvinim0ffz  10660  suprzubdc  10671  zsupssdc  10673  flqword2  10724  modfzo0difsn  10832  modsumfzodifsn  10833  uzennn  10873  seq3split  10925  iseqf1olemkle  10934  iseqf1olemklt  10935  iseqf1olemqk  10944  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seq3f1olemqsum  10950  bcval5  11201  bcm1n  11207  1elfz0hash  11247  seq3coll  11294  ccatrn  11377  ccat2s1fvwd  11415  pfxn0  11460  pfxtrcfv0  11466  pfxtrcfvl  11469  swrdswrd  11477  swrdccatin1  11497  pfxccat3  11506  pfxccat3a  11510  cats1fvd  11538  seq3shft  11603  resqrexlemoverl  11787  fsum3cvg3  12163  fisumrev2  12213  isumshft  12257  cvgratnnlemseq  12293  cvgratnnlemabsle  12294  cvgratnnlemsumlt  12295  cvgratz  12299  sinbnd2  12521  cosbnd2  12522  sinltxirr  12528  cos12dec  12535  nn0o  12674  bitsfzolem  12721  bitsfzo  12722  bitsmod  12723  bitsfi  12724  bitsinv1lem  12728  bitsinv1  12729  uzwodc  12814  dvdsnprmd  12903  eulerthlema  13008  hashgcdlem  13016  prm23lt5  13042  prm23ge5  13043  zgz  13152  gznegcl  13154  gzcjcl  13155  gzaddcl  13156  gzmulcl  13157  ballotfilemsel1i  13256  ballotfilemro  13266  ballotfilemfrceq  13272  nninfdclemcl  13339  nninfdclemp1  13341  nninfdclemlt  13342  unbendc  13345  strleund  13457  gzsumcl  13804  subgid  13978  issubg2m  13992  subsubg  14000  gzsumreidx  14141  gzsumsubmcl  14142  gzsummhm  14145  gzsumsplit0  14148  gzsumshift  14149  gzsumgsum  14155  isrngd  14252  ringrng  14341  isringd  14346  ringsrg  14352  subrngid  14509  subrngsubg  14512  issubrng2  14518  subsubrng  14522  subrgsubg  14535  islmodd  14629  dflidl2rng  14818  rnglidlrng  14835  rng2idlsubrng  14854  znidomb  14993  plyaddlem1  15848  sin0pilem1  15882  sin0pilem2  15883  cosq14gt0  15933  cosq23lt0  15934  coseq0q4123  15935  coseq00topi  15936  coseq0negpitopi  15937  tangtx  15939  cosordlem  15950  cosq34lt1  15951  cos02pilt1  15952  cos0pilt1  15953  rplogbval  16047  lgsdilem2  16155  gausslemma2dlem1a  16177  gausslemma2dlem2  16181  gausslemma2dlem5  16185  gausslemma2dlem6  16186  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  2lgslem1  16210  2sqlem3  16236  umgr2cwwkdifex  16666  trlsegvdeglem6  16706  depindlem2  16748  nnnninfen  17064  repiecelem  17074  repiecele0  17075  repiecege0  17076  cvgcmp2nlemabs  17081  iooref1o  17083  taupi  17123