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

Theorem sylanbrc 408
Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
sylanbrc.1 (𝜑𝜓)
sylanbrc.2 (𝜑𝜒)
sylanbrc.3 (𝜃 ↔ (𝜓𝜒))
Assertion
Ref Expression
sylanbrc (𝜑𝜃)

Proof of Theorem sylanbrc
StepHypRef Expression
1 sylanbrc.1 . . 3 (𝜑𝜓)
2 sylanbrc.2 . . 3 (𝜑𝜒)
31, 2jca 300 . 2 (𝜑 → (𝜓𝜒))
4 sylanbrc.3 . 2 (𝜃 ↔ (𝜓𝜒))
53, 4sylibr 132 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  sb2  1691  sbequ1  1692  sbidm  1773  eqeu  2763  euind  2780  reuind  2796  eldifd  2984  eqssd  3017  ssrabdv  3074  elind  3158  opm  3997  issod  4082  ordsucim  4252  onintonm  4269  ordtri2or2exmidlem  4277  en2lp  4305  ordwe  4326  sosng  4439  sotri2  4752  sotri3  4753  relssdmrn  4871  funun  4974  fnsng  4977  fnprg  4985  fntpg  4986  fntp  4987  fununi  4998  imain  5012  fnco  5038  f00  5112  f1ss  5128  f1ssr  5129  f1ssres  5130  f1f1orn  5168  foimacnv  5175  foun  5176  fun11iun  5178  sefvex  5227  dff3im  5344  foco2  5350  fmpt  5351  ffnfv  5355  fmpt2d  5359  ffvresb  5360  fprg  5378  fcof1  5454  fcofo  5455  fcof1o  5460  fliftf  5470  isoini2  5489  f1oiso  5496  moriotass  5527  fnoprabg  5633  f1ocnvd  5733  suppssfv  5739  suppssov1  5740  1stcof  5821  2ndcof  5822  1stconst  5873  2ndconst  5874  fo2ndf  5879  f1o2ndf1  5880  f1od2  5887  smores2  5943  tfrlem5  5963  tfrlemibfn  5977  tfr1onlembfn  5993  tfri1dALT  6000  tfrcllembfn  6006  nntri2  6138  eroveu  6263  dom2lem  6319  xpf1o  6385  fidifsnen  6405  unfidisj  6442  supeuti  6466  infeuti  6501  en2other2  6522  addclpi  6579  mulclpi  6580  nnppipi  6595  recmulnqg  6643  enq0ref  6685  nqnq0pi  6690  genipv  6761  addclpr  6789  nqprxx  6798  prmuloc  6818  mulclpr  6824  distrlem1prl  6834  distrlem1pru  6835  ltexprlempr  6860  ltexprlemrl  6862  ltexprlemru  6864  lteupri  6869  recexprlempr  6884  cauappcvgprlemm  6897  cauappcvgprlemopl  6898  cauappcvgprlemlol  6899  cauappcvgprlemopu  6900  cauappcvgprlemupu  6901  cauappcvgprlemloc  6904  cauappcvgprlemcl  6905  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlem2  6912  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemlol  6922  caucvgprlemopu  6923  caucvgprlemupu  6924  caucvgprlemloc  6927  caucvgprlemcl  6928  caucvgprlemladdfu  6929  caucvgprlem2  6932  caucvgprprlemml  6946  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemupu  6952  caucvgprprlemloc  6955  caucvgprprlemcl  6956  caucvgprprlem2  6962  elrealeu  7060  rereceu  7117  negf1o  7553  receuap  7826  divvalap  7829  cju  8105  nn0ge2m1nn  8415  nnnegz  8435  elnnz  8442  elnn0z  8445  peano2z  8468  nn0n0n1ge2  8499  msqznn  8528  eluzaddi  8726  eluzsubi  8727  uzind4  8757  supinfneg  8764  infsupneg  8765  elnn1uz2  8775  uz2mulcl  8776  divfnzn  8787  nnrp  8824  rpaddcl  8838  rpmulcl  8839  rpdivcl  8840  rpgecl  8843  ge0p1rp  8846  elrpd  8852  ge0addcl  9080  ge0mulcl  9081  icoshftf1o  9089  peano2fzr  9132  uzsubsubfz  9142  fzsplit2  9145  elfznn  9149  fzss1  9157  fzss2  9158  fzp1elp1  9168  elfz1b  9183  elfz0fzfz0  9214  fz0fzelfz0  9215  difelfznle  9223  elfzofz  9248  fzosplitsnm1  9295  ubmelm1fzo  9312  fzofzp1b  9314  fzosplitsn  9319  exbtwnz  9337  flqge0nn0  9375  flqge1nn  9376  zmodcl  9426  modqmuladdnn0  9450  modsumfzodifsn  9478  frec2uzf1od  9488  frec2uzisod  9489  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgtcl  9494  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgfunlem  9501  frecuzrdgtclt  9503  frecuzrdgsuctlem  9505  iseqfveq2  9544  monoord  9551  iseqid2  9564  serige0  9570  expival  9575  expcl2lemap  9585  expclzaplem  9597  expge0  9609  expge1  9610  zsqcl2  9650  bcval4  9776  bcn1  9782  bccl2  9792  sizeennnuni  9803  sizeunlem  9828  shftfn  9850  shftf  9856  recvguniq  10019  resqrexlemdecn  10036  rersqreu  10052  nn0abscl  10109  nnabscl  10124  abs2dif  10130  climuni  10270  2clim  10278  climcn2  10286  zdvdsdc  10361  fzo0dvdseq  10402  oexpneg  10421  oddge22np1  10425  evennn02n  10426  evennn2n  10427  nno  10450  divalglemeunn  10465  divalglemex  10466  divalglemeuneg  10467  divalg  10468  zsupcllemstep  10485  zsupcl  10487  divgcdz  10507  bezoutlemmain  10531  bezoutlemmo  10539  bezoutlemeu  10540  bezoutlemle  10541  sqgcd  10562  eucalgval2  10579  eucalglt  10583  lcmcllem  10593  lcmledvds  10596  lcmneg  10600  lcmgcdlem  10603  ncoprmgcdne1b  10615  prmind2  10646  sqnprm  10661  isprm6  10670  sqrt2irrlem  10684  pw2dvdseu  10690  sqpweven  10697  2sqpwodd  10698  sqrt2irrap  10702  oddennn  10703  evenennn  10704  znnen  10709  bj-nnord  10911  bj-inf2vnlem1  10923  qdencn  10943
  Copyright terms: Public domain W3C validator