Theorem syl3anbrc 1205

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 1201	. 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 1002

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 1004

This theorem is referenced by:  smores2  6455  smoiso  6463  iserd  6723  erinxp  6773  resixp  6897  netap  7463  2omotaplemap  7466  prarloc  7713  eluzmn  9752  eluzuzle  9754  uztrn  9763  nn0pzuz  9811  nn0ge2m1nnALT  9842  ige2m1fz  10335  0elfz  10343  uzsubfz0  10354  elfzmlbm  10356  difelfzle  10359  difelfznle  10360  elfzolt2b  10384  elfzolt3b  10385  elfzouz2  10387  fzossrbm1  10400  elfzo0  10411  eluzgtdifelfzo  10432  elfzodifsumelfzo  10436  fzonn0p1  10446  fzonn0p1p1  10448  elfzom1p1elfzo  10449  fzo0sn0fzo1  10456  ssfzo12bi  10460  ubmelm1fzo  10461  elfzonelfzo  10465  fzosplitprm1  10470  fzostep1  10473  fvinim0ffz  10477  suprzubdc  10486  zsupssdc  10488  flqword2  10539  modfzo0difsn  10647  modsumfzodifsn  10648  uzennn  10688  seq3split  10740  iseqf1olemkle  10749  iseqf1olemklt  10750  iseqf1olemqk  10759  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  bcval5  11015  1elfz0hash  11060  seq3coll  11096  ccatrn  11176  ccat2s1fvwd  11214  pfxn0  11259  pfxtrcfv0  11265  pfxtrcfvl  11268  swrdswrd  11276  swrdccatin1  11296  pfxccat3  11305  pfxccat3a  11309  cats1fvd  11337  seq3shft  11389  resqrexlemoverl  11572  fsum3cvg3  11947  fisumrev2  11997  isumshft  12041  cvgratnnlemseq  12077  cvgratnnlemabsle  12078  cvgratnnlemsumlt  12079  cvgratz  12083  sinbnd2  12305  cosbnd2  12306  sinltxirr  12312  cos12dec  12319  nn0o  12458  bitsfzolem  12505  bitsfzo  12506  bitsmod  12507  bitsfi  12508  bitsinv1lem  12512  bitsinv1  12513  uzwodc  12598  dvdsnprmd  12687  eulerthlema  12792  hashgcdlem  12800  prm23lt5  12826  prm23ge5  12827  zgz  12936  gznegcl  12938  gzcjcl  12939  gzaddcl  12940  gzmulcl  12941  nninfdclemcl  13059  nninfdclemp1  13061  nninfdclemlt  13062  unbendc  13065  strleund  13176  gsumfzz  13568  gsumfzcl  13572  subgid  13752  issubg2m  13766  subsubg  13774  gsumfzreidx  13914  gsumfzsubmcl  13915  gsumfzmptfidmadd  13916  gsumfzmhm  13920  isrngd  13956  ringrng  14039  isringd  14044  ringsrg  14050  subrngid  14205  subrngsubg  14208  issubrng2  14214  subsubrng  14218  subrgsubg  14231  islmodd  14297  dflidl2rng  14485  rnglidlrng  14502  rng2idlsubrng  14521  gsumfzfsum  14592  znidomb  14662  plyaddlem1  15461  sin0pilem1  15495  sin0pilem2  15496  cosq14gt0  15546  cosq23lt0  15547  coseq0q4123  15548  coseq00topi  15549  coseq0negpitopi  15550  tangtx  15552  cosordlem  15563  cosq34lt1  15564  cos02pilt1  15565  cos0pilt1  15566  rplogbval  15659  lgsdilem2  15755  gausslemma2dlem1a  15777  gausslemma2dlem2  15781  gausslemma2dlem5  15785  gausslemma2dlem6  15786  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  2lgslem1  15810  2sqlem3  15836  umgr2cwwkdifex  16220  nnnninfen  16559  cvgcmp2nlemabs  16572  iooref1o  16574  taupi  16613