ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5bi Unicode 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  |-  ( ph  <->  ps )
syl5bi.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
syl5bi  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5bi
StepHypRef Expression
1 syl5bi.1 . . 3  |-  ( ph  <->  ps )
21biimpi 113 . 2  |-  ( ph  ->  ps )
3 syl5bi.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 28 1  |-  ( ch 
->  ( ph  ->  th )
)
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  2244  necon1aidc  2253  necon4addc  2272  spcimgft  2626  spcimegft  2628  rspc  2647  rspcimdv  2654  euind  2725  2reuswapdc  2740  reuind  2741  sbciegft  2790  rspsbc  2837  preqr2g  3535  prel12  3539  intss1  3627  intmin  3632  iinss  3705  trel3  3859  trin  3861  trintssm  3867  repizf2  3912  copsexg  3978  po3nr  4044  sowlin  4054  eusvnfb  4182  reusv3  4188  ssorduni  4209  ordsucim  4222  tfis2f  4294  ssrelrel  4427  relop  4473  iss  4641  poirr2  4704  funopg  4921  funssres  4929  funun  4931  funcnvuni  4955  fv3  5184  fvmptt  5249  dff4im  5300  f1eqcocnv  5418  oprabid  5524  f1o2ndf1  5836  poxp  5840  reldmtpos  5855  rntpos  5859  smoiun  5903  tfrlem1  5910  tfrlemi1  5933  tfrexlem  5935  tfri3  5940  rdgon  5960  nntri3or  6059  qsss  6152  th3qlem1  6195  phplem4  6305  ltmpig  6418  prcdnql  6563  prcunqu  6564  recexprlem1ssl  6712  recexprlem1ssu  6713  recexprlemss1l  6714  recexprlemss1u  6715  cauappcvgprlemladdru  6735  cauappcvgprlemladdrl  6736  caucvgprlemladdrl  6757  mulgt0sr  6843  axprecex  6935  ltxrlt  7065  cju  7889  nngt1ne1  7924  nnsub  7928  0mnnnnn0  8186  un0addcl  8187  un0mulcl  8188  zapne  8287  eluzuzle  8453  indstr  8508  ixxdisj  8739  icodisj  8827  uzsubsubfz  8878  elfzmlbp  8957  fzofzim  9011  expcl2lemap  9145  expnegzap  9167  expaddzap  9177  expmulzap  9179  ovshftex  9298  cau3lem  9588  2clim  9699  bj-vtoclgft  9787  bj-indind  9929  bj-nntrans  9949  bj-nnelirr  9951
  Copyright terms: Public domain W3C validator