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

Theorem syl5ibrcom 155
Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)
Hypotheses
Ref Expression
syl5ibr.1 (𝜑𝜃)
syl5ibr.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5ibrcom (𝜑 → (𝜒𝜓))

Proof of Theorem syl5ibrcom
StepHypRef Expression
1 syl5ibr.1 . . 3 (𝜑𝜃)
2 syl5ibr.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2syl5ibr 154 . 2 (𝜒 → (𝜑𝜓))
43com12 30 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  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:  biimprcd  158  elsn2g  3460  preqr1g  3593  opth1  4037  euotd  4055  tz7.2  4155  reusv3  4256  alxfr  4257  reuhypd  4267  ordsucim  4290  suc11g  4346  nlimsucg  4355  xpsspw  4518  funcnvuni  5048  fvmptdv2  5355  fsn  5432  fconst2g  5473  funfvima  5487  foco2  5494  isores3  5555  eusvobj2  5599  ovmpt2dv2  5735  ovelrn  5750  f1opw2  5807  suppssfv  5809  suppssov1  5810  nnmordi  6227  nnmord  6228  qsss  6303  eroveu  6335  th3qlem1  6346  mapsncnv  6404  en1bg  6469  mapxpen  6516  en1eqsnbi  6607  updjud  6717  addnidpig  6839  enq0tr  6937  prcdnql  6987  prcunqu  6988  genipv  7012  genpelvl  7015  genpelvu  7016  distrlem5prl  7089  distrlem5pru  7090  aptiprlemu  7143  mulid1  7429  ltne  7514  cnegex  7604  creur  8354  creui  8355  cju  8356  nnsub  8395  un0addcl  8639  un0mulcl  8640  zaddcl  8723  elz2  8751  qmulz  9040  qre  9042  qnegcl  9053  xrltne  9210  iccid  9275  fzsn  9411  fzsuc2  9423  fz1sbc  9440  elfzp12  9443  modqmuladd  9701  iseqid3  9840  ibcval5  10067  bcpasc  10070  hashprg  10112  hashfzo  10126  shftlem  10146  replim  10188  sqrtsq  10372  absle  10417  maxabslemval  10536  negfi  10552  isummolem2  10661  isummo  10662  zisum  10663  fisum  10665  fzo0dvdseq  10733  divalgmod  10802  gcdabs1  10855  dvdsgcd  10876  dvdsmulgcd  10889  lcmgcdeq  10940  isprm2lem  10973  dvdsprime  10979  coprm  10998  prmdvdsexpr  11004  rpexp  11007  phibndlem  11067  dfphi2  11071  hashgcdlem  11078  bj-peano4  11288
  Copyright terms: Public domain W3C validator