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 )

Syntax hints:   -> wi 4   <-> wb 105   /\ w3a 1009

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 1011

This theorem is referenced by:  smores2  6555  smoiso  6563  iserd  6823  erinxp  6873  resixp  7005  netap  7610  2omotaplemap  7613  prarloc  7860  eluzmn  9907  eluzuzle  9909  uztrn  9918  nn0pzuz  9966  nn0ge2m1nnALT  9997  ige2m1fz  10495  0elfz  10503  uzsubfz0  10514  elfzmlbm  10516  difelfzle  10519  difelfznle  10520  elfzolt2b  10544  elfzolt3b  10545  elfzouz2  10547  fzossrbm1  10560  elfzo0  10571  eluzgtdifelfzo  10593  elfzodifsumelfzo  10597  fzonn0p1  10607  fzonn0p1p1  10609  elfzom1p1elfzo  10610  fzo0sn0fzo1  10617  ssfzo12bi  10621  ubmelm1fzo  10622  elfzonelfzo  10626  fzosplitprm1  10631  fzostep1  10634  fvinim0ffz  10638  suprzubdc  10649  zsupssdc  10651  flqword2  10702  modfzo0difsn  10810  modsumfzodifsn  10811  uzennn  10851  seq3split  10903  iseqf1olemkle  10912  iseqf1olemklt  10913  iseqf1olemqk  10922  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seq3f1olemqsum  10928  bcval5  11179  bcm1n  11185  1elfz0hash  11225  seq3coll  11272  ccatrn  11355  ccat2s1fvwd  11393  pfxn0  11438  pfxtrcfv0  11444  pfxtrcfvl  11447  swrdswrd  11455  swrdccatin1  11475  pfxccat3  11484  pfxccat3a  11488  cats1fvd  11516  seq3shft  11581  resqrexlemoverl  11765  fsum3cvg3  12141  fisumrev2  12191  isumshft  12235  cvgratnnlemseq  12271  cvgratnnlemabsle  12272  cvgratnnlemsumlt  12273  cvgratz  12277  sinbnd2  12499  cosbnd2  12500  sinltxirr  12506  cos12dec  12513  nn0o  12652  bitsfzolem  12699  bitsfzo  12700  bitsmod  12701  bitsfi  12702  bitsinv1lem  12706  bitsinv1  12707  uzwodc  12792  dvdsnprmd  12881  eulerthlema  12986  hashgcdlem  12994  prm23lt5  13020  prm23ge5  13021  zgz  13130  gznegcl  13132  gzcjcl  13133  gzaddcl  13134  gzmulcl  13135  ballotfilemsel1i  13234  ballotfilemro  13244  ballotfilemfrceq  13250  nninfdclemcl  13317  nninfdclemp1  13319  nninfdclemlt  13320  unbendc  13323  strleund  13434  gzsumcl  13781  subgid  13955  issubg2m  13969  subsubg  13977  gzsumreidx  14118  gzsumsubmcl  14119  gzsummhm  14122  gzsumsplit0  14125  gzsumshift  14126  gzsumgsum  14132  isrngd  14227  ringrng  14314  isringd  14319  ringsrg  14325  subrngid  14482  subrngsubg  14485  issubrng2  14491  subsubrng  14495  subrgsubg  14508  islmodd  14602  dflidl2rng  14790  rnglidlrng  14807  rng2idlsubrng  14826  znidomb  14965  plyaddlem1  15771  sin0pilem1  15805  sin0pilem2  15806  cosq14gt0  15856  cosq23lt0  15857  coseq0q4123  15858  coseq00topi  15859  coseq0negpitopi  15860  tangtx  15862  cosordlem  15873  cosq34lt1  15874  cos02pilt1  15875  cos0pilt1  15876  rplogbval  15970  lgsdilem2  16069  gausslemma2dlem1a  16091  gausslemma2dlem2  16095  gausslemma2dlem5  16099  gausslemma2dlem6  16100  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  2lgslem1  16124  2sqlem3  16150  umgr2cwwkdifex  16580  trlsegvdeglem6  16620  depindlem2  16662  nnnninfen  16969  repiecelem  16979  repiecele0  16980  repiecege0  16981  cvgcmp2nlemabs  16986  iooref1o  16988  taupi  17028