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

Theorem syl5ibrcom 156
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 155 . 2 (𝜒 → (𝜑𝜓))
43com12 30 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biimprcd  159  elsn2g  3526  preqr1g  3661  opth1  4126  euotd  4144  tz7.2  4244  reusv3  4349  alxfr  4350  reuhypd  4360  ordsucim  4384  suc11g  4440  nlimsucg  4449  xpsspw  4619  funcnvuni  5160  fvmptdv2  5476  fsn  5558  fconst2g  5601  funfvima  5615  foco2  5621  isores3  5682  eusvobj2  5726  ovmpodv2  5870  ovelrn  5885  f1opw2  5942  suppssfv  5944  suppssov1  5945  nnmordi  6378  nnmord  6379  qsss  6454  eroveu  6486  th3qlem1  6497  mapsncnv  6555  elixpsn  6595  ixpsnf1o  6596  en1bg  6660  mapxpen  6708  en1eqsnbi  6803  updjud  6933  addnidpig  7108  enq0tr  7206  prcdnql  7256  prcunqu  7257  genipv  7281  genpelvl  7284  genpelvu  7285  distrlem5prl  7358  distrlem5pru  7359  aptiprlemu  7412  mulid1  7727  ltne  7813  cnegex  7904  creur  8677  creui  8678  cju  8679  nnsub  8719  un0addcl  8964  un0mulcl  8965  zaddcl  9048  elz2  9076  qmulz  9367  qre  9369  qnegcl  9380  xrltne  9547  xlesubadd  9617  iccid  9659  fzsn  9797  fzsuc2  9810  fz1sbc  9827  elfzp12  9830  modqmuladd  10090  bcval5  10460  bcpasc  10463  hashprg  10505  hashfzo  10519  shftlem  10539  replim  10582  sqrtsq  10767  absle  10812  maxabslemval  10931  negfi  10950  xrmaxiflemval  10970  summodclem2  11102  summodc  11103  zsumdc  11104  fsum3  11107  fsummulc2  11168  fsum00  11182  isumsplit  11211  fzo0dvdseq  11462  divalgmod  11531  gcdabs1  11584  dvdsgcd  11607  dvdsmulgcd  11620  lcmgcdeq  11671  isprm2lem  11704  dvdsprime  11710  coprm  11729  prmdvdsexpr  11735  rpexp  11738  phibndlem  11798  dfphi2  11802  hashgcdlem  11809  istopon  12086  eltg3  12132  tgidm  12149  restbasg  12243  tgrest  12244  tgcn  12283  cnconst  12309  lmss  12321  txbas  12333  txbasval  12342  upxp  12347  blssps  12502  blss  12503  metrest  12581  blssioo  12620  elcncf1di  12641  bj-peano4  12987
  Copyright terms: Public domain W3C validator