ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl3anbrc GIF version

Theorem syl3anbrc 1181
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
StepHypRef Expression
1 syl3anbrc.1 . . 3 (𝜑𝜓)
2 syl3anbrc.2 . . 3 (𝜑𝜒)
3 syl3anbrc.3 . . 3 (𝜑𝜃)
41, 2, 33jca 1177 . 2 (𝜑 → (𝜓𝜒𝜃))
5 syl3anbrc.4 . 2 (𝜏 ↔ (𝜓𝜒𝜃))
64, 5sylibr 134 1 (𝜑𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  w3a 978
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 980
This theorem is referenced by:  smores2  6288  smoiso  6296  iserd  6554  erinxp  6602  resixp  6726  prarloc  7480  eluzuzle  9512  uztrn  9520  nn0pzuz  9563  nn0ge2m1nnALT  9594  ige2m1fz  10083  0elfz  10091  uzsubfz0  10102  elfzmlbm  10104  difelfzle  10107  difelfznle  10108  elfzolt2b  10131  elfzolt3b  10132  elfzouz2  10134  fzossrbm1  10146  elfzo0  10155  eluzgtdifelfzo  10170  elfzodifsumelfzo  10174  fzonn0p1  10184  fzonn0p1p1  10186  elfzom1p1elfzo  10187  fzo0sn0fzo1  10194  ssfzo12bi  10198  ubmelm1fzo  10199  elfzonelfzo  10203  fzosplitprm1  10207  fzostep1  10210  fvinim0ffz  10214  flqword2  10262  modfzo0difsn  10368  modsumfzodifsn  10369  uzennn  10409  seq3split  10452  iseqf1olemkle  10457  iseqf1olemklt  10458  iseqf1olemqk  10467  seq3f1olemqsumkj  10471  seq3f1olemqsumk  10472  seq3f1olemqsum  10473  bcval5  10714  1elfz0hash  10757  seq3coll  10793  seq3shft  10818  resqrexlemoverl  11001  fsum3cvg3  11375  fisumrev2  11425  isumshft  11469  cvgratnnlemseq  11505  cvgratnnlemabsle  11506  cvgratnnlemsumlt  11507  cvgratz  11511  sinbnd2  11733  cosbnd2  11734  cos12dec  11746  nn0o  11882  suprzubdc  11923  zsupssdc  11925  uzwodc  12008  dvdsnprmd  12095  eulerthlema  12200  hashgcdlem  12208  prm23lt5  12233  prm23ge5  12234  zgz  12341  gznegcl  12343  gzcjcl  12344  gzaddcl  12345  gzmulcl  12346  nninfdclemcl  12419  nninfdclemp1  12421  nninfdclemlt  12422  unbendc  12425  strleund  12531  isringd  13033  ringsrg  13037  sin0pilem1  13835  sin0pilem2  13836  cosq14gt0  13886  cosq23lt0  13887  coseq0q4123  13888  coseq00topi  13889  coseq0negpitopi  13890  tangtx  13892  cosordlem  13903  cosq34lt1  13904  cos02pilt1  13905  cos0pilt1  13906  rplogbval  13996  lgsdilem2  14070  2sqlem3  14086  cvgcmp2nlemabs  14403  iooref1o  14405  taupi  14441
  Copyright terms: Public domain W3C validator