Theorem syl3anbrc 1183

Description: Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)

Hypotheses

Ref	Expression
syl3anbrc.1	⊢ (𝜑 → 𝜓)
syl3anbrc.2	⊢ (𝜑 → 𝜒)
syl3anbrc.3	⊢ (𝜑 → 𝜃)
syl3anbrc.4	⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
syl3anbrc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl3anbrc

Step	Hyp	Ref	Expression
1		syl3anbrc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anbrc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anbrc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1179	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3anbrc.4	. 2 ⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
6	4, 5	sylibr 134	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 105   ∧ w3a 980

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 982

This theorem is referenced by:  smores2  6361  smoiso  6369  iserd  6627  erinxp  6677  resixp  6801  netap  7337  2omotaplemap  7340  prarloc  7587  eluzuzle  9626  uztrn  9635  nn0pzuz  9678  nn0ge2m1nnALT  9709  ige2m1fz  10202  0elfz  10210  uzsubfz0  10221  elfzmlbm  10223  difelfzle  10226  difelfznle  10227  elfzolt2b  10251  elfzolt3b  10252  elfzouz2  10254  fzossrbm1  10266  elfzo0  10275  eluzgtdifelfzo  10290  elfzodifsumelfzo  10294  fzonn0p1  10304  fzonn0p1p1  10306  elfzom1p1elfzo  10307  fzo0sn0fzo1  10314  ssfzo12bi  10318  ubmelm1fzo  10319  elfzonelfzo  10323  fzosplitprm1  10327  fzostep1  10330  fvinim0ffz  10334  suprzubdc  10343  zsupssdc  10345  flqword2  10396  modfzo0difsn  10504  modsumfzodifsn  10505  uzennn  10545  seq3split  10597  iseqf1olemkle  10606  iseqf1olemklt  10607  iseqf1olemqk  10616  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  bcval5  10872  1elfz0hash  10915  seq3coll  10951  seq3shft  11020  resqrexlemoverl  11203  fsum3cvg3  11578  fisumrev2  11628  isumshft  11672  cvgratnnlemseq  11708  cvgratnnlemabsle  11709  cvgratnnlemsumlt  11710  cvgratz  11714  sinbnd2  11936  cosbnd2  11937  sinltxirr  11943  cos12dec  11950  nn0o  12089  bitsfzolem  12136  bitsfzo  12137  bitsmod  12138  bitsfi  12139  bitsinv1lem  12143  bitsinv1  12144  uzwodc  12229  dvdsnprmd  12318  eulerthlema  12423  hashgcdlem  12431  prm23lt5  12457  prm23ge5  12458  zgz  12567  gznegcl  12569  gzcjcl  12570  gzaddcl  12571  gzmulcl  12572  nninfdclemcl  12690  nninfdclemp1  12692  nninfdclemlt  12693  unbendc  12696  strleund  12806  gsumfzz  13197  gsumfzcl  13201  subgid  13381  issubg2m  13395  subsubg  13403  gsumfzreidx  13543  gsumfzsubmcl  13544  gsumfzmptfidmadd  13545  gsumfzmhm  13549  isrngd  13585  ringrng  13668  isringd  13673  ringsrg  13679  subrngid  13833  subrngsubg  13836  issubrng2  13842  subsubrng  13846  subrgsubg  13859  islmodd  13925  dflidl2rng  14113  rnglidlrng  14130  rng2idlsubrng  14149  gsumfzfsum  14220  znidomb  14290  plyaddlem1  15067  sin0pilem1  15101  sin0pilem2  15102  cosq14gt0  15152  cosq23lt0  15153  coseq0q4123  15154  coseq00topi  15155  coseq0negpitopi  15156  tangtx  15158  cosordlem  15169  cosq34lt1  15170  cos02pilt1  15171  cos0pilt1  15172  rplogbval  15265  lgsdilem2  15361  gausslemma2dlem1a  15383  gausslemma2dlem2  15387  gausslemma2dlem5  15391  gausslemma2dlem6  15392  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  2lgslem1  15416  2sqlem3  15442  nnnninfen  15752  cvgcmp2nlemabs  15763  iooref1o  15765  taupi  15804