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
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  778  3jao  1195  19.33b2  1517  sbequ2  1649  sbi1v  1768  mor  1939  2euex  1984  necon3ad  2241  necon1aidc  2250  necon4addc  2269  spcimgft  2623  spcimegft  2625  rspc  2644  rspcimdv  2651  euind  2722  2reuswapdc  2737  reuind  2738  sbciegft  2787  rspsbc  2834  preqr2g  3529  prel12  3533  intss1  3621  intmin  3626  iinss  3699  trel3  3853  trin  3855  trintssm  3861  repizf2  3906  copsexg  3972  po3nr  4038  sowlin  4048  eusvnfb  4152  reusv3  4158  ssorduni  4179  ordsucim  4192  tfis2f  4250  ssrelrel  4383  relop  4429  iss  4597  poirr2  4660  funopg  4877  funssres  4885  funun  4887  funcnvuni  4911  fv3  5140  fvmptt  5205  dff4im  5256  f1eqcocnv  5374  oprabid  5480  f1o2ndf1  5791  poxp  5794  reldmtpos  5809  rntpos  5813  smoiun  5857  tfrlem1  5864  tfrlemi1  5887  tfrexlem  5889  tfri3  5894  rdgon  5913  nntri3or  6011  qsss  6101  th3qlem1  6144  ltmpig  6323  prcdnql  6467  prcunqu  6468  recexprlem1ssl  6605  recexprlem1ssu  6606  recexprlemss1l  6607  recexprlemss1u  6608  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  caucvgprlemladdrl  6649  mulgt0sr  6704  axprecex  6764  ltxrlt  6882  cju  7694  nngt1ne1  7729  nnsub  7733  0mnnnnn0  7990  un0addcl  7991  un0mulcl  7992  zapne  8091  eluzuzle  8257  indstr  8312  ixxdisj  8542  icodisj  8630  uzsubsubfz  8681  elfzmlbp  8760  fzofzim  8814  expcl2lemap  8921  expnegzap  8943  expaddzap  8953  expmulzap  8955  bj-vtoclgft  9249  bj-indind  9391  bj-nntrans  9411  bj-nnelirr  9413
  Copyright terms: Public domain W3C validator