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  9937  eluzuzle  9939  uztrn  9948  nn0pzuz  9996  nn0ge2m1nnALT  10027  ige2m1fz  10527  0elfz  10535  uzsubfz0  10546  elfzmlbm  10548  difelfzle  10551  difelfznle  10552  elfzolt2b  10576  elfzolt3b  10577  elfzouz2  10579  fzossrbm1  10592  elfzo0  10603  eluzgtdifelfzo  10625  elfzodifsumelfzo  10629  fzonn0p1  10639  fzonn0p1p1  10641  elfzom1p1elfzo  10642  fzo0sn0fzo1  10649  ssfzo12bi  10653  ubmelm1fzo  10654  elfzonelfzo  10658  fzosplitprm1  10663  fzostep1  10666  fvinim0ffz  10670  suprzubdc  10681  zsupssdc  10683  flqword2  10737  modfzo0difsn  10845  modsumfzodifsn  10846  uzennn  10886  seq3split  10938  iseqf1olemkle  10947  iseqf1olemklt  10948  iseqf1olemqk  10957  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  bcval5  11215  bcm1n  11221  1elfz0hash  11261  seq3coll  11308  ccatrn  11391  ccat2s1fvwd  11429  pfxn0  11474  pfxtrcfv0  11480  pfxtrcfvl  11483  swrdswrd  11491  swrdccatin1  11511  pfxccat3  11520  pfxccat3a  11524  cats1fvd  11552  seq3shft  11617  resqrexlemoverl  11801  fsum3cvg3  12179  fisumrev2  12229  isumshft  12273  cvgratnnlemseq  12309  cvgratnnlemabsle  12310  cvgratnnlemsumlt  12311  cvgratz  12315  sinbnd2  12537  cosbnd2  12538  sinltxirr  12544  cos12dec  12551  nn0o  12690  bitsfzolem  12737  bitsfzo  12738  bitsmod  12739  bitsfi  12740  bitsinv1lem  12744  bitsinv1  12745  uzwodc  12830  dvdsnprmd  12919  eulerthlema  13028  hashgcdlem  13036  prm23lt5  13062  prm23ge5  13063  zgz  13172  gznegcl  13174  gzcjcl  13175  gzaddcl  13176  gzmulcl  13177  ballotfilemsel1i  13305  ballotfilemro  13315  ballotfilemfrceq  13321  nninfdclemcl  13388  nninfdclemp1  13390  nninfdclemlt  13391  unbendc  13394  strleund  13506  gzsumcl  13853  subgid  14027  issubg2m  14041  subsubg  14049  gzsumreidx  14190  gzsumsubmcl  14191  gzsummhm  14194  gzsumsplit0  14197  gzsumshift  14198  gzsumgsum  14204  isrngd  14301  ringrng  14390  isringd  14395  ringsrg  14401  subrngid  14558  subrngsubg  14561  issubrng2  14567  subsubrng  14571  subrgsubg  14584  islmodd  14678  dflidl2rng  14867  rnglidlrng  14884  rng2idlsubrng  14903  znidomb  15042  plyaddlem1  15897  sin0pilem1  15932  sin0pilem2  15933  cosq14gt0  15983  cosq23lt0  15984  coseq0q4123  15985  coseq00topi  15986  coseq0negpitopi  15987  tangtx  15989  cosordlem  16000  cosq34lt1  16001  cos02pilt1  16002  cos0pilt1  16003  rplogbval  16100  ppiqsval  16156  ppidif  16175  ppiqub  16194  bposlem4  16212  lgsdilem2  16253  gausslemma2dlem1a  16275  gausslemma2dlem2  16279  gausslemma2dlem5  16283  gausslemma2dlem6  16284  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  2lgslem1  16308  2sqlem3  16334  umgr2cwwkdifex  16764  trlsegvdeglem6  16804  depindlem2  16846  nnnninfen  17162  repiecelem  17172  repiecele0  17173  repiecege0  17174  cvgcmp2nlemabs  17179  iooref1o  17181  taupi  17221