Theorem syl3anbrc 1208

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 1204	. 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 1005

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 1007

This theorem is referenced by:  smores2  6503  smoiso  6511  iserd  6771  erinxp  6821  resixp  6945  netap  7516  2omotaplemap  7519  prarloc  7766  eluzmn  9806  eluzuzle  9808  uztrn  9817  nn0pzuz  9865  nn0ge2m1nnALT  9896  ige2m1fz  10390  0elfz  10398  uzsubfz0  10409  elfzmlbm  10411  difelfzle  10414  difelfznle  10415  elfzolt2b  10439  elfzolt3b  10440  elfzouz2  10442  fzossrbm1  10455  elfzo0  10466  eluzgtdifelfzo  10488  elfzodifsumelfzo  10492  fzonn0p1  10502  fzonn0p1p1  10504  elfzom1p1elfzo  10505  fzo0sn0fzo1  10512  ssfzo12bi  10516  ubmelm1fzo  10517  elfzonelfzo  10521  fzosplitprm1  10526  fzostep1  10529  fvinim0ffz  10533  suprzubdc  10542  zsupssdc  10544  flqword2  10595  modfzo0difsn  10703  modsumfzodifsn  10704  uzennn  10744  seq3split  10796  iseqf1olemkle  10805  iseqf1olemklt  10806  iseqf1olemqk  10815  seq3f1olemqsumkj  10819  seq3f1olemqsumk  10820  seq3f1olemqsum  10821  bcval5  11071  1elfz0hash  11116  seq3coll  11152  ccatrn  11235  ccat2s1fvwd  11273  pfxn0  11318  pfxtrcfv0  11324  pfxtrcfvl  11327  swrdswrd  11335  swrdccatin1  11355  pfxccat3  11364  pfxccat3a  11368  cats1fvd  11396  seq3shft  11461  resqrexlemoverl  11644  fsum3cvg3  12020  fisumrev2  12070  isumshft  12114  cvgratnnlemseq  12150  cvgratnnlemabsle  12151  cvgratnnlemsumlt  12152  cvgratz  12156  sinbnd2  12378  cosbnd2  12379  sinltxirr  12385  cos12dec  12392  nn0o  12531  bitsfzolem  12578  bitsfzo  12579  bitsmod  12580  bitsfi  12581  bitsinv1lem  12585  bitsinv1  12586  uzwodc  12671  dvdsnprmd  12760  eulerthlema  12865  hashgcdlem  12873  prm23lt5  12899  prm23ge5  12900  zgz  13009  gznegcl  13011  gzcjcl  13012  gzaddcl  13013  gzmulcl  13014  nninfdclemcl  13132  nninfdclemp1  13134  nninfdclemlt  13135  unbendc  13138  strleund  13249  gsumfzz  13641  gsumfzcl  13645  subgid  13825  issubg2m  13839  subsubg  13847  gsumfzreidx  13987  gsumfzsubmcl  13988  gsumfzmptfidmadd  13989  gsumfzmhm  13993  gsumsplit0  13996  isrngd  14030  ringrng  14113  isringd  14118  ringsrg  14124  subrngid  14279  subrngsubg  14282  issubrng2  14288  subsubrng  14292  subrgsubg  14305  islmodd  14372  dflidl2rng  14560  rnglidlrng  14577  rng2idlsubrng  14596  gsumfzfsum  14667  znidomb  14737  plyaddlem1  15541  sin0pilem1  15575  sin0pilem2  15576  cosq14gt0  15626  cosq23lt0  15627  coseq0q4123  15628  coseq00topi  15629  coseq0negpitopi  15630  tangtx  15632  cosordlem  15643  cosq34lt1  15644  cos02pilt1  15645  cos0pilt1  15646  rplogbval  15739  lgsdilem2  15838  gausslemma2dlem1a  15860  gausslemma2dlem2  15864  gausslemma2dlem5  15868  gausslemma2dlem6  15869  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  2lgslem1  15893  2sqlem3  15919  umgr2cwwkdifex  16349  trlsegvdeglem6  16389  depindlem2  16431  nnnninfen  16730  repiecelem  16740  repiecele0  16741  repiecege0  16742  cvgcmp2nlemabs  16747  iooref1o  16749  taupi  16789  gsumgfsumlem  16795  gsumgfsum  16796