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

Theorem syl5bi 141
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bi.1 (𝜑𝜓)
syl5bi.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5bi (𝜒 → (𝜑𝜃))

Proof of Theorem syl5bi
StepHypRef Expression
1 syl5bi.1 . . 3 (𝜑𝜓)
21biimpi 113 . 2 (𝜑𝜓)
3 syl5bi.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 28 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3imtr4g  194  ancomsd  256  pm2.13dc  779  3jao  1196  19.33b2  1520  sbequ2  1652  sbi1v  1771  mor  1942  2euex  1987  necon3ad  2247  necon1aidc  2256  necon4addc  2275  spcimgft  2629  spcimegft  2631  rspc  2650  rspcimdv  2657  euind  2728  2reuswapdc  2743  reuind  2744  sbciegft  2793  rspsbc  2840  preqr2g  3538  prel12  3542  intss1  3630  intmin  3635  iinss  3708  trel3  3862  trin  3864  trintssm  3870  repizf2  3915  copsexg  3981  po3nr  4047  sowlin  4057  eusvnfb  4186  reusv3  4192  ssorduni  4213  ordsucim  4226  tfis2f  4307  ssrelrel  4440  relop  4486  iss  4654  poirr2  4717  funopg  4934  funssres  4942  funun  4944  funcnvuni  4968  fv3  5197  fvmptt  5262  dff4im  5313  f1eqcocnv  5431  oprabid  5537  f1o2ndf1  5849  poxp  5853  reldmtpos  5868  rntpos  5872  smoiun  5916  tfrlem1  5923  tfrlemi1  5946  tfrexlem  5948  tfri3  5953  rdgon  5973  nntri3or  6072  qsss  6165  th3qlem1  6208  phplem4  6318  ordiso2  6357  ltmpig  6437  prcdnql  6582  prcunqu  6583  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1l  6733  recexprlemss1u  6734  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemladdrl  6776  mulgt0sr  6862  axprecex  6954  ltxrlt  7085  cju  7913  nngt1ne1  7948  nnsub  7952  0mnnnnn0  8214  un0addcl  8215  un0mulcl  8216  zapne  8315  eluzuzle  8481  indstr  8536  ixxdisj  8772  icodisj  8860  uzsubsubfz  8911  elfzmlbp  8990  fzofzim  9044  subfzo0  9097  expcl2lemap  9267  expnegzap  9289  expaddzap  9299  expmulzap  9301  ovshftex  9420  cau3lem  9710  2clim  9822  bj-vtoclgft  9914  bj-indind  10056  bj-nntrans  10076  bj-nnelirr  10078
  Copyright terms: Public domain W3C validator